[Agda] Mixfix binders: first patch

Jean-Philippe Bernardy bernardy at chalmers.se
Mon Sep 13 15:30:34 CEST 2010


> On a related note, is there a way to give the associativity/precedence
> of the new notation?

Fixities can already be specified for any names, so the fixity of the
name will be used.

Cheers,
JP.


More information about the Agda mailing list