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

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

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 (Lean.Name.updatePrefix s 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 | Lean.Name.str n s => Lean.Name.str n (f s) | n => n

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.

Equations

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

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

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

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

• One or more equations did not get rendered due to their size.
• Lean.Name.isPrefixOf? pre Lean.Name.anonymous = if (pre == Lean.Name.anonymous) = true then some Lean.Name.anonymous else none

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

• Lean.ConstantInfo.isDef x = 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

• Lean.ConstantInfo.isThm x = 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

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

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

Update the type of a ConstantInfo.

Equations

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

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

Update the level parameters of a ConstantInfo.

Equations

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

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

• Lean.Expr.bvarIdx? x = 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

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

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

Equations

• Lean.Expr.fvarId? x = 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

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

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

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

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

• Lean.Expr.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

• Lean.Expr.ofInt α x = match x with | Int.ofNat n => Lean.Expr.ofNat α n | Int.negSucc n => do let __do_lift ← Lean.Expr.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

• Lean.Expr.zero? e = match Lean.Expr.numeral? e 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

• Lean.Expr.ne?' e = HOrElse.hOrElse (Lean.Expr.ne? e) fun (x : Unit) => Lean.Expr.not? e >>= 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

• Lean.Expr.le? p = do let __discr ← Lean.Expr.app4? p `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_1} [Functor M] [Pure M] (modifier : Lean.Expr → M Lean.Expr) : Lean.Expr → M Lean.Expr

Equations

• Lean.Expr.modifyAppArgM modifier x = match x with | Lean.Expr.app f 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 (Lean.Expr.app f x_2) = Lean.Expr.app f (modifier x_2)
• Lean.Expr.modifyRevArg modifier (Nat.succ i) (Lean.Expr.app f x_2) = Lean.Expr.app (Lean.Expr.modifyRevArg modifier i f) 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 (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.

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 (Lean.Expr.getAppNumArgs e)) : 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

• Lean.Expr.setArg e 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

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

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.

Equations

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

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.

Equations

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

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.

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

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

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

• Lean.Expr.rewriteType e eq = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← Lean.Expr.rewrite __do_lift 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

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

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

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