[Agda] Mixfix binders: first patch

Jean-Philippe Bernardy bernardy at chalmers.se
Fri Sep 10 17:33:27 CEST 2010


Hello,

Here is a first patch towards supporting mixfix binders, as described in

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=MixFixBinders.MixFixBinders

The feature is not complete, however since the patch is getting non-trivial,
I'm submitting this intermediate version to avoid the "code bomb" effect.

What you can currently do is only to swap the order of arguments to a function:

syntax identity A a = a :: A


Cheers,
JP.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: mixfix.patch
Type: application/octet-stream
Size: 87381 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100910/e6573a9a/mixfix-0001.obj


More information about the Agda mailing list