The Coq mailing list

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

Thank you & Laurent & Georges (in private) for you helpful comments.

I guess I was looking for something like

Reset Initial "-nois"

available as a vernacular command. But this doesn't seem to exist.

I guess I'll get away with redefining the prelude and taking care of  
the notational expansion.

Cheers,
Thorsten

On 29 Oct 2008, at 15:48, Pierre Letouzey wrote:

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


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.