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.

Equations

• x.brackets = match x with | Lean.BinderInfo.implicit => ("{", "}") | Lean.BinderInfo.strictImplicit => ("{{", "}}") | Lean.BinderInfo.instImplicit => ("[", "]") | x => ("(", ")")

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.

Equations

• Lean.Name.fromComponents = Lean.Name.fromComponents.go Lean.Name.anonymous

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 (s.updatePrefix x) rest

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

Update the last component of a name.

Equations

• Lean.Name.updateLast f x = match x with | n.str s => n.str (f s) | n => n

def Lean.Name.lastComponentAsString : 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.

Equations

• x.lastComponentAsString = match x with | pre.str s => s | pre.num n => toString n | Lean.Name.anonymous => ""

@[deprecated Lean.Name.lastComponentAsString]

def Lean.Name.getString : Lean.Name → String

Alias of Lean.Name.lastComponentAsString.

---

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

Equations

• Lean.Name.getString = Lean.Name.lastComponentAsString

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

Equations

• nm.splitAt n = match List.splitAt n nm.componentsRev with | (nm2, nm1) => (Lean.Name.fromComponents nm1.reverse, Lean.Name.fromComponents nm2.reverse)

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

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

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

Equations

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

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

Checks whether this ConstantInfo is a definition,

Equations

• x.isDef = match x with | Lean.ConstantInfo.defnInfo val => true | x => false

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

Checks whether this ConstantInfo is a theorem,

Equations

• x.isThm = match x with | Lean.ConstantInfo.thmInfo val => true | x => false

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

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.

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

Update the name of a ConstantInfo.

Equations

• c.updateName name = c.updateConstantVal (let __src := c.toConstantVal; { name := name, levelParams := __src.levelParams, type := __src.type })

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

Update the type of a ConstantInfo.

Equations

• c.updateType type = c.updateConstantVal (let __src := c.toConstantVal; { name := __src.name, levelParams := __src.levelParams, type := type })

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

Update the level parameters of a ConstantInfo.

Equations

• c.updateLevelParams levelParams = c.updateConstantVal (let __src := c.toConstantVal; { name := __src.name, levelParams := levelParams, type := __src.type })

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

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

Equations

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

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

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

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

Equations

• x.bvarIdx? = match x with | Lean.Expr.bvar idx => some idx | x => none

@[inline]

def Lean.Expr.getAppApps (e : Lean.Expr) : Array Lean.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

• e.getAppApps = let dummy := Lean.mkSort Lean.levelZero; let nargs := e.getAppNumArgs; Lean.Expr.getAppAppsAux e (mkArray nargs dummy) (nargs - 1)

def Lean.Expr.eraseProofs (e : Lean.Expr) : Lean.MetaM Lean.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.

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

Equations

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

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.lit a).isExplicitNumber = true
• (Lean.Expr.mdata data e).isExplicitNumber = e.isExplicitNumber
• x.isExplicitNumber = x.rat?.isSome

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

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

Equations

• x.fvarId? = match x with | Lean.Expr.fvar n => some n | x => none

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

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

Equations

• x.type? = match x with | Lean.Expr.sort u => u.dec | x => 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ₙ.

Equations

• e.isConstantApplication = (e.isApp && Lean.Expr.isConstantApplication.aux e.getAppNumArgs'.pred e.getAppFn' e.getAppNumArgs')

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.letE declName type value b nonDep).letDepth = b.letDepth + 1
• x.letDepth = 0

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

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

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

Equations

• α.ofNat n = Lean.Meta.mkAppOptM `OfNat.ofNat #[some α, some (Lean.mkRawNatLit n), none]

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

Equations

• α.ofInt x = match x with | Int.ofNat n => α.ofNat n | Int.negSucc n => do let __do_lift ← α.ofNat (n + 1) Lean.Meta.mkAppM `Neg.neg #[__do_lift]

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.

Equations

• e.zero? = match e.numeral? with | some 0 => true | x => false

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

Equations

• e.ne?' = HOrElse.hOrElse e.ne? fun (x : Unit) => e.not? >>= Lean.Expr.eq?

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

Equations

• p.le? = do let __discr ← p.app4? `LE.le match __discr with | (type, fst, lhs, rhs) => pure (type, lhs, rhs)

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

Equations

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

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

Equations

• Lean.Expr.modifyAppArgM modifier x = match x with | f.app a => Lean.mkApp f <$> modifier a | e => pure e

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

Equations

• Lean.Expr.modifyRevArg modifier 0 (f.app x_2) = f.app (modifier x_2)
• Lean.Expr.modifyRevArg modifier i.succ (f.app x_2) = (Lean.Expr.modifyRevArg modifier i f).app x_2
• Lean.Expr.modifyRevArg modifier x✝ x = x

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

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

Equations

• Lean.Expr.modifyArg modifier e i n = Lean.Expr.modifyRevArg modifier (n - i - 1) e

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

• e.setArg i x n = Lean.Expr.modifyArg (fun (x_1 : Lean.Expr) => x) e i n

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

Equations

• x✝.getRevArg? x = match x✝, x with | fn.app a, 0 => some a | f.app arg, i.succ => some (f.getRevArg! i) | x, x_1 => none

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

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

Equations

• e.getArg? i n = e.getRevArg? (n - i - 1)

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

Equations

• Lean.Expr.modifyArgM modifier e i n = match e.getArg? i with | some a => do let a ← modifier a pure (Lean.Expr.modifyArg (fun (x : Lean.Expr) => a) e i n) | x => pure e

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

• (fn.app arg).renameBVar old new = (fn.renameBVar old new).app (arg.renameBVar old new)
• (Lean.Expr.lam n ty bd bi).renameBVar old new = Lean.Expr.lam (if (n == old) = true then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
• (Lean.Expr.forallE n ty bd bi).renameBVar old new = Lean.Expr.forallE (if (n == old) = true then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
• e.renameBVar 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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

def Lean.Expr.reduceProjStruct? (e : Lean.Expr) : Lean.MetaM (Option Lean.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.

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.

Equations

• e.containsConst p = (Lean.Expr.find? (fun (x : Lean.Expr) => match x with | Lean.Expr.const n us => p n | x => false) e).isSome

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.

Equations

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

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.

Equations

• e.rewriteType eq = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← __do_lift.rewrite eq Lean.Meta.mkEqMP __do_lift e

def Lean.Expr.forallNot_of_notExists (ex : Lean.Expr) (hNotEx : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.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

• ex.forallNot_of_notExists hNotEx = match ex with | ((Lean.Expr.const `Exists [lvl]).app A).app p => Lean.Expr.forallNot_of_notExists.go lvl A p hNotEx | x => failure

partial def Lean.Expr.forallNot_of_notExists.go (lvl : Lean.Level) (A : Lean.Expr) (p : Lean.Expr) (hNotEx : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.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.

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.

Equations

• Lean.getFieldsToParents env structName = Array.filter (fun (fieldName : Lean.Name) => (Lean.isSubobjectField? env structName fieldName).isSome) (Lean.getStructureFields env structName)