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

feat(library/init/meta/interactive): add interactive done tactic

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-01 17:28:52 -07:00
parent 00aef04b81
commit 5446df1609
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/interactive.lean
View file

@ -849,5 +849,9 @@ tactic.by_contradiction >> return ()
meta def by_contra : tactic unit :=
tactic.by_contradiction >> return ()
/-- Fail if there are unsolved goals. -/
meta def done : tactic unit :=
tactic.done
end interactive
end tactic