The Coq mailing list

[megacz AT cs.berkeley.edu]

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?

 - a