- done: Lean.Expr → Lean.TransformStep
Return expression without visiting any subexpressions.
- visit: Lean.Expr → Lean.TransformStep
Visit expression (which should be different from current expression) instead. The new expression
eis passed to
- continue: optParam (Option Lean.Expr) none → Lean.TransformStep
Continue transformation with the given expression (defaults to current expression). For
pre, this means visiting the children of the expression. For
post, this is equivalent to returning
Transform the expression
preis invoked with the current expression and recursion is continued according to the
TransformStepresult. In all cases, the expression contained in the result, if any, must be definitionally equal to the current expression.
- After recursion, if any,
postis invoked on the resulting expression.
s in both
pre s and
post s may contain loose bound variables. So, this method is not appropriate for
if one needs to apply operations (e.g.,
inferType) that do not handle loose bound variables.
Meta.transform to avoid loose bound variables.
This method is useful for applying transformations such as beta-reduction and delta-reduction.
Core.transform, but terms provided to
post do not contain loose bound variables.
So, it is safe to use any
MetaM method at