[Agda] Optimised equational reasoning

[Andreas Abel]

On 04.11.2016 14:44, Andrew Pitts wrote:
>>   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.”)

Documentation fixed on Agda-2.5.2/2.6.0.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/