Similar to traverseLambda
but with an additional pos argument to track position.
Equations
Instances For
Equations
Instances For
Similar to traverseForall
but with an additional pos argument to track position.
Equations
Instances For
Equations
Instances For
Similar to traverseLet
but with an additional pos argument to track position.
Equations
Instances For
Equations
Instances For
Similar to Lean.Meta.traverseChildren
except that visit
also includes a Pos
argument so you can
track the subexpression position.
Equations
Instances For
Given an expression fun (x₁ : α₁) ... (xₙ : αₙ) => b
, will run
f
on each of the variable types αᵢ
and b
with the correct MetaM context,
replacing each expression with the output of f
and creating a new lambda.
(that is, correctly instantiating bound variables and repackaging them after)
Equations
Instances For
Given an expression (x₁ : α₁) → ... → (xₙ : αₙ) → b
, will run
f
on each of the variable types αᵢ
and b
with the correct MetaM context,
replacing the expression with the output of f
and creating a new forall expression.
(that is, correctly instantiating bound variables and repackaging them after)
Equations
Instances For
Similar to traverseLambda
and traverseForall
but with let binders.
Equations
Instances For
Maps visit
on each child of the given expression.
Applications, foralls, lambdas and let binders are bundled (as they are bundled in Expr.traverseApp
, traverseForall
, ...).
So traverseChildren f e
where e = `(fn a₁ ... aₙ)
will return
(← f `(fn)) (← f `(a₁)) ... (← f `(aₙ))
rather than (← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))
See also Lean.Core.traverseChildren
.