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

feat(library/init/meta/smt/smt_tactic): add smt_tactic.induction

Browse source 
Non-interactive version.
This commit is contained in:
Leonardo de Moura 2017-01-13 16:49:54 -08:00
parent 05d86e49ca
commit 6ebc23eca4
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/meta/smt/smt_tactic.lean
View file

@ -353,6 +353,9 @@ meta def add_lemmas_from_facts_core : list expr → smt_tactic unit
meta def add_lemmas_from_facts : smt_tactic unit :=
get_facts >>= add_lemmas_from_facts_core
meta def induction (e : expr) (rec : name) (ids : list name) : smt_tactic unit :=
slift (tactic.induction e rec ids)
end smt_tactic
open smt_tactic