The Coq mailing list

[gang chen <gangchen_sh AT yahoo.com>]

Hello,

Thanks for both replies. 
Yes, I do need C-style macro constants in order to achieve flexibility.

Best regards,

gang chen


Jean-Francois Monin wrote:
> 
> 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
> 
> --------------------------------------------------------
> 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
> 
> 

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