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 : Lean.BinderInfo → String × String

The brackets corresponding to a given BinderInfo.

Declarations about name

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

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

Equations

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

def Lean.Name.fromComponents : List Lean.Name → Lean.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.fromComponents.go : Lean.Name → List Lean.Name → Lean.Name

Auxiliary for Name.fromComponents

Equations

• Lean.Name.fromComponents.go x [] = x
• Lean.Name.fromComponents.go x (s :: rest) = Lean.Name.fromComponents.go (Lean.Name.updatePrefix s x) rest

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

Update the last component of a name.

def Lean.Name.getString : Lean.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 : Lean.Name) (n : Nat) : Lean.Name × Lean.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 : Lean.Name) (nm : Lean.Name) : Option Lean.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.

Equations

• Lean.Name.isPrefixOf? pre Lean.Name.anonymous = if (pre == Lean.Name.anonymous) = true then some Lean.Name.anonymous else none
• Lean.Name.isPrefixOf? pre (Lean.Name.num p' a) = if (pre == Lean.Name.num p' a) = true then some Lean.Name.anonymous else Option.map (fun x => Lean.Name.num x a) (Lean.Name.isPrefixOf? pre p')
• Lean.Name.isPrefixOf? pre (Lean.Name.str p' s) = if (pre == Lean.Name.str p' s) = true then some Lean.Name.anonymous else Option.map (fun x => Lean.Name.str x s) (Lean.Name.isPrefixOf? pre p')

def Lean.Name.isInternal' (declName : Lean.Name) : Bool

Lean 4 makes declarations which are technically not internal (that is, head string does not start with _) but which sometimes should be treated as such. For example, the to_additive attribute needs to transform proof_1 constants generated by Lean.Meta.mkAuxDefinitionFor. This might be better fixed in core, but until then, this method can act as a polyfill. This method only looks at the name to decide whether it is probably internal. Note: this declaration also occurs as shouldIgnore in the Lean 4 file test/lean/run/printDecls.

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

def Lean.NameSet.append (s : Lean.NameSet) (t : Lean.NameSet) : Lean.NameSet

The union of two NameSets.

instance Lean.NameSet.instAppendNameSet : Append Lean.NameSet

def Lean.ConstantInfo.isDef : Lean.ConstantInfo → Bool

Checks whether this ConstantInfo is a definition,

def Lean.ConstantInfo.isThm : Lean.ConstantInfo → Bool

Checks whether this ConstantInfo is a theorem,

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

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

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

Update the name of a ConstantInfo.

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

Update the type of a ConstantInfo.

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

Update the level parameters of a ConstantInfo.

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

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

def Lean.ConstantInfo.toDeclaration! : Lean.ConstantInfo → Lean.Declaration

Turn a ConstantInfo into a declaration.

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

Same as mkConst, but with fresh level metavariables.

Declarations about Expr

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

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

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

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

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

def Lean.Expr.getUsedConstants' (e : Lean.Expr) : Lean.NameSet

Like Expr.getUsedConstants, but produce a NameSet.

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

Turn an expression that is a natural number literal into a natural number.

def Lean.Expr.intLit! (e : Lean.Expr) : Int

Turn an expression that is a constructor of Int applied to a natural number literal into an integer.

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

Check if an expression is a "natural number in normal form", i.e. of the form OfNat n, where n matches .lit (.natVal lit) for some lit. and if so returns lit.

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

Check if an expression is an "integer in normal form", i.e. either a natural number in normal form, or the negation of one, and if so returns the integer.

def Lean.Expr.rat? (e : Lean.Expr) : Option Lean.Rat

Check if an expression is a "rational in normal form", i.e. either an integer number in normal form, or n / d where n is an integer in normal form, d is a natural number in normal form, d ≠ 1, and n and d are coprime (in particular, we check that (mkRat n d).den = d). If so returns the rational number.

def Lean.Expr.isExplicitNumber : Lean.Expr → Bool

Test if an expression represents an explicit number written in normal form:

• A "natural number in normal form" is an expression OfNat.ofNat n, even if it is not of type ℕ, as long as n is a literal.
• An "integer in normal form" is an expression which is either a natural number in number form, or -n, where n is a natural number in normal form.
• A "rational in normal form" is an expressions which is either an integer in normal form, or n / d where n is an integer in normal form, d is a natural number in normal form, d ≠ 1, and n and d are coprime (in particular, we check that (mkRat n d).den = d).

Equations

• Lean.Expr.isExplicitNumber (Lean.Expr.lit a) = true
• Lean.Expr.isExplicitNumber (Lean.Expr.mdata data e) = Lean.Expr.isExplicitNumber e
• Lean.Expr.isExplicitNumber x = Option.isSome (Lean.Expr.rat? x)

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

If an Expr has form .fvar n, then returns some n, otherwise none.

def Lean.Expr.isConstantApplication (e : Lean.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ₙ.

def Lean.Expr.isConstantApplication.aux (depth : Nat) : Lean.Expr → Nat → Bool

aux depth e n checks whether the body of the n-th lambda of e has loose bvar depth - 1.

def Lean.Expr.letDepth : Lean.Expr → Nat

Counts the immediate depth of a nested let expression.

Equations

• Lean.Expr.letDepth (Lean.Expr.letE declName type value b nonDep) = Lean.Expr.letDepth b + 1
• Lean.Expr.letDepth x = 0

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

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

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

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

def Lean.Expr.ofInt (α : Lean.Expr) : Int → Lean.MetaM Lean.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 : Lean.Expr) : Option Nat

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 : Lean.Expr) : Bool

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

def Lean.Expr.ne?' (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.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 : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.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.

def Lean.Expr.sides? (ty : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.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_1} [Functor M] [Pure M] (modifier : Lean.Expr → M Lean.Expr) : Lean.Expr → M Lean.Expr

def Lean.Expr.modifyAppArg (modifier : Lean.Expr → Lean.Expr) : Lean.Expr → Lean.Expr

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

Equations

• Lean.Expr.modifyRevArg modifier 0 = Lean.Expr.modifyAppArg modifier
• Lean.Expr.modifyRevArg modifier (Nat.succ i) = Lean.Expr.modifyAppArg (Lean.Expr.modifyRevArg modifier i)

def Lean.Expr.modifyArg (modifier : Lean.Expr → Lean.Expr) (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) : Lean.Expr

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

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

def Lean.Expr.getArg? (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) : Option Lean.Expr

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

def Lean.Expr.modifyArgM {M : Type → Type u_1} [Monad M] (modifier : Lean.Expr → M Lean.Expr) (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) : M Lean.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 : Lean.Expr) (old : Lean.Name) (new : Lean.Name) : Lean.Expr

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

Equations

• Lean.Expr.renameBVar (Lean.Expr.app fn arg) old new = Lean.Expr.app (Lean.Expr.renameBVar fn old new) (Lean.Expr.renameBVar arg old new)
• Lean.Expr.renameBVar (Lean.Expr.lam n ty bd bi) old new = Lean.Expr.lam (if (n == old) = true then new else n) (Lean.Expr.renameBVar ty old new) (Lean.Expr.renameBVar bd old new) bi
• Lean.Expr.renameBVar (Lean.Expr.forallE n ty bd bi) old new = Lean.Expr.forallE (if (n == old) = true then new else n) (Lean.Expr.renameBVar ty old new) (Lean.Expr.renameBVar bd old new) bi
• Lean.Expr.renameBVar e old new = e

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

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

def Lean.Expr.addLocalVarInfoForBinderIdent (fvar : Lean.Expr) (tk : Lean.TSyntax `Lean.binderIdent) : Lean.MetaM Unit

Annotates a binderIdent with the binder information from an fvar.

def Lean.Expr.mkDirectProjection (e : Lean.Expr) (fieldName : Lean.Name) : Lean.MetaM Lean.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 : Lean.Expr) (fieldName : Lean.Name) : Lean.MetaM Lean.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.containsConst (e : Lean.Expr) (p : Lean.Name → Bool) : Bool

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

def Lean.Expr.rewrite (e : Lean.Expr) (eq : Lean.Expr) : Lean.MetaM Lean.Expr

Rewrites e via some eq, producing a proof e = e' for some e'.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

def Lean.Expr.rewriteType (e : Lean.Expr) (eq : Lean.Expr) : Lean.MetaM Lean.Expr

Rewrites the type of e via some eq, then moves e into the new type via Eq.mp.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

def Lean.ConstantInfo.getUsedConstants (c : Lean.ConstantInfo) : Lean.NameSet

Return all names appearing in the type or value of a ConstantInfo.

def Lean.getFieldsToParents (env : Lean.Environment) (structName : Lean.Name) : Array Lean.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.

def Lean.Environment.getModuleFor? (env : Lean.Environment) (declName : Lean.Name) : Option Lean.Name

Return the name of the module in which a declaration was defined.

def Lean.Name.requiredModules (n : Lean.Name) : Lean.CoreM Lean.NameSet

Return the names of the modules in which constants used in the specified declaration were defined.

Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

def Lean.Environment.requiredModules (env : Lean.Environment) : Lean.NameSet

Return the names of the modules in which constants used in the current file were defined.

Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.