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.
nm.splitAt n splits a name
nm in two parts, such that the second part has depth
(nm.splitAt n).2.getNumParts = n (assuming
nm.getNumParts ≥ n).
splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat).
isPrefixOf? pre nm returns
some post if
nm = pre ++ post.
Note that this includes the case where
nm has multiple more namespaces.
pre is not a prefix of
nm, it returns
- Lean.Name.isPrefixOf? pre Lean.Name.anonymous = if (pre == Lean.Name.anonymous) = true then some Lean.Name.anonymous else none
- Lean.Name.isPrefixOf? pre (Lean.Name.num p' a) = if (pre == Lean.Name.num p' a) = true then some Lean.Name.anonymous else Option.map (fun x => Lean.Name.num x a) (Lean.Name.isPrefixOf? pre p')
- Lean.Name.isPrefixOf? pre (Lean.Name.str p' s) = if (pre == Lean.Name.str p' s) = true then some Lean.Name.anonymous else Option.map (fun x => Lean.Name.str x s) (Lean.Name.isPrefixOf? pre p')
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
proof_1 constants generated by
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
Check if an expression is a "rational in normal form",
i.e. either an integer number in normal form,
n / d where
n is an integer in normal form,
d is a natural number in normal form,
d ≠ 1, and
d are coprime (in particular, we check that
(mkRat n d).den = d).
If so returns the rational number.
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
nis a literal.
- An "integer in normal form" is an expression which is either a natural number in number form,
nis a natural number in normal form.
- A "rational in normal form" is an expressions which is either an integer in normal form,
n / dwhere
nis an integer in normal form,
dis a natural number in normal form,
d ≠ 1, and
dare coprime (in particular, we check that
(mkRat n d).den = d).
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
f a₀ a₁ ... aₙ₋₁, runs
modifier on the
n may be provided which says how many arguments we are expecting
e to have.
Traverses an expression
e and renames bound variables named
- 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
Get the projections that are projections to parent structures. Similar to
except that this returns the (last component of the) projection names instead of the parent names.
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.