The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Hello,

The obvious way of expressing such things in a rightly typed
language, i.e. WITH SUMS (e.g. as in the ML or Haskell family,
and of course in Coq, Agda, LEGO etc.) is to use this feature.

Inductive month : Set := 
  | Jan : month
  | Feb : month
  | ...
  | Dec : month.

Definition next_month (n:month) :=
  match n with
    Jan => Feb
    |  ...
  end.

Encoding everything with integers in C style is always possible
but quite weird. May be you have good reasons to proceed this way?

Regards,
  JF

On Sun, Jun 29, 2008 at 05:51:06PM -0700, gang chen wrote:
> 
> 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.
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46