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

fix: missing instantiateMVars

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-05 06:57:50 -08:00
parent dd0b71938d
commit 9715bc7738
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Lean/Meta/SynthInstance.lean
View file

@ -194,6 +194,7 @@ def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Wait
withMCtx mctx $ do
trace `Meta.synthInstance.newSubgoal $ fun _ => key;
mvarType ← inferType mvar;
mvarType ← instantiateMVars mvarType;
instances ← getInstances mvarType;
mctx ← getMCtx;
if instances.isEmpty then pure ()