Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tactic for detecting that there is a goal left?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic for detecting that there is a goal left?


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Tactic for detecting that there is a goal left?
  • Date: Fri, 13 Jun 2014 16:34:22 +0100

It doesn't actually work for the same reason "idtac; []" doesn't work; it fails with "Not enough subgoals" if you have no goals left.  The "bug" is that some things, like square brackets, have special behavior with respect to semicolons, which are lost if you stick them inside a tactic.

-Jason


On Fri, Jun 13, 2014 at 4:31 PM, Jonathan <jonikelee AT gmail.com> wrote:
On 06/13/2014 11:25 AM, Jonathan wrote:
How about:

idtac; [idtac|fail..].

Oh - that doesn't work when defined as a tactic, but does if it's inlined.  Weird.  How can that not be a bug?



On 06/13/2014 11:16 AM, Jason Gross wrote:
Actually, my [at_most_one_goal_left] tactic doesn't work.  Is there a way
to detect "zero or one goals"?


On Fri, Jun 13, 2014 at 4:11 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,
Is there a standard way of asking the question "are all goals solved?" and
"is there at most one goal left?" in Ltac?

I can use "; solve [ idtac ]" to mean "fail if there are any goals left",
and I have been using "; []" to detect "exactly one goal left", and and I
can define a tactic
   Ltac at_most_one_goal_left := idtac; [].
so that "; at_most_one_goal_left" will fail if there is more than one
goal.  But is seems poor that inlining a tactic definition changes its
behavior; am I simply exploiting a bug?

-Jason







Archive powered by MHonArc 2.6.18.

Top of Page