fix(init/meta/interactive): mk_simp_set: also remove equational lemmas

leanprover · Mar 24, 2017 · a11ee6b · a11ee6b
1 parent 028c0e6
commit a11ee6b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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