coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr
Cc: Patrice Chalin <chalin AT ksu.edu>
Subject: Re: [Coq-Club] shorthand to add a lemma into context?
Date: Sat, 26 Nov 2011 10:14:04 -0800

On Saturday, November 26, 2011 10:03:01 AM Patrice Chalin 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)" :) ?

pose proof lem.
--
Daniel Schepler

[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