coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] unload prelude?, Thorsten Altenkirch
- Re: [Coq-Club] unload prelude?, Thery Laurent
- Re: [Coq-Club] unload prelude?, Pierre Letouzey
- Re: [Coq-Club] unload prelude?,
Thorsten Altenkirch
- Re: [Coq-Club] unload prelude?, Pierre Letouzey
- Re: [Coq-Club] unload prelude?,
Thorsten Altenkirch
Archive powered by MhonArc 2.6.16.