diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 06676e4c83..ae87320366 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -202,4 +202,9 @@ meta_definition all_goals (tac : tactic unit) : tactic unit := do gs ← get_goals, all_goals_core tac gs [] +meta_definition now : tactic unit := +do n ← num_goals, + if n = 0 then skip + else fail "now tactic failed, there are unsolved goals" + end tactic