Lean.Meta.InferType

def Lean.Expr.instantiateBetaRevRange (e : Lean.Expr) (start : Nat) (stop : Nat) (args : Array Lean.Expr) :

Equations

Lean.Expr.instantiateBetaRevRange e start stop args = (fun visit => if (Lean.Expr.hasLooseBVars e && decide (stop > start)) = true then if stop ≤ Array.size args then Lean.MonadStateCacheT.run (visit e 0) else panicWithPosWithDecl "Lean.Meta.InferType" "Lean.Expr.instantiateBetaRevRange" 27 4 ("assertion violation: " ++ "stop ≤ args.size\n ") else e) (Lean.Expr.instantiateBetaRevRange.visit start stop args)

partial def Lean.Expr.instantiateBetaRevRange.visit (start : Nat) (stop : Nat) (args : Array Lean.Expr) (e : Lean.Expr) (offset : Nat) :

Lean.MonadStateCacheT (Lean.ExprStructEq × Nat) Lean.Expr Id Lean.Expr

source

def Lean.Meta.throwFunctionExpected {α : Type} (f : Lean.Expr) :

Lean.MetaM α

Equations

Lean.Meta.throwFunctionExpected f = Lean.throwError (Lean.toMessageData "function expected" ++ Lean.toMessageData (Lean.indentExpr f) ++ Lean.toMessageData "")

source

def Lean.Meta.throwIncorrectNumberOfLevels {α : Type} (constName : Lean.Name) (us : List Lean.Level) :

Lean.MetaM α

Equations

Lean.Meta.throwIncorrectNumberOfLevels constName us = Lean.throwError (Lean.toMessageData "incorrect number of universe levels " ++ Lean.toMessageData (Lean.mkConst constName us) ++ Lean.toMessageData "")

source

def Lean.Meta.throwTypeExcepted {α : Type} (type : Lean.Expr) :

Lean.MetaM α

Equations

Lean.Meta.throwTypeExcepted type = Lean.throwError (Lean.toMessageData "type expected" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "")

source

def Lean.Meta.getLevel (type : Lean.Expr) :

Lean.MetaM Lean.Level

Equations

Lean.Meta.getLevel type = do let typeType ← Lean.Meta.inferType type let typeType ← Lean.Meta.whnfD typeType match typeType with | Lean.Expr.sort lvl x => pure lvl | Lean.Expr.mvar mvarId x => do let a ← Lean.Meta.isReadOnlyOrSyntheticOpaqueExprMVar mvarId if a = true then Lean.Meta.throwTypeExcepted type else do let lvl ← Lean.Meta.mkFreshLevelMVar Lean.Meta.assignExprMVar mvarId (Lean.mkSort lvl) pure lvl | x => Lean.Meta.throwTypeExcepted type

source

def Lean.Meta.throwUnknownMVar {α : Type} (mvarId : Lean.MVarId) :

Lean.MetaM α

Equations

Lean.Meta.throwUnknownMVar mvarId = Lean.throwError (Lean.toMessageData "unknown metavariable '?" ++ Lean.toMessageData mvarId.name ++ Lean.toMessageData "'")

source

def Lean.Meta.inferTypeImp (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.inferTypeImp e = (fun infer => Lean.withIncRecDepth (Lean.Meta.withTransparency Lean.Meta.TransparencyMode.default (infer e))) (Lean.Meta.inferTypeImp.infer e)

source

def Lean.Meta.inferTypeImp.infer (e : Lean.Expr) :

Lean.Expr → Lean.MetaM Lean.Expr

Equations

Lean.Meta.inferTypeImp.infer e (Lean.Expr.const c [] x_1) = Lean.Meta.inferConstType c []
Lean.Meta.inferTypeImp.infer e (Lean.Expr.const c us x_1) = Lean.Meta.checkInferTypeCache e (Lean.Meta.inferConstType c us)
Lean.Meta.inferTypeImp.infer e (Lean.Expr.proj n i s x_1) = Lean.Meta.checkInferTypeCache (Lean.Expr.proj n i s x_1) (Lean.Meta.inferProjType n i s)
Lean.Meta.inferTypeImp.infer e (Lean.Expr.app f x_1 x_2) = Lean.Meta.checkInferTypeCache (Lean.Expr.app f x_1 x_2) (Lean.Meta.inferAppType (Lean.Expr.getAppFn f) (Lean.Expr.getAppArgs (Lean.Expr.app f x_1 x_2)))
Lean.Meta.inferTypeImp.infer e (Lean.Expr.mvar mvarId x_1) = Lean.Meta.inferMVarType mvarId
Lean.Meta.inferTypeImp.infer e (Lean.Expr.fvar fvarId x_1) = Lean.Meta.inferFVarType fvarId
Lean.Meta.inferTypeImp.infer e (Lean.Expr.bvar bidx x_1) = Lean.throwError (Lean.toMessageData "unexpected bound variable " ++ Lean.toMessageData (Lean.mkBVar bidx) ++ Lean.toMessageData "")
Lean.Meta.inferTypeImp.infer e (Lean.Expr.mdata x_1 e_1 x_2) = Lean.Meta.inferTypeImp.infer e e_1
Lean.Meta.inferTypeImp.infer e (Lean.Expr.lit v x_1) = pure (Lean.Literal.type v)
Lean.Meta.inferTypeImp.infer e (Lean.Expr.sort lvl x_1) = pure (Lean.mkSort (Lean.mkLevelSucc lvl))
Lean.Meta.inferTypeImp.infer e (Lean.Expr.forallE x_1 x_2 x_3 x_4) = Lean.Meta.checkInferTypeCache (Lean.Expr.forallE x_1 x_2 x_3 x_4) (Lean.Meta.inferForallType (Lean.Expr.forallE x_1 x_2 x_3 x_4))
Lean.Meta.inferTypeImp.infer e (Lean.Expr.lam x_1 x_2 x_3 x_4) = Lean.Meta.checkInferTypeCache (Lean.Expr.lam x_1 x_2 x_3 x_4) (Lean.Meta.inferLambdaType (Lean.Expr.lam x_1 x_2 x_3 x_4))
Lean.Meta.inferTypeImp.infer e (Lean.Expr.letE x_1 x_2 x_3 x_4 x_5) = Lean.Meta.checkInferTypeCache (Lean.Expr.letE x_1 x_2 x_3 x_4 x_5) (Lean.Meta.inferLambdaType (Lean.Expr.letE x_1 x_2 x_3 x_4 x_5))

source

partial def Lean.Meta.isPropQuick :

Lean.Expr → Lean.MetaM Lean.LBool

source

def Lean.Meta.isProp (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.isProp e = do let r ← Lean.Meta.isPropQuick e match r with | Lean.LBool.true => pure true | Lean.LBool.false => pure false | Lean.LBool.undef => do let type ← Lean.Meta.inferType e let type ← Lean.Meta.whnfD type match type with | Lean.Expr.sort u x => do let a ← Lean.Meta.instantiateLevelMVars u pure (Lean.Meta.isAlwaysZero a) | x => pure false

source

partial def Lean.Meta.isProofQuick :

Lean.Expr → Lean.MetaM Lean.LBool

source

def Lean.Meta.isProof (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.isProof e = do let r ← Lean.Meta.isProofQuick e match r with | Lean.LBool.true => pure true | Lean.LBool.false => pure false | Lean.LBool.undef => do let type ← Lean.Meta.inferType e Lean.Meta.isProp type

source

partial def Lean.Meta.isTypeQuick :

Lean.Expr → Lean.MetaM Lean.LBool

source

def Lean.Meta.isType (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.isType e = do let r ← Lean.Meta.isTypeQuick e match r with | Lean.LBool.true => pure true | Lean.LBool.false => pure false | Lean.LBool.undef => do let type ← Lean.Meta.inferType e let type ← Lean.Meta.whnfD type match type with | Lean.Expr.sort x x_1 => pure true | x => pure false

source

partial def Lean.Meta.isTypeFormerType (type : Lean.Expr) :

Lean.MetaM Bool

source

def Lean.Meta.isTypeFormer (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.isTypeFormer e = do let type ← Lean.Meta.inferType e Lean.Meta.isTypeFormerType type