coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] shorthand to add a lemma into context?

From: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>
To: Patrice Chalin <chalin AT ksu.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] shorthand to add a lemma into context?
Date: Sat, 26 Nov 2011 18:07:14 +0000

Hi Patrice,

The command you are looking for is :

assert (NAME := lem).

where NAME is a fresh name for your hypothesis.

Cheers,

--
guillaume

On 26 November 2011 18:03, Patrice Chalin
<chalin AT ksu.edu>
wrote:
> Hi,
>
> Given that the environment contains
>
> �Lemma lem: <long-formula>. Proof. ... Qed.
>
> I can add lem to the context of another proof by:
>
> �assert (<long-formula>) by apply lem.
>
> Is there a shorthand for this? �I know that I cannot write "assert lem"
> because
> lem names the proof. Maybe there is a "assert (type_of lem)" :) ?
>
> Thanks,
> Patrice
>

[Coq-Club] shorthand to add a lemma into context?, Patrice Chalin
- Re: [Coq-Club] shorthand to add a lemma into context?, gallais @ ensl.org
- Re: [Coq-Club] shorthand to add a lemma into context?, Daniel Schepler