The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

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


Thanks
Ian