Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] unload prelude?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unload prelude?


chronological Thread 
  • From: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
  • To: Thorsten Altenkirch <txa AT cs.nott.ac.uk>
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] unload prelude?
  • Date: Wed, 29 Oct 2008 16:48:20 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Oct 29, 2008 at 11:35:05AM +0000, Thorsten Altenkirch wrote:
>
> Section nat.
> 
> Inductive nat : Set :=
>   | O : nat
>   | S : nat -> nat.
> 
> Lemma O_S : forall n:nat, 0 <> S n.
> 

As Laurent already mentionned, beware of the "0" notation ...

> 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?
> 

I'm not aware of any "unload" feature, but you can indeed start coq
without its prelude, see the option -nois (meaning: no input state)
that both coqtop and coqide accept.

Of course, this way you start with precisely *nothing* in your
environment. You'll probably want at least some notion of equality
(as in the "<>" of your example) : you can either provide your own, 
or load some specific parts of the prelude, for example via a 
Require Import Logic.

Note that some advanced tactics may also be unusable since they may
need some objects of the prelude.

Best, 
Pierre Letouzey





Archive powered by MhonArc 2.6.16.

Top of Page