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

chore: normalize universe level

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-11 09:19:06 -08:00
parent 0358511121
commit 5dc1bbb188
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/Meta/InferType.lean
View file

@ -107,7 +107,7 @@ forallTelescope whnf e $ fun xs e => do
xTypeLvl ← getLevel whnf inferType xType;
pure $ Level.imax xTypeLvl lvl)
lvl;
pure $ Expr.sort lvl
pure $ Expr.sort lvl.normalize
/- Infer type of lambda and let expressions -/
@[specialize] private def inferLambdaType