Support logical implication syntax in annotations

[coord-e]

one idea is to have a single layer of macro_rules! for formula_fn expansion

[coord-e]

okay macro_rules! isn't expressive enough to add a new binop