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

fix: preserve tag

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-21 19:06:54 -08:00
parent 09f504f376
commit 9abb749663
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Elab/Tactic/Generalize.lean
View file

@ -21,9 +21,10 @@ private def getVarName (stx : Syntax) : Name :=
(stx.getIdAt 4).eraseMacroScopes
private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
tag ← Meta.getMVarTag mvarId;
eType ← Meta.inferType e;
u ← Meta.getLevel eType;
mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target;
mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
let rfl := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
let val := mkApp2 mvar' e rfl;
Meta.assignExprMVar mvarId val;