Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] local definition in proof mode

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] local definition in proof mode


chronological Thread 
  • From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
  • To: andr� hirschowitz <ah AT unice.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] local definition in proof mode
  • Date: Tue, 6 Apr 2010 21:17:48 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:content-transfer-encoding :in-reply-to:user-agent; b=EMa+atEIHNESrVehjltETEhOSuedVIfj347TODrlm96M2rXV9rKTb6wUnwPOY9uTZk 01A+WFnfHEhRkI15U9PN5FyN0ejAYLHKPX3FZhgMIUtXR4XtkuxOu/cZHiqW2Ivejmok sy5/A07zIivic6RgyBcOqyTz4EtnkZxovPcXI=
On Tue, Apr 06, 2010 at 03:07:32PM +0200, andré hirschowitz wrote:
> Exactly. I just want to give a name to an awful term which I am unable to
> write although I am able to produce it in proof mode.
> 
> >
> > That makes me think of a maybe real solution, but I am not sure it works:
> > instead of a "pose (H := _ : P).", you should try a "Lemma H: P."
> >
> 
> No, this does not work because the local environment is not taken into
> account by this command (if my experiment is correct). Neither does
> Definition for the same reason.

An ugly option is to cut and past the current environment into a section.
Section ugly.
<paste here>
Definition... Defined.
End ugly.

JF


Archive powered by MhonArc 2.6.16.

Top of Page