# Documentation

Lean.Meta.InferType

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

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)→ 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 : Nat) (stop : Nat) (args : ) (e : Lean.Expr) (offset : Nat) :
def Lean.Meta.throwIncorrectNumberOfLevels {α : Type} (constName : Lean.Name) (us : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
@[export lean_infer_type]
Equations
Equations
partial def Lean.Meta.isPropQuick :

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

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.

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

Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Meta.isTypeQuick :

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

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

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

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

Equations
partial def Lean.Meta.isTypeFormerType.go (type : Lean.Expr) (xs : ) :

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

Equations