The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> I am trying to learn the Coq system for notations. When I write:
> 
> 
> Notation "'total2'" := (@sigT) (at level 0): type_scope. 
> Notation "'tpair'" := (@existT) (at level 0) : type_scope.
> 
> Definition pr21 (T:UU) (P:T -> UU) (z: total2 T P) : T := 
> match z with 
> tpair t x => t
> end.  
> 
> Coq complains at the definition by saying "Constructor expected". What is 
> wrong there?

There are two kinds of notation. There are notations that modify the
parser (the one written with double quotes as above) and there are
notations that are just aliases (names) for arbitrary expressions.

It turns out that the first kind of notations is supported in patterns
only when it abbreviates the whole pattern to match (it could be made
differently but we did not see a need for it yet). For instance,
defining

Notation "'tpair' x y" := (@existT _ _ x y) (x, y at level 9, at level 10).

makes definition pr21 accepted.

In your case, since the objective is mainly to rename a constant,
using the second kind of notation would be preferable (in particular,
it does not modify the parser nor reserve "tpair" to be a keyword as
the first kind of notation does).

So my suggestion would be to write:

Notation total2 := @sigT.
Notation tpair := (@existT _ _).

Definition pr21 (T:UU) (P:T -> UU) (z: total2 T P) : T :=
match z with                                                                  
tpair t x => t
end.

Note that we lose the ability to mention scopes with the second kind
of notation, but in the current case, it is probably harmless unless
you intend to reuse the names total2 and tpair with a different
meaning when not in type position.

Hope it helps,

Hugo