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

fix: should only cache inferred type when there are no metavars

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-11 19:02:39 -07:00
parent 2694e7798a
commit 484a3a4e7c
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/Lean/Meta/InferType.lean
View file

@ -174,7 +174,8 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
| some type => pure type
| none =>
let type ← inferType
modifyInferTypeCache fun c => c.insert e type
unless e.hasMVar || type.hasMVar do
modifyInferTypeCache fun c => c.insert e type
pure type
def inferTypeImp (e : Expr) : MetaM Expr :=