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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-18 15:18:20 -07:00
parent 839f1e1ec8
commit 43bc429abf
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/Replace.lean
View file

@ -25,8 +25,8 @@ withMVarContext mvarId do
u ← getLevel target;
eq ← mkEq target targetNew;
newProof ← mkExpectedTypeHint eqProof eq;
let newVal := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
assignExprMVar mvarId mvarNew;
let val := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
assignExprMVar mvarId val;
pure mvarNew.mvarId!
/--