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 #

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

The brackets corresponding to a given BinderInfo.

Equations

Declarations about name #

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

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
source
def Lean.Name.fromComponents.go :
Name → List Name → Name

Auxiliary for Name.fromComponents

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

Update the last component of a name.

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

Equations
source
def Lean.Name.splitAt (nm : Name) (n : Nat) :
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).

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

Equations
source
def Lean.Name.isBlackListed {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) :
m Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.ConstantInfo.isDef :
ConstantInfo → Bool

Checks whether this ConstantInfo is a definition.

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

Checks whether this ConstantInfo is a theorem.

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

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

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

Update the name of a ConstantInfo.

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

Update the type of a ConstantInfo.

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

Update the level parameters of a ConstantInfo.

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

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

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

Turn a ConstantInfo into a declaration.

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

Same as mkConst, but with fresh level metavariables.

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

Declarations about Expr #

source
def Lean.Expr.bvarIdx? :
Expr → Option Nat
Equations
source
@[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.

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Expr.type? :
Expr → Option Level

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

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

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

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

source
def Lean.Expr.letDepth :
Expr → Nat

Counts the immediate depth of a nested let expression.

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

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

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

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

Equations
source
def Lean.Expr.ofInt (α : Expr) :
Int → MetaM Expr

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

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

Return some n if e is one of the following

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

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

Equations
source
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).

Equations
source
@[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.

Equations
source
@[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.

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Expr.modifyAppArgM {M : Type → Type u} [Functor M] [Pure M] (modifier : Expr → M Expr) :
Expr → M Expr
Equations
source
def Lean.Expr.modifyRevArg (modifier : Expr → Expr) :
Nat → Expr → Expr
Equations
source
def Lean.Expr.modifyArg (modifier : Expr → Expr) (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs) :
Expr

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

Equations
source
def Lean.Expr.setArg (e : Expr) (i : Nat) (x : Expr) (n : Nat := 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.

Equations
source
def Lean.Expr.getRevArg? :
Expr → Nat → Option Expr
Equations
source
def Lean.Expr.getArg? (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs) :
Option Expr

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

Equations
source
def Lean.Expr.modifyArgM {M : Type → Type u} [Monad M] (modifier : Expr → M Expr) (e : Expr) (i : Nat) (n : Nat := 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.

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Expr.addLocalVarInfoForBinderIdent (fvar : Expr) (tk : TSyntax `Lean.binderIdent) :
MetaM Unit

Annotates a binderIdent with the binder information from an fvar.

Equations
  • One or more equations did not get rendered due to their size.
source
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

Equations
  • One or more equations did not get rendered due to their size.
source
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

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Expr.containsConst (e : Expr) (p : Name → Bool) :
Bool

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

Equations
source
def Lean.Expr.rewrite (e eq : Expr) :
MetaM 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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Expr.rewriteType (e eq : Expr) :
MetaM 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.

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

Equations
source
partial def Lean.Expr.forallNot_of_notExists.go (lvl : Level) (A p hNotEx : Expr) :
MetaM (Expr × Expr)

Given (hNotEx : Not (@Exists.{lvl} A p)), return a forall x, Not (p x) and a proof for it.

This function handles nested existentials.

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

Equations