coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- Evaluable constant, Michel Levy
- Re: Evaluable constant,
Xavier RIVAL
- Re: Evaluable constant, Eduardo Gimenez
- Re: Evaluable constant, Jean Goubault-Larrecq
- Re: Evaluable constant, Jean-Francois Monin
- Re: Evaluable constant,
Xavier RIVAL
Archive powered by MhonArc 2.6.16.