coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Patrice Chalin<chalin AT ksu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] shorthand to add a lemma into context?
Date: Sat, 26 Nov 2011 19:03:01 +0100

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