[Agda] Mixfix binders: first patch
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Mon Sep 13 11:25:31 CEST 2010
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
More information about the Agda
mailing list