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

feat: add inferLambdaType

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-09 20:33:29 -08:00
parent c44517c876
commit cff9e4192d
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/Init/Lean/Meta.lean
View file

@ -544,6 +544,14 @@ forallTelescope whnf e $ fun xs e => do
lvl;
pure $ Expr.sort lvl
@[specialize] private def inferLambdaType
(whnf : Expr → MetaM Expr)
(inferType : Expr → MetaM Expr)
(e : Expr) : MetaM Expr :=
lambdaTelescope whnf e $ fun xs e => do
type ← inferType e;
mkForall xs type
@[inline] private def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
savingCache $ do
fvarId ← mkFreshId;
@ -583,8 +591,8 @@ do s ← get;
| Expr.mdata _ e => inferTypeAux e
| Expr.lit v => pure v.type
| Expr.sort lvl => pure $ Expr.sort (Level.succ lvl)
| e@(Expr.forallE _ _ _ _) => inferForallType whnf inferTypeAux e
| Expr.lam n bi d b => throw $ Exception.other "not implemented yet"
| e@(Expr.forallE _ _ _ _) => checkInferTypeCache e (inferForallType whnf inferTypeAux e)
| e@(Expr.lam _ _ _ _) => checkInferTypeCache e (inferLambdaType whnf inferTypeAux e)
| Expr.letE n t v b => throw $ Exception.other "not implemented yet"
#exit