The Coq mailing list

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

> 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
>
Your example is quite strange for defining the And; I would rather do:

Record And (A B:Prop) := {
     proj1 : A;
     proj2 : B
  }.
Notation "a &&& b" := (And a b).

I have not Coq currently, so I can't try it, but what you di is rather:

>  Reserved Notation "a &&& b" (at level 50).
>  Inductive And (A B:Prop) : Prop :=
>     conj : forall (foo: Prop -> Prop -> Prop),
>               A -> B -> (foo A B) -> a &&& b
>  where "a &&& b" := (And a b).

And you clearly can't call the &&& notation for foo in this definition.

The aim of "a &&& b" is to replace the 'And a b' which doesn't appear
anymore in the Record definition...

If your definition was allowed, it would mean that you want to be able to
define things like:

Reserved Notation "a &&& b" (at level 50).
Definition conj A B (foo: Prop -> Prop -> Prop) a b (c: A &&& B) :=
 and A B
where "a &&& b" := (foo a b).

Which is not allowed in Coq (allowing it could be a feature of rather low
interest [but low doesn't mean no!] as it would die at end of definition).
-- 
Cédric AUGER

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