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
.
Equations
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.
Equations
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.
Equations
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
Instances For
Checks whether this ConstantInfo
is a definition.
Equations
Instances For
Checks whether this ConstantInfo
is a theorem.
Equations
Instances For
Update ConstantVal
(the data common to all constructors of ConstantInfo
)
in a ConstantInfo
.
Equations
Instances For
Update the name of a ConstantInfo
.
Equations
Instances For
Update the type of a ConstantInfo
.
Equations
Instances For
Update the level parameters of a ConstantInfo
.
Equations
Instances For
Update the value of a ConstantInfo
, if it has one.
Equations
Instances For
Turn a ConstantInfo
into a declaration.
Equations
Instances For
Same as mkConst
, but with fresh level metavariables.
Equations
Instances For
Declarations about 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
Instances For
Erase proofs in an expression by replacing them with sorry
s.
This function replaces all proofs in the expression
and in the types that appear in the expression
by sorryAx
s.
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
Instances For
If an Expr
has the form Type u
, then return some u
, otherwise none
.
Equations
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ₙ
.
Equations
Instances For
Counts the immediate depth of a nested let
expression.
Equations
Instances For
Check that an expression contains no metavariables (after instantiation).
Equations
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
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
Instances For
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
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?
.
Equations
Instances For
Given f a₀ a₁ ... aₙ₋₁
, runs modifier
on the i
th argument or
returns the original expression if out of bounds.
Equations
Instances For
Given f a₀ a₁ ... aₙ₋₁
, sets the argument on the i
th argument to x
or
returns the original expression if out of bounds.
Equations
Instances For
Given f a₀ a₁ ... aₙ₋₁
, returns the i
th argument or none if out of bounds.
Equations
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.
Equations
Instances For
Traverses an expression e
and renames bound variables named old
to new
.
Equations
Instances For
getBinderName e
returns some n
if e
is an expression of the form ∀ n, ...
and none
otherwise.
Equations
Instances For
If e
has a structure as type with field fieldName
, mkDirectProjection e fieldName
creates
the projection expression e.fieldName
Equations
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
Equations
Instances For
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
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.
Equations
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.