Lukas Stevens (Aug 05 2020 at 11:27): Lukas Stevens (Aug 05 2020 at 11:27):Is there a tactic that fails if there are no premises and otherwise succeeds?
Manuel Eberl (Aug 05 2020 at 11:31):In Isabelle, I usually just write apply (my_tac; fail) if I expect my_tac to solve everything.
Manuel Eberl (Aug 05 2020 at 11:31):In ML, there is a SOLVED combinator.
Lukas Stevens (Aug 05 2020 at 11:32):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.
Manuel Eberl (Aug 05 2020 at 11:33):Err, it's called SOLVE
Manuel Eberl (Aug 05 2020 at 11:33):Oh, sorry, premises… no, I don't think so.
Manuel Eberl (Aug 05 2020 at 11:36):It should be easy enough to write one with Subgoal.FOCUS_PREMS though.
Manuel Eberl (Aug 05 2020 at 11:37):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: Nov 13 2025 at 04:27 UTC