coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Saving proofs?

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Saving proofs?
Date: Mon, 20 Dec 2004 11:24:55 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Mon, Dec 20, 2004 at 08:55:56AM +0100, Wojciech Moczydlowski wrote:

> I have a question regarding saving proofs in Coq, namely, how to do it.
> That is, I would like to be able to do the following (in coqtop).
> 1. State some lemma.
> 2. Prove it (using coqtop).
> 3. Somehow save the proof (and lemma) so that next time I can proceed with
> the development with the lemma proved.

I recommend using some kind of interface to Coq: CoqIDE (comes in the
Coq sources) or Proof General (http://proofgeneral.inf.ed.ac.uk/).

--
Lionel

[Coq-Club] Saving proofs?, Wojciech Moczydlowski
- Re: [Coq-Club] Saving proofs?, Pierre Casteran
- Re: [Coq-Club] Saving proofs?, Lionel Elie Mamane
- Re: [Coq-Club] Saving proofs?, pcourtie