[Agda] Mixfix binders: first patch

[Andreas Abel]

On Sep 13, 2010, at 2:23 AM, Nils Anders Danielsson wrote:

> 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.

??? What do you mean by that?

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.

I find it awkward to define a a new function by

   def plus x x = mult2 x

where "an alternative expression for plus x x is mult2 x".

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/