The Coq mailing list

["Claudia Fernanda Oliveira K Tavares" <claudia AT consiste.dimap.ufrn.br>]

Hi!

I've received some examples to test in Coq, but they have some problem. I 
think that is a changing of syntax. 

-----------------------------------------------------------------
| Coq < Parameter plus_zero: (x:nat) (nat_plus x O) = x.
| Toplevel input, characters 22-23
| > Parameter plus_zero: (x:nat) (nat_plus x O) = x.
| >                       ^
| Error: The reference x was not found in the current environment
-------------------------------------------------------------------
 What's wrong?
 Thanks,

Cláudia.
--
Consiste/DIMAp (http://www.consiste.dimap.ufrn.br/)