The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

> On Sun, Mar 14, 2010 at 08:52:24AM +0100, 
>Â megacz AT cs.berkeley.edu
>  wrote:
>> Coq will let me use a notation in the definition of an inductive type:
>>
>>  Reserved Notation "a &&& b" (at level 50).
>>  Inductive And (A B:Prop) : Prop :=
>>     conj : A -> B -> A &&& B
>>  where "a &&& b" := (And a b).
>>
>> ... but does not seem to let me do the same thing for a Record type:
>>
>>  Reserved Notation "a &&& b" (at level 50).
>>  Record And (A B:Prop) := {
>>     foo : Prop -> Prop -> Prop            ;
>>     conj : A -> B -> A &&& B -> Prop
>>  } where "a &&& b" := (foo a b).
>>
>> Is there any way to use a notation within the Record that defines terms
>> used in the expansion of the Notation?
>
>  Reserved Notation "a &&& b" (at level 50).
>  Record And (A B:Prop) := {
>     foo : Prop -> Prop -> Prop
>         where "a &&& b" := (foo a b);
>     conj : A -> B -> A &&& B -> Prop
>  }.
Does it really work? The "where" is completely misleading as it refers to
something not yet used...
>
>
> Thanks
> Ian
>
>


-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay