max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta/tactic): add 'now' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-17 16:15:32 -07:00
parent b21a3376e0
commit ee888e9872
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/tactic.lean
View file

@ -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