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

Instances For

### 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.
Instances For

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.

Instances For

Auxiliary for Name.fromComponents

Equations
Instances For

Update the last component of a name.

Instances For

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

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

Instances For

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
Instances For

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.

Instances For
def Lean.Name.isBlackListed {m : } [] [] (declName : Lean.Name) :
Instances For

The union of two NameSets.

Instances For

Checks whether this ConstantInfo is a definition,

Instances For

Checks whether this ConstantInfo is a theorem,

Instances For

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

Instances For

Update the name of a ConstantInfo.

Instances For

Update the type of a ConstantInfo.

Instances For

Update the level parameters of a ConstantInfo.

Instances For

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

Instances For

Turn a ConstantInfo into a declaration.

Instances For
def Lean.mkConst' (constName : Lean.Name) :

Same as mkConst, but with fresh level metavariables.

Instances For

### Declarations about Expr#

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

Instances For
Instances For

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

Instances For

Like Expr.getUsedConstants, but produce a NameSet.

Instances For

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

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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
Instances For

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

Instances For

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

Instances For

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

Instances For

Counts the immediate depth of a nested let expression.

Equations
Instances For

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

Instances For
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).

Instances For

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

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

Instances For

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

Instances For
@[inline]

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.

Instances For

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

Instances For
def Lean.Expr.modifyAppArgM {M : TypeType u_1} [] [Pure M] (modifier : ) :
Instances For
def Lean.Expr.modifyAppArg (modifier : ) :
Instances For
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.

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

Instances For
def Lean.Expr.modifyArgM {M : TypeType u_1} [] (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.

Instances For

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

Equations
Instances For

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

Instances For
def Lean.Expr.addLocalVarInfoForBinderIdent (fvar : Lean.Expr) (tk : Lean.TSyntax Lean.binderIdent) :

Annotates a binderIdent with the binder information from an fvar.

Instances For

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

Instances For
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

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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.

Instances For