Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "conditional" ltacs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "conditional" ltacs


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] "conditional" ltacs
  • Date: Tue, 09 Jul 2013 16:31:28 -0400

On 07/09/2013 04:29 PM, t x wrote:
I want to write a ltac that says: "apply this lemma, if and only if the newly introduced goals can be solved by omega"

Perhaps [apply lemma; solve [ omega ] ]?



Archive powered by MHonArc 2.6.18.

Top of Page