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

fix: assignDelayed misuse at intro

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-16 20:09:27 -08:00
parent 5a1221c491
commit 8f59d4a9e6
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/Meta/Tactic/Intro.lean
View file

@ -18,7 +18,8 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
withNewLocalInstances isClassExpensive fvars j $ do
newMVar ← mkFreshExprSyntheticOpaqueMVar type;
lctx ← getLCtx;
modify $ fun s => { mctx := s.mctx.assignDelayed mvarId lctx fvars newMVar, .. s };
newVal ← mkLambda fvars newMVar;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
pure $ (fvars, newMVar.mvarId!)
| (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do
let type := type.instantiateRevRange j fvars.size fvars;