Is there a tactic that fails if there are no premises and otherwise succeeds?
In Isabelle, I usually just write
apply (my_tac; fail) if I expect
my_tac to solve everything.
In ML, there is a
But there being no premises does not mean that the goal is solved. To the contrary in my case, it means that my tactic cannot do anything.
Err, it's called
Oh, sorry, premises… no, I don't think so.
It should be easy enough to write one with
If it has to be fast, it might be better to write a tactic that directly examines the tactic state (using e.g.
COND) without going through
Subgoal.FOCUS_PREMS. Although Makarius might frown on that.
Last updated: Sep 25 2021 at 08:21 UTC