The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi,

for paedagogical reasons I would like to redefine parts of he prelude  
(using the same names) without clashing with the definitions in the  
prelude. E.g. I'd like to show the inductive definition of nat and  
then proceed proving things about it. E.g. I try

Section nat.

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Lemma O_S : forall n:nat, 0 <> S n.

and Coq complains:

The term "S n" has type "nat" while it is expected to have type
 "Datatypes.nat"

What would be the best way of achieving this. I guess I can run coq  
without the prelude, but this would require special instructions how  
to start Coq. Is there a way to "unload" the prelude (or parts of it)  
as part of a coq script?

Or is there any other advice how I could achieve my goal?

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.