From b3a0eb9bfc175bd0718c8645f66bb1db821ea2c9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 25 Mar 2017 00:55:25 +0100 Subject: [PATCH] fix(init/meta/interactive): mk_simp_set: also remove equational lemmas --- library/init/meta/interactive.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index ac81d25053..e5a4da127f 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -507,7 +507,9 @@ private meta def simp_lemmas.append_pexprs : simp_lemmas → list pexpr → tact private meta def mk_simp_set (attr_names : list name) (hs : list pexpr) (ex : list name) : tactic simp_lemmas := do s₀ ← join_user_simp_lemmas attr_names, s₁ ← simp_lemmas.append_pexprs s₀ hs, - return $ simp_lemmas.erase s₁ ex + -- add equational lemmas, if any + ex ← ex^.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n), + return $ simp_lemmas.erase s₁ $ ex^.join private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit | s := do