The Coq mailing list

[gang chen <gangchen_sh AT yahoo.com>]

Hello all,

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 ?

gang chen




-- 
View this message in context: 
http://www.nabble.com/How-to--define-a-macro-constant---tp18187095p18187095.html
Sent from the Coq mailing list archive at Nabble.com.