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

Auxiliary function for instantiating the loose bound variables in e with args[start:stop]. This function is similar to instantiateRevRange, but it applies beta-reduction when we instantiate a bound variable with a lambda expression. Example: Given the term #0 a, and start := 0, stop := 1, args := #[fun x => x] the result is a instead of (fun x => x) a. This reduction is useful when we are inferring the type of eliminator-like applications. For example, given (n m : Nat) (f : Nat → Nat) (h : m = n), the type of Eq.subst (motive := fun x => f m = f x) h rfl is motive n which is (fun (x : Nat) => f m = f x) n This function reduces the new application to f m = f n

We use it to implement inferAppType

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

@[inline]

def Lean.Meta.withInferTypeConfig {α : Type} (x : MetaM α) : MetaM α

Ensure MetaM configuration is strong enough for inferring/checking types. For example, beta := true is essential when type checking.

Remark: we previously use the default configuration here, but this is problematic because it overrides unrelated configurations.

Equations

• One or more equations did not get rendered due to their size.

@[export lean_infer_type]

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

Equations

• Lean.Meta.inferTypeImp e = Lean.withIncRecDepth (Lean.Meta.withInferTypeConfig (Lean.Meta.inferTypeImp.infer e))

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.inferTypeImp.infer (Lean.Expr.const c []) = Lean.Meta.inferConstType✝ c []
• Lean.Meta.inferTypeImp.infer (Lean.Expr.const c us) = Lean.Meta.checkInferTypeCache✝ (Lean.Expr.const c us) (Lean.Meta.inferConstType✝ c us)
• Lean.Meta.inferTypeImp.infer (Lean.Expr.proj n i s) = Lean.Meta.checkInferTypeCache✝ (Lean.Expr.proj n i s) (Lean.Meta.inferProjType✝ n i s)
• Lean.Meta.inferTypeImp.infer (f.app arg) = Lean.Meta.checkInferTypeCache✝ (f.app arg) (Lean.Meta.inferAppType✝ f.getAppFn (f.app arg).getAppArgs)
• Lean.Meta.inferTypeImp.infer (Lean.Expr.mvar mvarId) = Lean.Meta.inferMVarType✝ mvarId
• Lean.Meta.inferTypeImp.infer (Lean.Expr.fvar fvarId) = Lean.Meta.inferFVarType✝ fvarId
• Lean.Meta.inferTypeImp.infer (Lean.Expr.bvar bidx) = Lean.throwError (Lean.toMessageData "unexpected bound variable " ++ Lean.toMessageData (Lean.mkBVar bidx) ++ Lean.toMessageData "")
• Lean.Meta.inferTypeImp.infer (Lean.Expr.mdata data e_2) = Lean.Meta.inferTypeImp.infer e_2
• Lean.Meta.inferTypeImp.infer (Lean.Expr.lit v) = pure v.type
• Lean.Meta.inferTypeImp.infer (Lean.Expr.sort lvl) = pure (Lean.mkSort (Lean.mkLevelSucc lvl))

partial def Lean.Meta.isPropQuick : Expr → MetaM LBool

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

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

isProp e returns 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.

partial def Lean.Meta.isProofQuick : Expr → MetaM LBool

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

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

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Meta.isTypeQuick : Expr → MetaM LBool

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

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

Return true iff the type of e is a Sort _.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.typeFormerTypeLevelQuick : Expr → Option Level

Equations

• Lean.Meta.typeFormerTypeLevelQuick (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Meta.typeFormerTypeLevelQuick b
• Lean.Meta.typeFormerTypeLevelQuick (Lean.Expr.sort l) = some l
• Lean.Meta.typeFormerTypeLevelQuick x✝ = none

def Lean.Meta.typeFormerTypeLevel (type : Expr) : MetaM (Option Level)

Return u iff type is Sort u or As → Sort u.

Equations

• Lean.Meta.typeFormerTypeLevel type = match Lean.Meta.typeFormerTypeLevelQuick type with | some l => pure (some l) | none => Lean.Meta.savingCache (Lean.Meta.typeFormerTypeLevel.go type #[])

partial def Lean.Meta.typeFormerTypeLevel.go (type : Expr) (xs : Array Expr) : MetaM (Option Level)

def Lean.Meta.isTypeFormerType (type : Expr) : MetaM Bool

Return true iff type is Sort _ or As → Sort _.

Equations

• Lean.Meta.isTypeFormerType type = do let __do_lift ← Lean.Meta.typeFormerTypeLevel type pure __do_lift.isSome

def Lean.Meta.isPropFormerType (type : Expr) : MetaM Bool

Return true iff type is Prop or As → Prop.

Equations

• Lean.Meta.isPropFormerType type = do let __do_lift ← Lean.Meta.typeFormerTypeLevel type pure (__do_lift == some Lean.Level.zero)

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

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

Equations

• Lean.Meta.isTypeFormer e = do let __do_lift ← Lean.Meta.inferType e Lean.Meta.isTypeFormerType __do_lift

def Lean.Meta.arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr)

Given n and a non-dependent function type α₁ → α₂ → ... → αₙ → Sort u, returns the types α₁, α₂, ..., αₙ. Throws an error if there are not at least n argument types or if a later argument type depends on a prior one (i.e., it's a dependent function type).

This can be used to infer the expected type of the alternatives when constructing a MatcherApp.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.inferArgumentTypesN (n : Nat) (e : Expr) : MetaM (Array Expr)

Infers the types of the next n parameters that e expects. See arrowDomainsN.

Equations

• Lean.Meta.inferArgumentTypesN n e = do let __do_lift ← Lean.Meta.inferType e Lean.Meta.arrowDomainsN n __do_lift