[Agda] Mixfix binders: first patch

[Nils Anders Danielsson]

On 2010-09-13 10:15, Andreas Abel wrote:
> On Sep 13, 2010, at 2:23 AM, Nils Anders Danielsson wrote:
>> 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.
>
> ??? What do you mean by that?

syntax <symbol we're defining syntax for> <bound variables> =
   <new notation making use of the bound variables>

> If I write something like
>
> Notation "exists x : A, B" := sigT A (fun x => B).
>
> then the variables bound on the lhs are x,A,B where x is an identifier
> for a variable.

But you have to read the RHS to know which of them are variables.

-- 
/NAD