Stream: Coq users

Topic: Getting number of goals


view this post on Zulip k32 (Jul 24 2020 at 21:55):

Hi! I have a somewhat weird testcase for a tactic, where I verify that it produces less than N goals, by using Fail Focus N. Abort.. But Focus command is deprecated, and although Fail N:{. Abort. does the job, it makes Emacs go crazy due to unbalanced braces. Is there a less hacky way to check the number of goals?

view this post on Zulip Paolo Giarrusso (Jul 24 2020 at 22:55):

There are numgoals and guard, and they are mentioned in the manual. For instance, see the following code:

Tactic Notation "nosplit" tactic3(tac) := tac; let n := numgoals in guard n = 1.

view this post on Zulip Paolo Giarrusso (Jul 24 2020 at 22:57):

After that, "nosplit foo" will run foo and fail if it produces more than one goal. I suspect you just need to adapt the argument of guard.

view this post on Zulip k32 (Jul 25 2020 at 08:33):

Thanks, this worked nicely.


Last updated: Feb 04 2023 at 21:02 UTC