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

fix: preserve tags in simp conv

Browse source
This commit is contained in:
Mario Carneiro 2022-09-27 19:52:22 -04:00 • committed by Leonardo de Moura
parent 2a748d3035
commit db110f5dfe
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/Tactic/Conv/Basic.lean
View file

@ -73,9 +73,10 @@ def getRhs : TacticM Expr :=
/-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`. -/
def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
let mvarId ← getMainGoal
let rhs ← getRhs
let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoalRaw (← mkEq lhs' rhs))
(← getMainGoal).assign (← mkEqTrans h newGoal)
let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoalRaw (← mkEq lhs' rhs)) (← mvarId.getTag)
mvarId.assign (← mkEqTrans h newGoal)
replaceMainGoal [newGoal.mvarId!]
/-- Replace `lhs` with the definitionally equal `lhs'`. -/