Documentation

Lean.Meta.InferType

source
def Lean.Expr.instantiateBetaRevRange (e : Lean.Expr) (start : Nat) (stop : Nat) (args : Array Lean.Expr) :
Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
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
source
def Lean.Meta.throwIncorrectNumberOfLevels {α : Type} (constName : Lean.Name) (us : List Lean.Level) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.throwTypeExcepted {α : Type} (type : Lean.Expr) :
Lean.MetaM α
Equations
source
def Lean.Meta.getLevel (type : Lean.Expr) :
Lean.MetaM Lean.Level
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.throwUnknownMVar {α : Type} (mvarId : Lean.MVarId) :
Lean.MetaM α
Equations
source
@[export lean_infer_type]
def Lean.Meta.inferTypeImp (e : Lean.Expr) :
Lean.MetaM Lean.Expr
Equations
source
def Lean.Meta.inferTypeImp.infer (e : Lean.Expr) :
Lean.Expr → Lean.MetaM Lean.Expr
Equations
source
partial def Lean.Meta.isPropQuick:
Lean.Expr → Lean.MetaM Lean.LBool

isPropQuick e is an "approximate" predicate which returns LBool.true if e is a proposition.

source
def Lean.Meta.isProp (e : Lean.Expr) :
Lean.MetaM Bool

isProp whnf e return true if e is a proposition.

 If `e` contains metavariables, it may not be possible
 to decide whether is a proposition or not. We return `false` in this
 case. We considered using `LBool` and retuning `LBool.undef`, but
 we have no applications for it.
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.isProofQuick:
Lean.Expr → Lean.MetaM Lean.LBool

isProofQuick e is an "approximate" predicate which returns LBool.true if e is a proof.

source
def Lean.Meta.isProof (e : Lean.Expr) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.isTypeQuick:
Lean.Expr → Lean.MetaM Lean.LBool

isTypeQuick e is an "approximate" predicate which returns LBool.true if e is a type.

source
def Lean.Meta.isType (e : Lean.Expr) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.isTypeFormerType (type : Lean.Expr) :
Lean.MetaM Bool
source
def Lean.Meta.isTypeFormer (e : Lean.Expr) :
Lean.MetaM Bool

Return true iff e : Sort _ or e : (forall As, Sort _). Remark: it subsumes isType

Equations