From 6ebc23eca4302eeaf34e37ba07d57b9755d10e45 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jan 2017 16:49:54 -0800 Subject: [PATCH] feat(library/init/meta/smt/smt_tactic): add smt_tactic.induction Non-interactive version. --- library/init/meta/smt/smt_tactic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index 4c8a2c8a17..373a9e3f53 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -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