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

perf: cache inferConstType

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-21 15:48:36 -08:00
parent 50b6561f8f
commit 322fc79d84
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

@ -179,7 +179,8 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
def inferTypeImp (e : Expr) : MetaM Expr :=
let rec infer : Expr → MetaM Expr
| Expr.const c lvls _ => inferConstType c lvls
| Expr.const c [] _ => inferConstType c []
| Expr.const c us _ => checkInferTypeCache e (inferConstType c us)
| e@(Expr.proj n i s _) => checkInferTypeCache e (inferProjType n i s)
| e@(Expr.app f _ _) => checkInferTypeCache e (inferAppType f.getAppFn e.getAppArgs)
| Expr.mvar mvarId _ => inferMVarType mvarId