[Agda] Mixfix binders: first patch

[Andreas Abel]

Great stuff!

Even though Agda is not Coq (and syntax is not notation), I suggest to  
swap sides in the syntax definition

   syntax new-notation = definition-in-terms-of-old-notation

Seems to be more consistent with the usual way of defining things.

Cheers,
Andreas

On Sep 12, 2010, at 12:45 PM, Jean-Philippe Bernardy wrote:

> I have implemented a bit more of this, and uploaded the patch bundle
> to the issue tracker.
>
> You can now define simple binders. ie. a declaration like
>
> syntax bind e1 (\x → e2) = x ← e1 ; e2
>
> allows to write the rhs to mean the lhs.
>
> http://code.google.com/p/agda/issues/detail?id=306
>
> Cheers,
> JP.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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