2 ms·
Just glancing over this (super cool, John!), but what's going on here: Notation "f <~ g" := (f ~> g) (at level 70). Seems likely to cause confusion... wha
by thinkpad20 11y ago
Just glancing over this (super cool, John!), but what's going on here:
Notation "f <~ g" := (f ~> g) (at level 70).
Seems likely to cause confusion... what's the reasoning/explanation behind this? I might imagine a law such as Notation "f <~ g" := (g ~> f), but...?
It's been too long since I wrote some Coq! Gotta get back into it :)