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

fix(library/init/meta/simp_tactic): make sure replace_target does not fail due to reducibility settings

Browse source
This commit is contained in:
Leonardo de Moura 2017-05-23 21:43:37 -07:00
parent e163b5c884
commit bebdba1004
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/meta/simp_tactic.lean
View file

@ -245,9 +245,12 @@ do e_type ← infer_type e >>= whnf,
simplify_core cfg S `eq e
meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
do assert `htarget new_target, swap,
ht ← get_local `htarget,
mk_eq_mpr pr ht >>= exact
do t ← target,
assert `htarget new_target, swap,
ht ← get_local `htarget,
eq_type ← mk_app `eq [t, new_target],
locked_pr ← return $ expr.app (expr.app (expr.const ``id_locked [level.zero]) eq_type) pr,
mk_eq_mpr locked_pr ht >>= exact
meta def simplify_goal (S : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
do t ← target,