Additional operations on Expr and related types

This file defines basic operations on the types expr, name, declaration, level, environment.

This file is mostly for non-tactics.

Declarations about BinderInfo

def Lean.BinderInfo.brackets : BinderInfo → String × String

The brackets corresponding to a given BinderInfo.

Declarations about name

@[specialize #[]]

def Lean.Name.mapPrefix (f : Name → Option Name) (n : Name) : Name

Find the largest prefix n of a Name such that f n != none, then replace this prefix with the value of f n.

def Lean.Name.fromComponents : List Name → Name

Build a name from components. For example, from_components [`foo, `bar] becomes `foo.bar. It is the inverse of Name.components on list of names that have single components.

def Lean.Name.updateLast (f : String → String) : Name → Name

Update the last component of a name.

def Lean.Name.lastComponentAsString : Name → String

Get the last field of a name as a string. Doesn't raise an error when the last component is a numeric field.

def Lean.Name.splitAt (nm : Name) (n : ℕ) : Name × Name

nm.splitAt n splits a name nm in two parts, such that the second part has depth n, i.e. (nm.splitAt n).2.getNumParts = n (assuming nm.getNumParts ≥ n). Example: splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat).

def Lean.Name.isPrefixOf? (pre nm : Name) : Option Name

isPrefixOf? pre nm returns some post if nm = pre ++ post. Note that this includes the case where nm has multiple more namespaces. If pre is not a prefix of nm, it returns none.

def Lean.Name.isBlackListed {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

def Lean.ConstantInfo.isDef : ConstantInfo → Bool

Checks whether this ConstantInfo is a definition.

def Lean.ConstantInfo.isThm : ConstantInfo → Bool

Checks whether this ConstantInfo is a theorem.

def Lean.ConstantInfo.updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo

Update ConstantVal (the data common to all constructors of ConstantInfo) in a ConstantInfo.

def Lean.ConstantInfo.updateName (c : ConstantInfo) (name : Name) : ConstantInfo

Update the name of a ConstantInfo.

def Lean.ConstantInfo.updateType (c : ConstantInfo) (type : Expr) : ConstantInfo

Update the type of a ConstantInfo.

def Lean.ConstantInfo.updateLevelParams (c : ConstantInfo) (levelParams : List Name) : ConstantInfo

Update the level parameters of a ConstantInfo.

def Lean.ConstantInfo.updateValue : ConstantInfo → Expr → ConstantInfo

Update the value of a ConstantInfo, if it has one.

def Lean.ConstantInfo.toDeclaration! : ConstantInfo → Declaration

Turn a ConstantInfo into a declaration.

def Lean.mkConst' (constName : Name) : MetaM Expr

Same as mkConst, but with fresh level metavariables.

Declarations about Expr

def Lean.Expr.bvarIdx? : Expr → Option ℕ

@[inline]

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

Given f a b c, return #[f a, f a b, f a b c]. Each entry in the array is an Expr.app, and this array has the same length as the one returned by Lean.Expr.getAppArgs.

def Lean.Expr.eraseProofs (e : Expr) : MetaM Expr

Erase proofs in an expression by replacing them with sorrys.

This function replaces all proofs in the expression and in the types that appear in the expression by sorryAxs. The resulting expression has the same type as the old one.

It is useful, e.g., to verify if the proof-irrelevant part of a definition depends on a variable.

def Lean.Expr.type? : Expr → Option Level

If an Expr has the form Type u, then return some u, otherwise none.

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

isConstantApplication e checks whether e is syntactically an application of the form (fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ where H does not contain the variable xₙ. In other words, it does a syntactic check that the expression does not depend on yₙ.

@[inline]

partial def Lean.Expr.isAppOrForallOfConstP (p : Name → Bool) (type : Expr) : Bool

Returns true if type is an application of a constant decl for which p decl is true, or a forall with return type of the same form (i.e. of the form ∀ (x₀ : X₀) (x₁ : X₁) ⋯, decl .. where p decl).

Runs cleanupAnnotations on type and forallE bodies, and ignores metadata in applications.

@[inline]

def Lean.Expr.isAppOrForallOfConst (declName : Name) (type : Expr) : Bool

Returns true if type is an application of a constant declName, or a forall with return type of the same form (i.e. of the form ∀ (x₀ : X₀) (x₁ : X₁) ⋯, declName ..).

Runs cleanupAnnotations on type and forallE bodies, and ignores metadata in applications.

def Lean.Expr.getUnusedForallInstanceBinderIdxsWhere (p : Expr → Bool) (e : Expr) : Array ℕ

Gets the indices i (in ascending order) of the binders of a nested .forallE, (x₀ : A₀) → (x₁ : A₁) → ⋯ → X, such that

• the binder [xᵢ : Aᵢ] has instImplicit binderInfo
• p Aᵢ is true
• The rest of the type (xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X does not depend on xᵢ. (It's in this sense that xᵢ : Aᵢ is "unused".)

Note that the argument to p may have loose bvars. This is a performance optimization.

This function runs cleanupAnnotations on each expression before examining it.

We see through lets, and do not increment the index when doing so. This behavior is compatible with forallBoundedTelescope.

def Lean.Expr.letDepth : Expr → ℕ

Counts the immediate depth of a nested let expression.

def Lean.Expr.ensureHasNoMVars (e : Expr) : MetaM Unit

Check that an expression contains no metavariables (after instantiation).

def Lean.Expr.ofNat (α : Expr) (n : ℕ) : MetaM Expr

Construct the term of type α for a given natural number (doing typeclass search for the OfNat instance required).

def Lean.Expr.ofInt (α : Expr) : ℤ → MetaM Expr

Construct the term of type α for a given integer (doing typeclass search for the OfNat and Neg instances required).

partial def Lean.Expr.numeral? (e : Expr) : Option ℕ

Return some n if e is one of the following

• a nat literal (numeral)
• Nat.zero
• Nat.succ x where isNumeral x
• OfNat.ofNat _ x _ where isNumeral x

def Lean.Expr.zero? (e : Expr) : Bool

Test if an expression is either Nat.zero, or OfNat.ofNat 0.

def Lean.Expr.ne?' (e : Expr) : Option (Expr × Expr × Expr)

Tests is if an expression matches either x ≠ y or ¬ (x = y). If it matches, returns some (type, x, y).

@[inline]

def Lean.Expr.le? (p : Expr) : Option (Expr × Expr × Expr)

Lean.Expr.le? e takes e : Expr as input. If e represents a ≤ b, then it returns some (t, a, b), where t is the Type of a, otherwise, it returns none.

@[inline]

def Lean.Expr.lt? (p : Expr) : Option (Expr × Expr × Expr)

Lean.Expr.lt? e takes e : Expr as input. If e represents a < b, then it returns some (t, a, b), where t is the Type of a, otherwise, it returns none.

def Lean.Expr.sides? (ty : Expr) : Option (Expr × Expr × Expr × Expr)

Given a proposition ty that is an Eq, Iff, or HEq, returns (tyLhs, lhs, tyRhs, rhs), where lhs : tyLhs and rhs : tyRhs, and where lhs is related to rhs by the respective relation.

See also Lean.Expr.iff?, Lean.Expr.eq?, and Lean.Expr.heq?.

def Lean.Expr.modifyAppArgM {M : Type → Type u} [Functor M] [Pure M] (modifier : Expr → M Expr) : Expr → M Expr

def Lean.Expr.modifyRevArg (modifier : Expr → Expr) : ℕ → Expr → Expr

def Lean.Expr.modifyArg (modifier : Expr → Expr) (e : Expr) (i : ℕ) (n : ℕ := e.getAppNumArgs) : Expr

Given f a₀ a₁ ... aₙ₋₁, runs modifier on the ith argument or returns the original expression if out of bounds.

def Lean.Expr.setArg (e : Expr) (i : ℕ) (x : Expr) (n : ℕ := e.getAppNumArgs) : Expr

Given f a₀ a₁ ... aₙ₋₁, sets the argument on the ith argument to x or returns the original expression if out of bounds.

def Lean.Expr.getRevArg? : Expr → ℕ → Option Expr

def Lean.Expr.getArg? (e : Expr) (i : ℕ) (n : ℕ := e.getAppNumArgs) : Option Expr

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

def Lean.Expr.modifyArgM {M : Type → Type u} [Monad M] (modifier : Expr → M Expr) (e : Expr) (i : ℕ) (n : ℕ := e.getAppNumArgs) : M Expr

Given f a₀ a₁ ... aₙ₋₁, runs modifier on the ith argument. An argument n may be provided which says how many arguments we are expecting e to have.

def Lean.Expr.renameBVar (e : Expr) (old new : Name) : Expr

Traverses an expression e and renames bound variables named old to new.

def Lean.Expr.getBinderName (e : Expr) : MetaM (Option Name)

getBinderName e returns some n if e is an expression of the form ∀ n, ... and none otherwise.

def Lean.Expr.mapForallBinderNames : Expr → (Name → Name) → Expr

Map binder names in a nested forall (a₁ : α₁) → ... → (aₙ : αₙ) → _

def Lean.Expr.mkDirectProjection (e : Expr) (fieldName : Name) : MetaM Expr

If e has a structure as type with field fieldName, mkDirectProjection e fieldName creates the projection expression e.fieldName

def Lean.Expr.mkProjection (e : Expr) (fieldName : Name) : MetaM Expr

If e has a structure as type with field fieldName (either directly or in a parent structure), mkProjection e fieldName creates the projection expression e.fieldName

def Lean.Expr.reduceProjStruct? (e : Expr) : MetaM (Option Expr)

If e is a projection of the structure constructor, reduce the projection. Otherwise returns none. If this function detects that expression is ill-typed, throws an error. For example, given Prod.fst (x, y), returns some x.

@[specialize #[]]

def Lean.Expr.containsConst (e : Expr) (p : Name → Bool) : Bool

Returns true if e contains a name n where p n is true.

def Lean.Expr.forallNot_of_notExists (ex hNotEx : Expr) : MetaM (Expr × Expr)

Given (hNotEx : Not ex) where ex is of the form Exists x, p x, return a forall x, Not (p x) and a proof for it.

This function handles nested existentials.

def Lean.getFieldsToParents (env : Environment) (structName : Name) : Array Name

Get the projections that are projections to parent structures. Similar to getParentStructures, except that this returns the (last component of the) projection names instead of the parent names.