Skip to Content.
Sympa Menu

coq-club - Re: Evaluable constant

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Evaluable constant


chronological Thread 
  • From: Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>
  • To: Michel Levy <Michel.Levy AT imag.fr>
  • Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
  • Subject: Re: Evaluable constant
  • Date: Tue, 09 Oct 2001 09:56:35 +0200
  • Organization: LSV, ENS Cachan

Michel Levy wrote:
> 
> Could you explain me what is an evaluable constant, more exactly, why I

        Xavier is right.  Another possibility
is to end your proof using the 'Defined' keyword
instead of 'Save' or 'Qed'.  This makes the
proof transparent.

        -- Jean.





Archive powered by MhonArc 2.6.16.

Top of Page