[Agda] Mixfix binders: first patch

[Nils Anders Danielsson]

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

Two points:

* How could the variables be bound in the new notation? You could have

     syntax foo a b c = bar a b c

   just as well as

     syntax c a b bar = bar a b c.

   The two right-hand sides here are identical, but the sets of bound
   variables are not.

* I don't expect to be allowed to write non-linear LHSs. What would the
   following declaration mean?

     syntax foo a a = bar a

   When pretty-printing "foo e₁ e₂", should Agda first check if e₁ and e₂
   are syntactically equal, and only in that case use the new syntax?

> Unless we want to allow non-linear new notation like
>
> Notation "x : A =myFakeHetId= y : A" := _==_ {A} x y
>
> which I rather would not.

Me neither.

-- 
/NAD