18 Jan
2016
18 Jan
'16
9:32 a.m.
On Mon, 18 Jan 2016, Andrew Butterfield wrote:
In equational logic, it makes more sense for implication to bind tighter than equivalence, and it would usually be considered as infixr
a `implies` b `implies` c same as a `implies` (b `implies` c)
But if this breaks something else then plain infix is fine....
That this is the same associativity rule as for function arrows is not a coincidence, by the way.
It is currying in logic. I assume it was the reason to make 'implies' infixr in utility-ht.