[Agda] Mixfix binders: first patch

[Andreas Abel]

On Sep 13, 2010, at 11:25 AM, Nils Anders Danielsson wrote:
> 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.

Thanks for the explanation.

May I ask you for email discussions like this one to not cut away the  
arguments you have not responded to?

The cut-away argument implies that the RHS (in the terminology above)  
is not linear in the use of variables, e.g., you could have

   Notation "exists x : A, B" := sigT A (fun x:A => B)

which would hint toward binding the variables in the new notation  
rather than the old one.  Unless we want to allow non-linear new  
notation like

   Notation "x : A =myFakeHetId= y : A" := _==_ {A} x y

which I rather would not.

Cheers,
Andreas

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/