[Agda] Mixfix binders: first patch

[Nils Anders Danielsson]

On 2010-09-13 00:52, Andreas Abel wrote:
> 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.

Choice 1: "syntax e = e′" means "an alternative syntax for e is e′".

Choice 2: "syntax e = e′" means "e is an alternative syntax for e′".

I think I prefer choice 1 (the currently implemented one), because when
this notation is used variables are bound as in an ordinary function
definition: to the left of their use sites.

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

--
/NAD