inductive Lean.Literal : Type

Literal values for Expr.

• natVal (val : Nat) : Literal

  Natural number literal

• strVal (val : String) : Literal

  String literal

@[implicit_reducible]

instance Lean.instInhabitedLiteral : Inhabited Literal

def Lean.instInhabitedLiteral.default : Literal

def Lean.instBEqLiteral.beq : Literal → Literal → Bool

@[implicit_reducible]

instance Lean.instBEqLiteral : BEq Literal

@[implicit_reducible]

instance Lean.instReprLiteral : Repr Literal

def Lean.instReprLiteral.repr : Literal → Nat → Format

def Lean.Literal.hash : Literal → UInt64

@[implicit_reducible]

instance Lean.instHashableLiteral : Hashable Literal

def Lean.Literal.lt : Literal → Literal → Bool

Total order on Expr literal values. Natural number values are smaller than string literal values.

@[implicit_reducible]

instance Lean.instLTLiteral : LT Literal

@[implicit_reducible]

instance Lean.instDecidableLtLiteral (a b : Literal) : Decidable (a < b)

inductive Lean.BinderInfo : Type

Arguments in forallE binders can be labelled as implicit or explicit.

Each lam or forallE binder comes with a binderInfo argument (stored in ExprData). This can be set to

• default -- (x : α)
• implicit -- {x : α}
• strict_implicit -- ⦃x : α⦄
• inst_implicit -- [x : α].
• aux_decl -- Auxiliary definitions are helper methods that Lean generates. aux_decl is used for _match, _fun_match, _let_match and the self reference that appears in recursive pattern matching.

The difference between implicit {} and strict-implicit ⦃⦄ is how implicit arguments are treated that are not followed by explicit arguments. {} arguments are applied eagerly, while ⦃⦄ arguments are left partially applied:

def foo {x : Nat} : Nat := x
def bar ⦃x : Nat⦄ : Nat := x
#check foo -- foo : Nat
#check bar -- bar : ⦃x : Nat⦄ → Nat

See also the Lean Language Reference.

• default : BinderInfo

  Default binder annotation, e.g. (x : α)

• implicit : BinderInfo

  Implicit binder annotation, e.g., {x : α}

• strictImplicit : BinderInfo

  Strict implicit binder annotation, e.g., {{ x : α }}

• instImplicit : BinderInfo

  Local instance binder annotation, e.g., [Decidable α]

@[implicit_reducible]

instance Lean.instInhabitedBinderInfo : Inhabited BinderInfo

def Lean.instInhabitedBinderInfo.default : BinderInfo

@[implicit_reducible]

instance Lean.instBEqBinderInfo : BEq BinderInfo

def Lean.instBEqBinderInfo.beq : BinderInfo → BinderInfo → Bool

@[implicit_reducible]

instance Lean.instReprBinderInfo : Repr BinderInfo

def Lean.instReprBinderInfo.repr : BinderInfo → Nat → Format

def Lean.BinderInfo.hash : BinderInfo → UInt64

def Lean.BinderInfo.isExplicit : BinderInfo → Bool

Return true if the given BinderInfo does not correspond to an implicit binder annotation (i.e., implicit, strictImplicit, or instImplicit).

@[implicit_reducible]

instance Lean.instHashableBinderInfo : Hashable BinderInfo

def Lean.BinderInfo.isInstImplicit : BinderInfo → Bool

Return true if the given BinderInfo is an instance implicit annotation (e.g., [Decidable α])

def Lean.BinderInfo.isImplicit : BinderInfo → Bool

Return true if the given BinderInfo is a regular implicit annotation (e.g., {α : Type u})

def Lean.BinderInfo.isStrictImplicit : BinderInfo → Bool

Return true if the given BinderInfo is a strict implicit annotation (e.g., {{α : Type u}})

@[reducible, inline]

abbrev Lean.MData : Type

Expression metadata. Used with the Expr.mdata constructor.

@[reducible, inline]

abbrev Lean.MData.empty : MData

def Lean.Expr.Data : Type

Cached hash code, cached results, and other data for Expr.

• hash : 32-bits
• approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
• hasFVar : 1-bit -- does it contain free variables?
• hasExprMVar : 1-bit -- does it contain metavariables?
• hasLevelMVar : 1-bit -- does it contain level metavariables?
• hasLevelParam : 1-bit -- does it contain level parameters?
• looseBVarRange : 20-bits

Remark: this is mostly an internal datastructure used to implement Expr, most will never have to use it.

@[implicit_reducible]

instance Lean.instInhabitedData_1 : Inhabited Expr.Data

def Lean.Expr.Data.hash (c : Data) : UInt64

@[implicit_reducible]

instance Lean.instBEqData_1 : BEq Expr.Data

def Lean.Expr.Data.approxDepth (c : Data) : UInt8

def Lean.Expr.Data.looseBVarRange (c : Data) : UInt32

def Lean.Expr.Data.hasFVar (c : Data) : Bool

def Lean.Expr.Data.hasExprMVar (c : Data) : Bool

def Lean.Expr.Data.hasLevelMVar (c : Data) : Bool

def Lean.Expr.Data.hasLevelParam (c : Data) : Bool

@[extern lean_uint8_to_uint64]

def Lean.BinderInfo.toUInt64 : BinderInfo → UInt64

@[extern lean_expr_mk_data]

opaque Lean.Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Data

@[extern lean_expr_mk_app_data]

opaque Lean.Expr.mkAppData (fData aData : Data) : Data

Optimized version of Expr.mkData for applications.

@[inline]

def Lean.Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) : Data

@[inline]

def Lean.Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) : Data

@[implicit_reducible]

instance Lean.instReprData_1 : Repr Expr.Data

structure Lean.FVarId : Type

The unique free variable identifier. It is just a hierarchical name, but we wrap it in FVarId to make sure they don't get mixed up with MVarId.

This is not the user-facing name for a free variable. This information is stored in the local context (LocalContext). The unique identifiers are generated using a NameGenerator.

• name : Name

@[implicit_reducible]

instance Lean.instInhabitedFVarId : Inhabited FVarId

def Lean.instInhabitedFVarId.default : FVarId

def Lean.instBEqFVarId.beq : FVarId → FVarId → Bool

@[implicit_reducible]

instance Lean.instBEqFVarId : BEq FVarId

def Lean.instHashableFVarId.hash : FVarId → UInt64

@[implicit_reducible]

instance Lean.instHashableFVarId : Hashable FVarId

@[implicit_reducible]

instance Lean.instReprFVarId : Repr FVarId

def Lean.FVarIdSet : Type

A set of unique free variable identifiers. This is a persistent data structure implemented using Std.TreeSet.

@[implicit_reducible]

instance Lean.instInhabitedFVarIdSet : Inhabited FVarIdSet

@[implicit_reducible]

instance Lean.instEmptyCollectionFVarIdSet : EmptyCollection FVarIdSet

@[implicit_reducible]

instance Lean.instSingletonFVarIdFVarIdSet : Singleton FVarId FVarIdSet

@[implicit_reducible]

instance Lean.instForInFVarIdSetFVarIdOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m FVarIdSet FVarId

def Lean.FVarIdSet.insert (s : FVarIdSet) (fvarId : FVarId) : FVarIdSet

def Lean.FVarIdSet.union (vs₁ vs₂ : FVarIdSet) : FVarIdSet

def Lean.FVarIdSet.ofList (l : List FVarId) : FVarIdSet

def Lean.FVarIdSet.ofArray (l : Array FVarId) : FVarIdSet

def Lean.FVarIdHashSet : Type

A set of unique free variable identifiers implemented using hashtables. Hashtables are faster than red-black trees if they are used linearly. They are not persistent data-structures.

@[implicit_reducible]

instance Lean.instInhabitedFVarIdHashSet : Inhabited FVarIdHashSet

@[implicit_reducible]

instance Lean.instEmptyCollectionFVarIdHashSet : EmptyCollection FVarIdHashSet

def Lean.FVarIdMap (α : Type) : Type

A mapping from free variable identifiers to values of type α. This is a persistent data structure implemented using Std.TreeMap.

def Lean.FVarIdMap.insert {α : Type} (s : FVarIdMap α) (fvarId : FVarId) (a : α) : FVarIdMap α

@[implicit_reducible]

instance Lean.instEmptyCollectionFVarIdMap {α : Type} : EmptyCollection (FVarIdMap α)

@[implicit_reducible]

instance Lean.instInhabitedFVarIdMap {α : Type} : Inhabited (FVarIdMap α)

structure Lean.MVarId : Type

Universe metavariable Id

• name : Name

def Lean.instInhabitedMVarId.default : MVarId

@[implicit_reducible]

instance Lean.instInhabitedMVarId : Inhabited MVarId

@[implicit_reducible]

instance Lean.instBEqMVarId : BEq MVarId

def Lean.instBEqMVarId.beq : MVarId → MVarId → Bool

def Lean.instHashableMVarId.hash : MVarId → UInt64

@[implicit_reducible]

instance Lean.instHashableMVarId : Hashable MVarId

@[implicit_reducible]

instance Lean.instReprMVarId : Repr MVarId

def Lean.MVarIdSet : Type

@[implicit_reducible]

instance Lean.instInhabitedMVarIdSet : Inhabited MVarIdSet

@[implicit_reducible]

instance Lean.instEmptyCollectionMVarIdSet : EmptyCollection MVarIdSet

def Lean.MVarIdSet.insert (s : MVarIdSet) (mvarId : MVarId) : MVarIdSet

def Lean.MVarIdSet.ofList (l : List MVarId) : MVarIdSet

def Lean.MVarIdSet.ofArray (l : Array MVarId) : MVarIdSet

@[implicit_reducible]

instance Lean.instForInMVarIdSetMVarIdOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m MVarIdSet MVarId

def Lean.MVarIdMap (α : Type) : Type

def Lean.MVarIdMap.insert {α : Type} (s : MVarIdMap α) (mvarId : MVarId) (a : α) : MVarIdMap α

@[implicit_reducible]

instance Lean.instEmptyCollectionMVarIdMap {α : Type} : EmptyCollection (MVarIdMap α)

@[implicit_reducible]

instance Lean.instForInMVarIdMapProdMVarIdOfMonad {m : Type u_1 → Type u_2} {α : Type} [Monad m] : ForIn m (MVarIdMap α) (MVarId × α)

@[implicit_reducible]

instance Lean.instInhabitedMVarIdMap {α : Type} : Inhabited (MVarIdMap α)

@[extern lean_expr_data]

noncomputable def Lean.Expr.data : Expr → Data

inductive Lean.Expr : Type

Lean expressions. This data structure is used in the kernel and elaborator. However, expressions sent to the kernel should not contain metavariables.

Remark: we use the E suffix (short for Expr) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use.

• bvar (deBruijnIndex : Nat) : Expr

  The bvar constructor represents bound variables, i.e. occurrences of a variable in the expression where there is a variable binder above it (i.e. introduced by a lam, forallE, or letE).

  The deBruijnIndex parameter is the de-Bruijn index for the bound variable. See the Wikipedia page on de-Bruijn indices for additional information.

  For example, consider the expression fun x : Nat => forall y : Nat, x = y. The x and y variables in the equality expression are constructed using bvar and bound to the binders introduced by the earlier lam and forallE constructors. Here is the corresponding Expr representation for the same expression:

  .lam `x (.const `Nat [])
    (.forallE `y (.const `Nat [])
      (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
      .default)
    .default
  

• fvar (fvarId : FVarId) : Expr

  The fvar constructor represent free variables. These free variable occurrences are not bound by an earlier lam, forallE, or letE constructor and its binder exists in a local context only.

  Note that Lean uses the locally nameless approach. See McBride and McKinna for additional details.

  When "visiting" the body of a binding expression (i.e. lam, forallE, or letE), bound variables are converted into free variables using a unique identifier, and their user-facing name, type, value (for LetE), and binder annotation are stored in the LocalContext.

• mvar (mvarId : MVarId) : Expr

  Metavariables are used to represent "holes" in expressions, and goals in the tactic framework. Metavariable declarations are stored in the MetavarContext. Metavariables are used during elaboration, and are not allowed in the kernel, or in the code generator.

• sort (u : Level) : Expr

  Used for Type u, Sort u, and Prop:

  • Prop is represented as .sort .zero,
  • Sort u as .sort (.param `u), and
  • Type u as .sort (.succ (.param `u))
• const (declName : Name) (us : List Level) : Expr

  A (universe polymorphic) constant that has been defined earlier in the module or by another imported module. For example, @Eq.{1} is represented as Expr.const `Eq [.succ .zero], and @Array.map.{0, 0} is represented as Expr.const `Array.map [.zero, .zero].

• app (fn arg : Expr) : Expr

  A function application.

  For example, the natural number one, i.e. Nat.succ Nat.zero is represented as Expr.app (.const `Nat.succ []) (.const .zero []). Note that multiple arguments are represented using partial application.

  For example, the two argument application f x y is represented as Expr.app (.app f x) y.

• lam (binderName : Name) (binderType body : Expr) (binderInfo : BinderInfo) : Expr

  A lambda abstraction (aka anonymous functions). It introduces a new binder for variable x in scope for the lambda body.

  For example, the expression fun x : Nat => x is represented as

  Expr.lam `x (.const `Nat []) (.bvar 0) .default
  

• forallE (binderName : Name) (binderType body : Expr) (binderInfo : BinderInfo) : Expr

  A dependent arrow (a : α) → β) (aka forall-expression) where β may dependent on a. Note that this constructor is also used to represent non-dependent arrows where β does not depend on a.

  For example:

  • forall x : Prop, x ∧ x:

    Expr.forallE `x (.sort .zero)
      (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
    

  • Nat → Bool:

    Expr.forallE `a (.const `Nat [])
      (.const `Bool []) .default
    

• letE (declName : Name) (type value body : Expr) (nondep : Bool) : Expr

  Let-expressions.

  The let-expression let x : Nat := 2; Nat.succ x is represented as

  Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
  

  If the nondep flag is true, then the elaborator treats this as a non-dependent let (known as a have expression). Given an environment, a metavariable context, and a local context, we say a let-expression let x : t := v; e is non-dependent when it is equivalent to (fun x : t => e) v. In contrast, the dependent let-expression let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b is type correct, but (fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2 is not.

  The kernel does not verify nondep when type checking. This is an elaborator feature.

• lit : Literal → Expr

  Natural number and string literal values.

  They are not really needed, but provide a more compact representation in memory for these two kinds of literals, and are used to implement efficient reduction in the elaborator and kernel. The "raw" natural number 2 can be represented as Expr.lit (.natVal 2). Note that, it is definitionally equal to:

  Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
  

• mdata (data : MData) (expr : Expr) : Expr

  Metadata (aka annotations).

  We use annotations to provide hints to the pretty-printer, store references to Syntax nodes, position information, and save information for elaboration procedures (e.g., we use the inaccessible annotation during elaboration to mark Exprs that correspond to inaccessible patterns).

  Note that Expr.mdata data e is definitionally equal to e.

• proj (typeName : Name) (idx : Nat) (struct : Expr) : Expr

  Projection-expressions. They are redundant, but are used to create more compact terms, speedup reduction, and implement eta for structures. The type of struct must be an structure-like inductive type. That is, it has only one constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators check whether the typeName matches the type of struct, and whether the (zero-based) index is valid (i.e., it is smaller than the number of constructor fields). When exporting Lean developments to other systems, proj can be replaced with typeName.rec applications.

  Example, given a : Nat × Bool, a.1 is represented as

  .proj `Prod 0 a
  

@[implicit_reducible]

instance Lean.instReprExpr : Repr Expr

def Lean.instReprExpr.repr : Expr → Nat → Format

@[implicit_reducible]

instance Lean.instInhabitedExpr : Inhabited Expr

def Lean.Expr.ctorName : Expr → String

The constructor name for the given expression. This is used for debugging purposes.

def Lean.Expr.hash (e : Expr) : UInt64

@[implicit_reducible]

instance Lean.Expr.instHashable : Hashable Expr

def Lean.Expr.hasFVar (e : Expr) : Bool

Return true if e contains free variables. This is a constant time operation.

def Lean.Expr.hasExprMVar (e : Expr) : Bool

Return true if e contains expression metavariables. This is a constant time operation.

def Lean.Expr.hasLevelMVar (e : Expr) : Bool

Return true if e contains universe (aka Level) metavariables. This is a constant time operation.

def Lean.Expr.hasMVar (e : Expr) : Bool

Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.

def Lean.Expr.hasLevelParam (e : Expr) : Bool

Return true if e contains universe level parameters. This is a constant time operation.

def Lean.Expr.approxDepth (e : Expr) : UInt32

Return the approximated depth of an expression. This information is used to compute the expression hash code, and speedup comparisons. This is a constant time operation. We say it is approximate because it maxes out at 255.

def Lean.Expr.looseBVarRange (e : Expr) : Nat

The range of de-Bruijn variables that are loose. That is, bvars that are not bound by a binder. For example, bvar i has range i + 1 and an expression with no loose bvars has range 0.

def Lean.Expr.binderInfo (e : Expr) : BinderInfo

Return the binder information if e is a lambda or forall expression, and .default otherwise.

Export functions.

@[export lean_expr_hash]

def Lean.Expr.hashEx : Expr → UInt64

@[export lean_expr_has_fvar]

def Lean.Expr.hasFVarEx : Expr → Bool

@[export lean_expr_has_expr_mvar]

def Lean.Expr.hasExprMVarEx : Expr → Bool

@[export lean_expr_has_level_mvar]

def Lean.Expr.hasLevelMVarEx : Expr → Bool

@[export lean_expr_has_mvar]

def Lean.Expr.hasMVarEx : Expr → Bool

@[export lean_expr_has_level_param]

def Lean.Expr.hasLevelParamEx : Expr → Bool

@[export lean_expr_loose_bvar_range]

def Lean.Expr.looseBVarRangeEx (e : Expr) : UInt32

@[export lean_expr_binder_info]

def Lean.Expr.binderInfoEx : Expr → BinderInfo

def Lean.mkConst (declName : Name) (us : List Level := []) : Expr

mkConst declName us return .const declName us.

def Lean.Literal.type : Literal → Expr

Return the type of a literal value.

@[export lean_lit_type]

def Lean.Literal.typeEx : Literal → Expr

def Lean.mkBVar (idx : Nat) : Expr

.bvar idx is now the preferred form.

def Lean.mkSort (u : Level) : Expr

.sort u is now the preferred form.

def Lean.mkFVar (fvarId : FVarId) : Expr

.fvar fvarId is now the preferred form. This function is seldom used, free variables are often automatically created using the telescope functions (e.g., forallTelescope and lambdaTelescope) at MetaM.

def Lean.mkMVar (mvarId : MVarId) : Expr

.mvar mvarId is now the preferred form. This function is seldom used, metavariables are often created using functions such as mkFreshExprMVar at MetaM.

def Lean.mkMData (m : MData) (e : Expr) : Expr

.mdata m e is now the preferred form.

def Lean.mkProj (structName : Name) (idx : Nat) (struct : Expr) : Expr

.proj structName idx struct is now the preferred form.

@[match_pattern]

def Lean.mkApp (f a : Expr) : Expr

.app f a is now the preferred form.

def Lean.mkLambda (x : Name) (bi : BinderInfo) (t b : Expr) : Expr

.lam x t b bi is now the preferred form.

def Lean.mkForall (x : Name) (bi : BinderInfo) (t b : Expr) : Expr

.forallE x t b bi is now the preferred form.

def Lean.mkSimpleThunkType (type : Expr) : Expr

Return Unit -> type. Do not confuse with Thunk type

def Lean.mkSimpleThunk (type : Expr) : Expr

Return fun (_ : Unit), e

@[inline]

def Lean.mkLet (x : Name) (t v b : Expr) (nondep : Bool := false) : Expr

Returns let x : t := v; b, a let expression. If nondep := true, then returns a have.

@[inline]

def Lean.mkHave (x : Name) (t v b : Expr) : Expr

Returns have x : t := v; b, a non-dependent let expression.

@[match_pattern]

def Lean.mkAppB (f a b : Expr) : Expr

@[match_pattern]

def Lean.mkApp2 (f a b : Expr) : Expr

@[match_pattern]

def Lean.mkApp3 (f a b c : Expr) : Expr

@[match_pattern]

def Lean.mkApp4 (f a b c d : Expr) : Expr

@[match_pattern]

def Lean.mkApp5 (f a b c d e : Expr) : Expr

@[match_pattern]

def Lean.mkApp6 (f a b c d e₁ e₂ : Expr) : Expr

@[match_pattern]

def Lean.mkApp7 (f a b c d e₁ e₂ e₃ : Expr) : Expr

@[match_pattern]

def Lean.mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) : Expr

@[match_pattern]

def Lean.mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) : Expr

@[match_pattern]

def Lean.mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) : Expr

@[match_pattern]

def Lean.mkLit (l : Literal) : Expr

.lit l is now the preferred form.

@[match_pattern]

def Lean.mkRawNatLit (n : Nat) : Expr

Returns the "raw" natural number .lit (.natVal n). This is not the default representation used by the Lean frontend. See mkNatLit.

def Lean.mkInstOfNatNat (n : Expr) : Expr

Returns instOfNatNat n : OfNat Nat n

def Lean.mkNatLitCore (n : Expr) : Expr

@[match_pattern]

def Lean.mkNatLit (n : Nat) : Expr

Returns a natural number literal used in the frontend. It is a OfNat.ofNat application. Recall that all theorems and definitions containing numeric literals are encoded using OfNat.ofNat applications in the frontend.

@[match_pattern]

def Lean.mkStrLit (s : String) : Expr

Return the string literal .lit (.strVal s)

@[export lean_expr_mk_bvar]

def Lean.mkBVarEx : Nat → Expr

@[export lean_expr_mk_fvar]

def Lean.mkFVarEx : FVarId → Expr

@[export lean_expr_mk_mvar]

def Lean.mkMVarEx : MVarId → Expr

@[export lean_expr_mk_sort]

def Lean.mkSortEx : Level → Expr

@[export lean_expr_mk_const]

def Lean.mkConstEx (c : Name) (lvls : List Level) : Expr

@[export lean_expr_mk_app]

def Lean.mkAppEx : Expr → Expr → Expr

@[export lean_expr_mk_lambda]

def Lean.mkLambdaEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr

@[export lean_expr_mk_forall]

def Lean.mkForallEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr

@[export lean_expr_mk_let]

def Lean.mkLetEx (n : Name) (t v b : Expr) (nondep : Bool) : Expr

@[export lean_expr_mk_lit]

def Lean.mkLitEx : Literal → Expr

@[export lean_expr_mk_mdata]

def Lean.mkMDataEx : MData → Expr → Expr

@[export lean_expr_mk_proj]

def Lean.mkProjEx : Name → Nat → Expr → Expr

def Lean.mkAppN (f : Expr) (args : Array Expr) : Expr

mkAppN f #[a₀, ..., aₙ] constructs the application f a₀ a₁ ... aₙ.

def Lean.mkAppRange (f : Expr) (i j : Nat) (args : Array Expr) : Expr

mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ] ==> the expression f a_i ... a_{j-1}

def Lean.mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr

Same as mkApp f args but reversing args.

@[extern lean_expr_dbg_to_string]

opaque Lean.Expr.dbgToString (e : Expr) : String

@[extern lean_expr_quick_lt]

opaque Lean.Expr.quickLt (a b : Expr) : Bool

A total order for expressions. We say it is quick because it first compares the hashcodes.

@[extern lean_expr_lt]

opaque Lean.Expr.lt (a b : Expr) : Bool

A total order for expressions that takes the structure into account (e.g., variable names).

def Lean.Expr.quickComp (a b : Expr) : Ordering

@[extern lean_expr_eqv]

opaque Lean.Expr.eqv (a b : Expr) : Bool

Return true iff a and b are alpha equivalent. Binder annotations are ignored.

@[implicit_reducible]

instance Lean.Expr.instBEq : BEq Expr

@[extern lean_expr_equal]

opaque Lean.Expr.equal (a b : Expr) : Bool

Return true iff a and b are equal. Binder names and annotations are taken into account.

def Lean.Expr.isSort : Expr → Bool

Return true if the given expression is a .sort ..

def Lean.Expr.isType : Expr → Bool

Return true if the given expression is of the form .sort (.succ ..).

def Lean.Expr.isType0 : Expr → Bool

Return true if the given expression is of the form .sort (.succ .zero).

def Lean.Expr.isProp : Expr → Bool

Return true if the given expression is .sort .zero

def Lean.Expr.isBVar : Expr → Bool

Return true if the given expression is a bound variable.

def Lean.Expr.isMVar : Expr → Bool

Return true if the given expression is a metavariable.

def Lean.Expr.isFVar : Expr → Bool

Return true if the given expression is a free variable.

def Lean.Expr.isApp : Expr → Bool

Return true if the given expression is an application.

def Lean.Expr.isProj : Expr → Bool

Return true if the given expression is a projection .proj ..

def Lean.Expr.isConst : Expr → Bool

Return true if the given expression is a constant.

def Lean.Expr.isConstOf : Expr → Name → Bool

Return true if the given expression is a constant of the given name. Examples:

• (.const `Nat []).isConstOf `Nat is true
• (.const `Nat []).isConstOf `False is false

def Lean.Expr.isFVarOf : Expr → FVarId → Bool

Return true if the given expression is a free variable with the given id. Examples:

• isFVarOf (.fvar id) id is true
• isFVarOf (.fvar id) id' is false
• isFVarOf (.sort levelZero) id is false

def Lean.Expr.isForall : Expr → Bool

Return true if the given expression is a forall-expression aka (dependent) arrow.

def Lean.Expr.isLambda : Expr → Bool

Return true if the given expression is a lambda abstraction aka anonymous function.

def Lean.Expr.isBinding : Expr → Bool

Return true if the given expression is a forall or lambda expression.

def Lean.Expr.isLet : Expr → Bool

Return true if the given expression is a let-expression or a have-expression.

def Lean.Expr.isHave : Expr → Bool

Return true if the given expression is a non-dependent let-expression (a have-expression).

@[export lean_expr_is_have]

def Lean.Expr.isHaveEx : Expr → Bool

def Lean.Expr.isMData : Expr → Bool

Return true if the given expression is a metadata.

def Lean.Expr.isLit : Expr → Bool

Return true if the given expression is a literal value.

def Lean.Expr.appFn! : Expr → Expr

def Lean.Expr.appArg! : Expr → Expr

def Lean.Expr.appFn!' : Expr → Expr

def Lean.Expr.appArg!' : Expr → Expr

def Lean.Expr.appArg (e : Expr) (h : e.isApp = true) : Expr

def Lean.Expr.appFn (e : Expr) (h : e.isApp = true) : Expr

def Lean.Expr.sortLevel! : Expr → Level

def Lean.Expr.litValue! : Expr → Literal

def Lean.Expr.isRawNatLit : Expr → Bool

def Lean.Expr.rawNatLit? : Expr → Option Nat

def Lean.Expr.isStringLit : Expr → Bool

def Lean.Expr.isCharLit : Expr → Bool

def Lean.Expr.constName! : Expr → Name

If the expression is a constant, return that name. Otherwise panic.

def Lean.Expr.constName? : Expr → Option Name

If the expression is a constant, return that name. Otherwise return Option.none.

def Lean.Expr.constName (e : Expr) : Name

If the expression is a constant, return that name. Otherwise return Name.anonymous.

def Lean.Expr.constLevels! : Expr → List Level

def Lean.Expr.bvarIdx! : Expr → Nat

def Lean.Expr.fvarId! : Expr → FVarId

def Lean.Expr.fvarId? : Expr → Option FVarId

def Lean.Expr.mvarId! : Expr → MVarId

def Lean.Expr.bindingName! : Expr → Name

def Lean.Expr.bindingDomain! : Expr → Expr

def Lean.Expr.bindingBody! : Expr → Expr

def Lean.Expr.bindingInfo! : Expr → BinderInfo

def Lean.Expr.forallName (a : Expr) : a.isForall = true → Name

def Lean.Expr.forallDomain (a : Expr) : a.isForall = true → Expr

def Lean.Expr.forallBody (a : Expr) : a.isForall = true → Expr

def Lean.Expr.forallInfo (a : Expr) : a.isForall = true → BinderInfo

def Lean.Expr.letName! : Expr → Name

def Lean.Expr.letType! : Expr → Expr

def Lean.Expr.letValue! : Expr → Expr

def Lean.Expr.letBody! : Expr → Expr

def Lean.Expr.letNondep! : Expr → Bool

def Lean.Expr.consumeMData : Expr → Expr

def Lean.Expr.mdataExpr! : Expr → Expr

def Lean.Expr.projExpr! : Expr → Expr

def Lean.Expr.projIdx! : Expr → Nat

def Lean.Expr.getForallBody : Expr → Expr

Return the "body" of a forall expression. Example: let e be the representation for forall (p : Prop) (q : Prop), p ∧ q, then getForallBody e returns .app (.app (.const `And []) (.bvar 1)) (.bvar 0)

def Lean.Expr.getForallBodyMaxDepth (maxDepth : Nat) : Expr → Expr

def Lean.Expr.getForallBinderNames : Expr → List Name

Given a sequence of nested foralls (a₁ : α₁) → ... → (aₙ : αₙ) → _, returns the names [a₁, ... aₙ].

def Lean.Expr.getNumHeadForalls : Expr → Nat

Returns the number of leading ∀ binders of an expression. Ignores metadata.

def Lean.Expr.getAppFn : Expr → Expr

If the given expression is a sequence of function applications f a₁ .. aₙ, return f. Otherwise return the input expression.

def Lean.Expr.getAppFn' : Expr → Expr

Similar to getAppFn, but skips mdata

def Lean.Expr.isAppOf (e : Expr) (n : Name) : Bool

Given f a₀ a₁ ... aₙ, returns true if f is a constant with name n.

def Lean.Expr.isAppOfArity : Expr → Name → Nat → Bool

Given f a₁ ... aᵢ, returns true if f is a constant with name n and has the correct number of arguments.

def Lean.Expr.isAppOfArity' : Expr → Name → Nat → Bool

Similar to isAppOfArity but skips Expr.mdata.

def Lean.Expr.getAppNumArgs (e : Expr) : Nat

Counts the number n of arguments for an expression f a₁ .. aₙ.

def Lean.Expr.getAppNumArgs' (e : Expr) : Nat

Like getAppNumArgs but ignores metadata.

def Lean.Expr.getBoundedAppFn (maxArgs : Nat) : Expr → Expr

Like Lean.Expr.getAppFn but assumes the application has up to maxArgs arguments. If there are any more arguments than this, then they are returned by getAppFn as part of the function.

In particular, if the given expression is a sequence of function applications f a₁ .. aₙ, returns f a₁ .. aₖ where k is minimal such that n - k ≤ maxArgs.

@[inline]

def Lean.Expr.getAppArgs (e : Expr) : Array Expr

Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ]

@[inline]

def Lean.Expr.getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr

Like Lean.Expr.getAppArgs but returns up to maxArgs arguments.

In particular, given f a₁ a₂ ... aₙ, returns #[aₖ₊₁, ..., aₙ] where k is minimal such that the size of this array is at most maxArgs.

@[inline]

def Lean.Expr.getAppRevArgs (e : Expr) : Array Expr

Same as getAppArgs but reverse the output array.

@[specialize #[]]

def Lean.Expr.withAppAux {α : Sort u_1} (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α

@[inline]

def Lean.Expr.withApp {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) : α

Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ].

def Lean.Expr.getAppFnArgs (e : Expr) : Name × Array Expr

Return the function (name) and arguments of an application.

@[inline]

def Lean.Expr.getAppArgsN (e : Expr) (n : Nat) : Array Expr

Given f a_1 ... a_n, returns #[a_1, ..., a_n]. Note that f may be an application. The resulting array has size n even if f.getAppNumArgs < n.

def Lean.Expr.stripArgsN (e : Expr) (n : Nat) : Expr

Given e of the form f a_1 ... a_n, return f. If n is greater than the number of arguments, then return e.getAppFn.

def Lean.Expr.getAppPrefix (e : Expr) (n : Nat) : Expr

Given e of the form f a_1 ... a_n ... a_m, return f a_1 ... a_n. If n is greater than the arity, then return e.

def Lean.Expr.traverseApp {M : Type → Type u_1} [Monad M] (f : Expr → M Expr) (e : Expr) : M Expr

Given e = fn a₁ ... aₙ, runs f on fn and each of the arguments aᵢ and makes a new function application with the results.

@[inline]

def Lean.Expr.withAppRev {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) : α

Same as withApp but with arguments reversed.

def Lean.Expr.getRevArgD : Expr → Nat → Expr → Expr

def Lean.Expr.getRevArg! : Expr → Nat → Expr

def Lean.Expr.getRevArg!' : Expr → Nat → Expr

Similar to getRevArg! but skips mdata

@[inline]

def Lean.Expr.getArg! (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs) : Expr

Given f a₀ a₁ ... aₙ, returns the ith argument or panics if out of bounds.

@[inline]

def Lean.Expr.getArg!' (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs') : Expr

Similar to getArg!, but skips mdata

@[inline]

def Lean.Expr.getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n : Nat := e.getAppNumArgs) : Expr

Given f a₀ a₁ ... aₙ, returns the ith argument or returns v₀ if out of bounds.

def Lean.Expr.hasLooseBVars (e : Expr) : Bool

Return true if e contains any loose bound variables.

This is a constant time operation.

def Lean.Expr.isArrow (e : Expr) : Bool

Return true if e is a non-dependent arrow. Remark: the following function assumes e does not have loose bound variables.

@[extern lean_expr_has_loose_bvar]

opaque Lean.Expr.hasLooseBVar (e : Expr) (bvarIdx : Nat) : Bool

Return true if e contains the specified loose bound variable with index bvarIdx.

This operation traverses the expression tree.

def Lean.Expr.hasLooseBVarInExplicitDomain (e : Expr) (bvarIdx : Nat) (considerRange : Bool) : Bool

Returns true if e contains the loose bound variable bvarIdx in an explicit parameter, or in the range if considerRange == true. Additionally, if the bound variable appears in an implicit parameter, it transitively looks for that implicit parameter.

@[extern lean_expr_lower_loose_bvars]

opaque Lean.Expr.lowerLooseBVars (e : Expr) (s d : Nat) : Expr

Lower the loose bound variables >= s in e by d. That is, a loose bound variable bvar i with i >= s is mapped to bvar (i-d).

Remark: if s < d, then the result is e.

@[extern lean_expr_lift_loose_bvars]

opaque Lean.Expr.liftLooseBVars (e : Expr) (s d : Nat) : Expr

Lift loose bound variables >= s in e by d.

def Lean.Expr.inferImplicit (e : Expr) (numParams : Nat) (considerRange : Bool) : Expr

inferImplicit e numParams considerRange updates the first numParams parameter binder annotations of the e forall type. It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or the resulting type if considerRange == true.

Remark: we use this function to infer the binder annotations of structure projections.

def Lean.Expr.updateForallBinderInfos (e : Expr) (binderInfos? : List (Option BinderInfo)) : Expr

Uses binderInfos? to update the binder infos of the corresponding forall expressions.

def Lean.Expr.updateBinderNames (e : Expr) (binderNames? : List (Option Name)) : Expr

Uses binderNames? to update the binder names of the corresponding lambda and forall expressions.

@[extern lean_expr_instantiate]

opaque Lean.Expr.instantiate (e : Expr) (subst : Array Expr) : Expr

Instantiates the loose bound variables in e using the subst array, where a loose Expr.bvar i at "binding depth" d is instantiated with subst[i - d] if 0 <= i - d < subst.size, and otherwise it is replaced with Expr.bvar (i - subst.size); non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate is instantiating the last n of these and reindexing the remaining ones. Warning: instantiate uses the de Bruijn indexing to index the subst array, which might be the reverse order from what you might expect. See also Lean.Expr.instantiateRev.

Terminology. The "binding depth" of a subexpression is the number of bound variables available to that subexpression by virtue of being in the bodies of Expr.forallE, Expr.lam, and Expr.letE expressions. A bound variable Expr.bvar i is "loose" if its de Bruijn index i is not less than its binding depth.)

About instantiation. Instantiation isn't mere substitution. When an expression from subst is being instantiated, its internal loose bound variables have their de Bruijn indices incremented by the binding depth of the replaced loose bound variable. This is necessary for the substituted expression to still refer to the correct binders after instantiation. Similarly, the reason loose bound variables not instantiated using subst have their de Bruijn indices decremented like Expr.bvar (i - subst.size) is that instantiate can be used to eliminate binding expressions internal to a larger expression, and this adjustment keeps these bound variables referring to the same binders.

@[extern lean_expr_instantiate1]

opaque Lean.Expr.instantiate1 (e subst : Expr) : Expr

Instantiates loose bound variable 0 in e using the expression subst, where in particular a loose Expr.bvar i at binding depth d is instantiated with subst if i = d, and otherwise it is replaced with Expr.bvar (i - 1); non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate1 is instantiating the last one of these and reindexing the remaining ones.

This function is equivalent to instantiate e #[subst], but it avoids allocating an array.

See the documentation for Lean.Expr.instantiate for a description of instantiation. In short, during instantiation the loose bound variables in subst have their own de Bruijn indices updated to account for the binding depth of the replaced loose bound variable.

@[extern lean_expr_instantiate_rev]

opaque Lean.Expr.instantiateRev (e : Expr) (subst : Array Expr) : Expr

Instantiates the loose bound variables in e using the subst array. This is equivalent to Lean.Expr.instantiate e subst.reverse, but it avoids reversing the array. In particular, rather than instantiating Expr.bvar i with subst[i - d] it instantiates with subst[subst.size - 1 - (i - d)], where d is the binding depth.

This function instantiates with the "forwards" indexing scheme. For example, if e represents the expression fun x y => x + y, then instantiateRev e.bindingBody!.bindingBody! #[a, b] yields a + b. The instantiate function on the other hand would yield b + a, since de Bruijn indices count outwards.

@[extern lean_expr_instantiate_range]

opaque Lean.Expr.instantiateRange (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) : Expr

Similar to Lean.Expr.instantiate, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

This function is equivalent to instantiate e (subst.extract beginIdx endIdx), but it does not allocate a new array.

This instantiates with the "backwards" indexing scheme. See also Lean.Expr.instantiateRevRange, which instantiates with the "forwards" indexing scheme.

@[extern lean_expr_instantiate_rev_range]

opaque Lean.Expr.instantiateRevRange (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) : Expr

Similar to Lean.Expr.instantiateRev, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

This function is equivalent to instantiateRev e (subst.extract beginIdx endIdx), but it does not allocate a new array.

This instantiates with the "forwards" indexing scheme (see the docstring for Lean.Expr.instantiateRev for an example). See also Lean.Expr.instantiateRange, which instantiates with the "backwards" indexing scheme.

@[extern lean_expr_abstract]

opaque Lean.Expr.abstract (e : Expr) (xs : Array Expr) : Expr

Replace free (or meta) variables xs with loose bound variables, with xs ordered from outermost to innermost de Bruijn index.

For example, e := f x y with xs := #[x, y] goes to f #1 #0, whereas e := f x y with xs := #[y, x] goes to f #0 #1.

Careful, this function does not instantiate assigned meta variables.

@[extern lean_expr_abstract_range]

opaque Lean.Expr.abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : Expr

Similar to abstract, but consider only the first min n xs.size entries in xs.

def Lean.Expr.replaceFVar (e fvar v : Expr) : Expr

Replace occurrences of the free variable fvar in e with v

def Lean.Expr.replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr

Replace occurrences of the free variable fvarId in e with v

def Lean.Expr.replaceFVars (e : Expr) (fvars vs : Array Expr) : Expr

Replace occurrences of the free variables fvars in e with vs

@[implicit_reducible]

instance Lean.Expr.instToString : ToString Expr

def Lean.Expr.isAtomic : Expr → Bool

Returns true when the expression does not have any sub-expressions.

def Lean.mkDecIsTrue (pred proof : Expr) : Expr

def Lean.mkDecIsFalse (pred proof : Expr) : Expr

@[reducible, inline]

abbrev Lean.ExprMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.PersistentExprMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.SExprMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.ExprSet : Type

@[reducible, inline]

abbrev Lean.PersistentExprSet : Type

@[reducible, inline]

abbrev Lean.PExprSet : Type

structure Lean.ExprStructEq : Type

Auxiliary type for forcing == to be structural equality for Expr

• val : Expr

@[implicit_reducible]

instance Lean.instInhabitedExprStructEq : Inhabited ExprStructEq

def Lean.instInhabitedExprStructEq.default : ExprStructEq

@[implicit_reducible]

instance Lean.instCoeExprExprStructEq : Coe Expr ExprStructEq

def Lean.ExprStructEq.beq : ExprStructEq → ExprStructEq → Bool

def Lean.ExprStructEq.hash : ExprStructEq → UInt64

@[implicit_reducible]

instance Lean.ExprStructEq.instBEq : BEq ExprStructEq

@[implicit_reducible]

instance Lean.ExprStructEq.instHashable : Hashable ExprStructEq

@[implicit_reducible]

instance Lean.ExprStructEq.instToString : ToString ExprStructEq

@[reducible, inline]

abbrev Lean.ExprStructMap (α : Type) : Type

@[reducible, inline]

abbrev Lean.PersistentExprStructMap (α : Type) : Type

def Lean.Expr.mkAppRevRange (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : Expr

mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)

def Lean.Expr.betaRev (f : Expr) (revArgs : Array Expr) (useZeta preserveMData : Bool := false) : Expr

If f is a lambda expression, than "beta-reduce" it using revArgs. This function is often used with getAppRev or withAppRev. Examples:

• betaRev (fun x y => t x y) #[] ==> fun x y => t x y
• betaRev (fun x y => t x y) #[a] ==> fun y => t a y
• betaRev (fun x y => t x y) #[a, b] ==> t b a
• betaRev (fun x y => t x y) #[a, b, c, d] ==> t d c b a Suppose t is (fun x y => t x y) a b c d, then args := t.getAppRev is #[d, c, b, a], and betaRev (fun x y => t x y) #[d, c, b, a] is t a b c d.

If useZeta is true, the function also performs zeta-reduction (reduction of let binders) to create further opportunities for beta reduction.

def Lean.Expr.beta (f : Expr) (args : Array Expr) : Expr

Apply the given arguments to f, beta-reducing if f is a lambda expression. See docstring for betaRev for examples.

def Lean.Expr.getNumHeadLambdas : Expr → Nat

Count the number of lambdas at the head of the given expression.

def Lean.Expr.isHeadBetaTargetFn (useZeta : Bool) : Expr → Bool

Return true if the given expression is the function of an expression that is target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

See isHeadBetaTarget.

def Lean.Expr.headBeta (e : Expr) : Expr

(fun x => e) a ==> e[x/a].

def Lean.Expr.isHeadBetaTarget (e : Expr) (useZeta : Bool := false) : Bool

Return true if the given expression is a target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

def Lean.Expr.etaExpanded? (e : Expr) : Option Expr

If e is of the form (fun x₁ ... xₙ => f x₁ ... xₙ) and f does not contain x₁, ..., xₙ, then return some f. Otherwise, return none.

It assumes e does not have loose bound variables.

Remark: ₙ may be 0

def Lean.Expr.etaExpandedStrict? : Expr → Option Expr

Similar to etaExpanded?, but only succeeds if ₙ ≥ 1.

def Lean.Expr.getOptParamDefault? (e : Expr) : Option Expr

Return some e' if e is of the form optParam _ e'

def Lean.Expr.getAutoParamTactic? (e : Expr) : Option Expr

Return some e' if e is of the form autoParam _ e'

@[export lean_is_out_param]

def Lean.Expr.isOutParam (e : Expr) : Bool

Return true if e is of the form outParam _

def Lean.Expr.isSemiOutParam (e : Expr) : Bool

Return true if e is of the form semiOutParam _

def Lean.Expr.isOptParam (e : Expr) : Bool

Return true if e is of the form optParam _ _

def Lean.Expr.isAutoParam (e : Expr) : Bool

Return true if e is of the form autoParam _ _

def Lean.Expr.isTypeAnnotation (e : Expr) : Bool

Returns true if e is an application of one of the type annotation gadgets. This does not check that the application has the correct arity.

@[export lean_expr_consume_type_annotations]

partial def Lean.Expr.consumeTypeAnnotations (e : Expr) : Expr

Remove outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

• Given e of the form outParam (optParam Nat b), consumeTypeAnnotations e = b.
• Given e of the form Nat → outParam (optParam Nat b), consumeTypeAnnotations e = e.

partial def Lean.Expr.cleanupAnnotations (e : Expr) : Expr

Remove metadata annotations and outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

• Given e of the form outParam (optParam Nat b), cleanupAnnotations e = b.
• Given e of the form Nat → outParam (optParam Nat b), cleanupAnnotations e = e.

def Lean.Expr.appFnCleanup (e : Expr) (h : e.isApp = true) : Expr

Similar to appFn, but also applies cleanupAnnotations to resulting function. This function is used compile the match_expr term.

def Lean.Expr.isFalse (e : Expr) : Bool

def Lean.Expr.isTrue (e : Expr) : Bool

partial def Lean.Expr.getForallArity : Expr → Nat

getForallArity type returns the arity of a forall-type. This function consumes nested annotations, and performs pending beta reductions. It does not use whnf. Examples:

• If a is Nat, getForallArity a returns 0
• If a is Nat → Bool, getForallArity a returns 1

def Lean.Expr.nat? (e : Expr) : Option Nat

Checks if an expression is a "natural number numeral in normal form", i.e. of type Nat, and explicitly of the form OfNat.ofNat n where n matches .lit (.natVal n) for some literal natural number n. and if so returns n.

def Lean.Expr.int? (e : Expr) : Option Int

Checks if an expression is an "integer numeral in normal form", i.e. of type Nat or Int, and either a natural number numeral in normal form (as specified by nat?), or the negation of a positive natural number numeral in normal form, and if so returns the integer.

@[inline]

def Lean.Expr.hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool

Return true iff e contains a free variable which satisfies p.

def Lean.Expr.containsFVar (e : Expr) (fvarId : FVarId) : Bool

Return true if e contains the given free variable.

The update functions try to avoid allocating new values using pointer equality. Note that if the update*! functions are used under a match-expression, the compiler will eliminate the double-match.

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateApp!Impl]

def Lean.Expr.updateApp! (e newFn newArg : Expr) : Expr

@[inline]

def Lean.Expr.updateFVar! (e : Expr) (fvarIdNew : FVarId) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateConst!Impl]

def Lean.Expr.updateConst! (e : Expr) (newLevels : List Level) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateSort!Impl]

def Lean.Expr.updateSort! (e : Expr) (newLevel : Level) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateMData!Impl]

def Lean.Expr.updateMData! (e newExpr : Expr) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateProj!Impl]

def Lean.Expr.updateProj! (e newExpr : Expr) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateForall!Impl]

def Lean.Expr.updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain newBody : Expr) : Expr

@[inline]

def Lean.Expr.updateForallE! (e newDomain newBody : Expr) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLambda!Impl]

def Lean.Expr.updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain newBody : Expr) : Expr

@[inline]

def Lean.Expr.updateLambdaE! (e newDomain newBody : Expr) : Expr

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLet!Impl]

def Lean.Expr.updateLet! (e newType newVal newBody : Expr) (newNondep : Bool) : Expr

@[inline]

def Lean.Expr.updateLetE! (e newType newVal newBody : Expr) : Expr

Like Expr.updateLet! but preserves the nondep flag.

def Lean.Expr.updateFn : Expr → Expr → Expr

def Lean.Expr.eta (e : Expr) : Expr

Eta reduction. If e is of the form (fun x => f x), then return f.

def Lean.Expr.setOption {α : Type} (e : Expr) (optionName : Name) [KVMap.Value α] (val : α) : Expr

Annotate e with the given option. The information is stored using metadata around e.

def Lean.Expr.setPPExplicit (e : Expr) (flag : Bool) : Expr

Annotate e with pp.explicit := flag The delaborator uses pp options.

def Lean.Expr.setPPUniverses (e : Expr) (flag : Bool) : Expr

Annotate e with pp.universes := flag The delaborator uses pp options.

def Lean.Expr.setPPPiBinderTypes (e : Expr) (flag : Bool) : Expr

Annotate e with pp.piBinderTypes := flag The delaborator uses pp options.

def Lean.Expr.setPPFunBinderTypes (e : Expr) (flag : Bool) : Expr

Annotate e with pp.funBinderTypes := flag The delaborator uses pp options.

def Lean.Expr.setPPNumericTypes (e : Expr) (flag : Bool) : Expr

Annotate e with pp.numericTypes := flag The delaborator uses pp options.

def Lean.Expr.setAppPPExplicit (e : Expr) : Expr

If e is an application f a_1 ... a_n annotate f, a_1 ... a_n with pp.explicit := false, and annotate e with pp.explicit := true.

def Lean.Expr.setAppPPExplicitForExposingMVars (e : Expr) : Expr

Similar for setAppPPExplicit, but only annotate children with pp.explicit := false if e does not contain metavariables.

@[specialize #[]]

def Lean.Expr.traverseChildren {M : Type → Type u_1} [Applicative M] (f : Expr → M Expr) : Expr → M Expr

Maps f on each immediate child of the given expression.

def Lean.Expr.foldlM {α : Type} {m : Type → Type u_1} [Monad m] (f : α → Expr → m α) (init : α) (e : Expr) : m α

e.foldlM f a folds the monadic function f over the subterms of the expression e, with initial value a.

def Lean.Expr.sizeWithoutSharing (e : Expr) : Nat

Returns the size of e as a tree, i.e. nodes reachable via multiple paths are counted multiple times.

This is a naive implementation that visits shared subterms multiple times instead of caching their sizes. It is primarily meant for debugging.

def Lean.mkAnnotation (kind : Name) (e : Expr) : Expr

Annotate e with the given annotation name kind. It uses metadata to store the annotation.

def Lean.annotation? (kind : Name) (e : Expr) : Option Expr

Return some e' if e = mkAnnotation kind e'

def Lean.mkInaccessible (e : Expr) : Expr

Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t) and _ in patterns.

def Lean.inaccessible? (e : Expr) : Option Expr

Return some e' if e = mkInaccessible e'.

def Lean.patternWithRef? (p : Expr) : Option (Syntax × Expr)

During elaboration expressions corresponding to pattern matching terms are annotated with Syntax objects. This function returns some (stx, p') if p is the pattern p' annotated with stx

def Lean.isPatternWithRef (p : Expr) : Bool

def Lean.mkPatternWithRef (p : Expr) (stx : Syntax) : Expr

Annotate the pattern p with stx. This is an auxiliary annotation for producing better hover information.

def Lean.patternAnnotation? (e : Expr) : Option Expr

Return some p if e is an annotated pattern (inaccessible? or patternWithRef?)

def Lean.mkLHSGoalRaw (e : Expr) : Expr

Annotate e with the LHS annotation. The delaborator displays expressions of the form lhs = rhs as lhs when they have this annotation. This is used to implement the infoview for the conv mode.

This version of mkLHSGoal does not check that the argument is an equality.

def Lean.isLHSGoal? (e : Expr) : Option Expr

Return some lhs if e = mkLHSGoal e', where e' is of the form lhs = rhs.

def Lean.mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId

Polymorphic operation for generating unique/fresh free variable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

def Lean.mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m MVarId

Polymorphic operation for generating unique/fresh metavariable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

def Lean.mkFreshLMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m LMVarId

Polymorphic operation for generating unique/fresh universe metavariable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

def Lean.mkNot (p : Expr) : Expr

Return Not p

def Lean.mkOr (p q : Expr) : Expr

Return p ∨ q

def Lean.mkAnd (p q : Expr) : Expr

Return p ∧ q

def Lean.mkAndN : List Expr → Expr

Make an n-ary And application. mkAndN [] returns True.

def Lean.mkEM (p : Expr) : Expr

Returns Classical.em p

def Lean.mkIff (p q : Expr) : Expr

Returns p ↔ q

Constants for Nat typeclasses.

def Lean.Nat.mkType : Expr

def Lean.Nat.mkInstAdd : Expr

def Lean.Nat.mkInstHAdd : Expr

def Lean.Nat.mkInstSub : Expr

def Lean.Nat.mkInstHSub : Expr

def Lean.Nat.mkInstMul : Expr

def Lean.Nat.mkInstHMul : Expr

def Lean.Nat.mkInstDiv : Expr

def Lean.Nat.mkInstHDiv : Expr

def Lean.Nat.mkInstMod : Expr

def Lean.Nat.mkInstHMod : Expr

def Lean.Nat.mkInstNatPow : Expr

def Lean.Nat.mkInstPow : Expr

def Lean.Nat.mkInstHPow : Expr

def Lean.Nat.mkInstLT : Expr

def Lean.Nat.mkInstLE : Expr

def Lean.mkNatSucc (a : Expr) : Expr

Given a : Nat, returns Nat.succ a

def Lean.mkNatAdd (a b : Expr) : Expr

Given a b : Nat, returns a + b

def Lean.mkNatSub (a b : Expr) : Expr

Given a b : Nat, returns a - b

def Lean.mkNatMul (a b : Expr) : Expr

Given a b : Nat, returns a * b

def Lean.mkNatPow (a b : Expr) : Expr

Given a b : Nat, returns a ^ b

def Lean.mkNatLE (a b : Expr) : Expr

Given a b : Nat, return a ≤ b

def Lean.mkNatEq (a b : Expr) : Expr

Given a b : Nat, return a = b

def Lean.mkPropEq (a b : Expr) : Expr

Given a b : Prop, returns a = b

Constants for Int typeclasses.

def Lean.Int.mkType : Expr

def Lean.Int.mkInstNeg : Expr

def Lean.Int.mkInstAdd : Expr

def Lean.Int.mkInstHAdd : Expr

def Lean.Int.mkInstSub : Expr

def Lean.Int.mkInstHSub : Expr

def Lean.Int.mkInstMul : Expr

def Lean.Int.mkInstHMul : Expr

def Lean.Int.mkInstDiv : Expr

def Lean.Int.mkInstHDiv : Expr

def Lean.Int.mkInstMod : Expr

def Lean.Int.mkInstHMod : Expr

def Lean.Int.mkInstPow : Expr

def Lean.Int.mkInstPowNat : Expr

def Lean.Int.mkInstHPow : Expr

def Lean.Int.mkInstLT : Expr

def Lean.Int.mkInstLE : Expr

def Lean.Int.mkInstNatCast : Expr

def Lean.mkIntNeg (a : Expr) : Expr

Given a : Int, returns - a

def Lean.mkIntAdd (a b : Expr) : Expr

Given a b : Int, returns a + b

def Lean.mkIntSub (a b : Expr) : Expr

Given a b : Int, returns a - b

def Lean.mkIntMul (a b : Expr) : Expr

Given a b : Int, returns a * b

def Lean.mkIntDiv (a b : Expr) : Expr

Given a b : Int, returns a / b

def Lean.mkIntMod (a b : Expr) : Expr

Given a b : Int, returns a % b

def Lean.mkIntNatCast (a : Expr) : Expr

Given a : Nat, returns NatCast.natCast (R := Int) a

def Lean.mkIntPowNat (a b : Expr) : Expr

Given a b : Int, returns a ^ b

def Lean.mkIntLE (a b : Expr) : Expr

Given a b : Int, returns a ≤ b

def Lean.mkIntLT (a b : Expr) : Expr

Given a b : Int, returns a < b

def Lean.mkIntEq (a b : Expr) : Expr

Given a b : Int, returns a = b

def Lean.mkIntDvd (a b : Expr) : Expr

Given a b : Int, returns a ∣ b

def Lean.mkIntLit (n : Int) : Expr

def Lean.reflBoolTrue : Expr

def Lean.reflBoolFalse : Expr

def Lean.eagerReflBoolTrue : Expr

def Lean.eagerReflBoolFalse : Expr

def Lean.Expr.replaceFn (e : Expr) (declName : Name) : Expr

Replaces the head constant in a function application chain with a different constant.

Given an expression that is either a constant or a function application chain, replaces the head constant with declName while preserving all arguments and universe levels.

Examples:

• f.replaceFn g → g (where f is a constant)
• (f a b c).replaceFn g → g a b c
• (@f.{u, v} a b).replaceFn g → @g.{u, v} a b

Panics: If the expression is neither a constant nor a function application.

Use case: Useful for substituting one function for another while maintaining the same application structure, such as replacing a theorem with a related theorem that has the same type and universe parameters.