lemming at henning-thielemann.de
Mon Jan 18 09:32:15 UTC 2016
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.
More information about the Libraries