[Agda] Optimised equational reasoning

[Andrew Pitts]

On 4 November 2016 at 11:35, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> Hi,
>
> At the last Agda meeting Ulf and I optimised an equational reasoning
> combinator, and I thought others might want to know about the technique
> we used.
>
> Consider the following transitivity combinator:
>
>   infixr -2 _≡⟨⟩_
>….

Not that it is relevant to your post, but I am surprised to find out
from your code snippet that Agda accepts negative integers as
precendence levels.  (The documentation
<http://agda.readthedocs.io/en/latest/language/mixfix-operators.html>
says “Each operator is associated to a precedence, which is a natural
number. The default precedence for an operator is 20.”) It would be
even nicer if it accepted rational numbers. :-)

Andy