The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-04-17, Vladimir Voevodsky wrote:
> Hello,
> 
> 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.
I don't think you want type_scope here.
> 
> 
> 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?

In this case, you could write:

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

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

One difference is that tpair and total2 are treated like normal
identifiers by the parser, rather than adding new rules to the parser.

The parser for patterns is different from the one for general terms,
although I am not entirely sure why it isn't accepting this case.

  Tom