The Coq mailing list

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

Hi,

On Sun, Jun 29, 2008 at 05:51:06PM -0700, gang chen wrote:
> 
> I'd like to define constants which can work with "match".
> 
> First, I tried
> 
> Notation Jan := 1.
> Notation Feb := 2.
> 
> Definition next_month (n:nat) :=
>   match n with
>     Jan => Feb
> |  ...
> 
> Then, coqc shows :
> Error: The constructor S expects 1 argument
> 
> Then, I tried
> 
> Notation "'Jan'" := 1.
> Notation "'Feb'" := 2.
> 
> It works almost fine except that coqc gave a warning message:
> Defining 'Jan' as keyword
> Defining 'Feb' as key word
> 
> Is it possible to not to display these messages ?
> 
> Besides, why the two Notation definitions behave differently ?

The first notation introduces new names for denoting 1 and 2. It does
not modify the parser.

The second notation modifies the parser. "Jan" and "Feb" become tokens
and can no longer be used as regular identifiers.

If you try Coq V8.2 beta, it will work with the first notation, w/o
needing to modify the parser (i.e. without using the second kind of
notation).

Best regards,

Hugo Herbelin