idris-lang/Idris-dev — pull request #730 by david-christiansen (2013-12-15 10:47:52+00:00)
Title: Syntax for preorder reasoning over equality and isomorphisms

This enables Agda-style preorder reasoning. Implementations are included for isomorphisms and for propositional equality. It is implemented by desugaring to overloadable function names, so it should be quite flexible.