# Documentation

Mathlib.Lean.Expr.Basic

# 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#

The brackets corresponding to a given BinderInfo.

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

### Declarations about 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.

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.

Equations

Auxiliary for Name.fromComponents

Equations

Update the last component of a name.

Equations

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

Equations
def Lean.Name.splitAt (nm : Lean.Name) (n : Nat) :

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≥ n). Example: splitAt foo.bar.baz.back.bat 1 = (foo.bar.baz.back, bat).

Equations
• = match with | (nm2, nm1) =>

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 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.

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

Checks whether this ConstantInfo is a definition,

Equations
• = match x with | => true | x => false

Checks whether this ConstantInfo is a theorem,

Equations
• = match x with | => true | x => false

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

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

Update the name of a ConstantInfo.

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

Update the type of a ConstantInfo.

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

Update the level parameters of a ConstantInfo.

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

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

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

Turn a ConstantInfo into a declaration.

Equations
• One or more equations did not get rendered due to their size.
def Lean.mkConst' (constName : Lean.Name) :

Same as mkConst, but with fresh level metavariables.

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

### Declarations about Expr#

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

Equations
Equations
• = match x with | => some idx | x => none

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

Equations

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

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

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

Equations
• = match x with | => some n | x => none

isConstantApplication e checks whether e is syntactically an application of the form (fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ⋯ xₙ => H) y₁ ⋯ 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ₙ.

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

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

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

Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.ofNat (α : Lean.Expr) (n : Nat) :

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

Equations

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

Equations
partial def Lean.Expr.numeral? (e : Lean.Expr) :

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

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

Equations
def Lean.Expr.modifyAppArgM {M : TypeType u_1} [inst : ] [inst : Pure M] (modifier : ) :
Equations
def Lean.Expr.modifyArg (modifier : ) (e : Lean.Expr) (i : Nat) (n : ) :

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

Equations
Equations
def Lean.Expr.getArg? (e : Lean.Expr) (i : Nat) (n : ) :

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

Equations
def Lean.Expr.modifyArgM {M : TypeType u_1} [inst : ] (modifier : ) (e : Lean.Expr) (i : Nat) (n : ) :

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.

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

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

Equations

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

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

Annotates a binderIdent with the binder information from an fvar.

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

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

Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.mkProjection (e : Lean.Expr) (fieldName : Lean.Name) :

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

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

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.

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