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 : BinderInfo → String × String

The brackets corresponding to a given BinderInfo.

Equations

• Lean.BinderInfo.implicit.brackets = ("{", "}")
• Lean.BinderInfo.strictImplicit.brackets = ("{{", "}}")
• Lean.BinderInfo.instImplicit.brackets = ("[", "]")
• x✝.brackets = ("(", ")")

Declarations about name

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.

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

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

def Lean.Name.fromComponents.go : Name → List Name → 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) : Name → Name

Update the last component of a name.

Equations

• Lean.Name.updateLast f (n.str s) = n.str (f s)
• Lean.Name.updateLast f x✝ = x✝

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

• (pre.str s).lastComponentAsString = s
• (pre.num n).lastComponentAsString = toString n
• Lean.Name.anonymous.lastComponentAsString = ""

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

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

• 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] [MonadEnv m] (declName : Name) : m Bool

Equations

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

def Lean.ConstantInfo.isDef : ConstantInfo → Bool

Checks whether this ConstantInfo is a definition,

Equations

• (Lean.ConstantInfo.defnInfo val).isDef = true
• x✝.isDef = false

def Lean.ConstantInfo.isThm : ConstantInfo → Bool

Checks whether this ConstantInfo is a theorem,

Equations

• (Lean.ConstantInfo.thmInfo val).isThm = true
• x✝.isThm = false

def Lean.ConstantInfo.updateConstantVal : ConstantInfo → ConstantVal → 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.
• (Lean.ConstantInfo.defnInfo info).updateConstantVal x✝ = Lean.ConstantInfo.defnInfo { toConstantVal := x✝, value := info.value, hints := info.hints, safety := info.safety, all := info.all }
• (Lean.ConstantInfo.axiomInfo info).updateConstantVal x✝ = Lean.ConstantInfo.axiomInfo { toConstantVal := x✝, isUnsafe := info.isUnsafe }
• (Lean.ConstantInfo.thmInfo info).updateConstantVal x✝ = Lean.ConstantInfo.thmInfo { toConstantVal := x✝, value := info.value, all := info.all }
• (Lean.ConstantInfo.opaqueInfo info).updateConstantVal x✝ = Lean.ConstantInfo.opaqueInfo { toConstantVal := x✝, value := info.value, isUnsafe := info.isUnsafe, all := info.all }
• (Lean.ConstantInfo.quotInfo info).updateConstantVal x✝ = Lean.ConstantInfo.quotInfo { toConstantVal := x✝, kind := info.kind }

def Lean.ConstantInfo.updateName (c : ConstantInfo) (name : Name) : 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 : ConstantInfo) (type : Expr) : 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 : ConstantInfo) (levelParams : List Name) : 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 : ConstantInfo → Expr → ConstantInfo

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

Equations

• (Lean.ConstantInfo.defnInfo info).updateValue x✝ = Lean.ConstantInfo.defnInfo { toConstantVal := info.toConstantVal, value := x✝, hints := info.hints, safety := info.safety, all := info.all }
• (Lean.ConstantInfo.thmInfo info).updateValue x✝ = Lean.ConstantInfo.thmInfo { toConstantVal := info.toConstantVal, value := x✝, all := info.all }
• (Lean.ConstantInfo.opaqueInfo info).updateValue x✝ = Lean.ConstantInfo.opaqueInfo { toConstantVal := info.toConstantVal, value := x✝, isUnsafe := info.isUnsafe, all := info.all }
• x✝¹.updateValue x✝ = x✝¹

def Lean.ConstantInfo.toDeclaration! : ConstantInfo → Declaration

Turn a ConstantInfo into a declaration.

Equations

• (Lean.ConstantInfo.defnInfo info).toDeclaration! = Lean.Declaration.defnDecl info
• (Lean.ConstantInfo.thmInfo info).toDeclaration! = Lean.Declaration.thmDecl info
• (Lean.ConstantInfo.axiomInfo info).toDeclaration! = Lean.Declaration.axiomDecl info
• (Lean.ConstantInfo.opaqueInfo info).toDeclaration! = Lean.Declaration.opaqueDecl info
• (Lean.ConstantInfo.quotInfo val).toDeclaration! = panicWithPosWithDecl "Mathlib.Lean.Expr.Basic" "Lean.ConstantInfo.toDeclaration!" 152 20 "toDeclaration for quotInfo not implemented"
• (Lean.ConstantInfo.inductInfo val).toDeclaration! = panicWithPosWithDecl "Mathlib.Lean.Expr.Basic" "Lean.ConstantInfo.toDeclaration!" 153 20 "toDeclaration for inductInfo not implemented"
• (Lean.ConstantInfo.ctorInfo val).toDeclaration! = panicWithPosWithDecl "Mathlib.Lean.Expr.Basic" "Lean.ConstantInfo.toDeclaration!" 154 20 "toDeclaration for ctorInfo not implemented"
• (Lean.ConstantInfo.recInfo val).toDeclaration! = panicWithPosWithDecl "Mathlib.Lean.Expr.Basic" "Lean.ConstantInfo.toDeclaration!" 155 20 "toDeclaration for recInfo not implemented"

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

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

Equations

• (Lean.Expr.bvar idx).bvarIdx? = some idx
• x✝.bvarIdx? = none

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

• e.getAppApps = Lean.Expr.getAppAppsAux✝ e (mkArray e.getAppNumArgs (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs - 1)

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.

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

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

Equations

• (Lean.Expr.fvar n).fvarId? = some n
• x✝.fvarId? = none

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

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

Equations

• (Lean.Expr.sort u).type? = u.dec
• x✝.type? = none

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

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

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.

def Lean.Expr.letDepth : 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 : 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.

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

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

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

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

partial def Lean.Expr.numeral? (e : 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 : 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 : 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

• e.ne?' = (e.ne? <|> e.not? >>= Lean.Expr.eq?)

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

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

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

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

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.

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

Equations

• Lean.Expr.modifyAppArgM modifier (f.app a) = Lean.mkApp f <$> modifier a
• Lean.Expr.modifyAppArgM modifier x✝ = pure x✝

def Lean.Expr.modifyRevArg (modifier : Expr → Expr) : Nat → Expr → 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 : 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

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

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

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

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

Equations

• (fn.app a).getRevArg? 0 = some a
• (f.app arg).getRevArg? i.succ = some (f.getRevArg! i)
• x✝¹.getRevArg? x✝ = none

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

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

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

• 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 : Expr) (old new : Name) : 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
• (Lean.Expr.mdata d e').renameBVar old new = Lean.Expr.mdata d (e'.renameBVar old new)
• e.renameBVar old new = e

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.

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.

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.

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.

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.

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

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

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

• (((Lean.Expr.const `Exists [lvl']).app A').app p').forallNot_of_notExists hNotEx = Lean.Expr.forallNot_of_notExists.go lvl' A' p' hNotEx
• ex.forallNot_of_notExists hNotEx = failure

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.

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

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