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
#
The brackets corresponding to a given BinderInfo
.
Instances For
Declarations about 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.
Instances For
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
Instances For
Get the last field of a name as a string. Doesn't raise an error when the last component is a numeric field.
Instances For
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
- 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')
Instances For
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
transform proof_1
constants generated by Lean.Meta.mkAuxDefinitionFor
.
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 test/lean/run/printDecls
.
Instances For
Instances For
The union of two NameSet
s.
Instances For
Checks whether this ConstantInfo
is a definition,
Instances For
Checks whether this ConstantInfo
is a theorem,
Instances For
Update ConstantVal
(the data common to all constructors of ConstantInfo
)
in a ConstantInfo
.
Instances For
Update the name of a ConstantInfo
.
Instances For
Update the type of a ConstantInfo
.
Instances For
Update the level parameters of a ConstantInfo
.
Instances For
Update the value of a ConstantInfo
, if it has one.
Instances For
Turn a ConstantInfo
into a declaration.
Instances For
Same as mkConst
, but with fresh level metavariables.
Instances For
Declarations about Expr
#
If the expression is a constant, return that name. Otherwise return Name.anonymous
.
Instances For
Like Expr.getUsedConstants
, but produce a NameSet
.
Instances For
Turn an expression that is a natural number literal into a natural number.
Instances For
Turn an expression that is a constructor of Int
applied to a natural number literal
into an integer.
Instances For
Check if an expression is an "integer in normal form", i.e. either a natural number in normal form, or the negation of one, and if so returns the integer.
Instances For
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.
Instances For
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 asn
is a literal. - An "integer in normal form" is an expression which is either a natural number in number form,
or
-n
, wheren
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
wheren
is an integer in normal form,d
is a natural number in normal form,d ≠ 1
, andn
andd
are coprime (in particular, we check that(mkRat n d).den = d
).
Equations
Instances For
If an Expr
has form .fvar n
, then returns some n
, otherwise none
.
Instances For
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ₙ
.
Instances For
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
Instances For
Check that an expression contains no metavariables (after instantiation).
Instances For
Construct the term of type α
for a given natural number
(doing typeclass search for the OfNat
instance required).
Instances For
Return some n
if e
is one of the following
- A nat literal (numeral)
Nat.zero
Nat.succ x
whereisNumeral x
OfNat.ofNat _ x _
whereisNumeral x
Test if an expression is either Nat.zero
, or OfNat.ofNat 0
.
Instances For
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
.
Instances For
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?
.
Instances For
Equations
- Lean.Expr.modifyRevArg modifier 0 = Lean.Expr.modifyAppArg modifier
- Lean.Expr.modifyRevArg modifier (Nat.succ i) = Lean.Expr.modifyAppArg (Lean.Expr.modifyRevArg modifier i)
Instances For
Given f a₀ a₁ ... aₙ₋₁
, runs modifier
on the i
th argument or
returns the original expression if out of bounds.
Instances For
Given f a₀ a₁ ... aₙ₋₁
, returns the i
th argument or none if out of bounds.
Instances For
Given f a₀ a₁ ... aₙ₋₁
, runs modifier
on the i
th argument.
An argument n
may be provided which says how many arguments we are expecting e
to have.
Instances For
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
Instances For
getBinderName e
returns some n
if e
is an expression of the form ∀ n, ...
and none
otherwise.
Instances For
Annotates a binderIdent
with the binder information from an fvar
.
Instances For
If e
has a structure as type with field fieldName
, mkDirectProjection e fieldName
creates
the projection expression e.fieldName
Instances For
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
Instances For
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.
Instances For
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.
Instances For
Return all names appearing in the type or value of a ConstantInfo
.
Instances For
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.
Instances For
Return the name of the module in which a declaration was defined.
Instances For
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.
Instances For
Return the names of the modules in which constants used in the current file were defined.
Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.