k32 (Jul 24 2020 at 21:55): 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?
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.
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.
k32 (Jul 25 2020 at 08:33):Thanks, this worked nicely.
Last updated: Oct 01 2023 at 18:01 UTC