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

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

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-25 00:55:25 +01:00 • committed by Leonardo de Moura
parent c7b47c7b7f
commit b3a0eb9bfc
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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