Traversal functions for expressions. #
def
Lean.Expr.traverseChildren
{M : Type → Type u_1}
[inst : Applicative M]
(f : Lean.Expr → M Lean.Expr)
:
Maps f on each immediate child of the given expression.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Expr.foldlM
{α : Type}
{m : Type → Type u_1}
[inst : Monad m]
(f : α → Lean.Expr → m α)
(x : α)
(e : Lean.Expr)
:
m α
e.foldlM f a folds the monadic function f over the subterms of the expression e,
with initial value a.
Equations
- Lean.Expr.foldlM f x e = Prod.snd <$> StateT.run (Lean.Expr.traverseChildren (fun e' => Functor.mapConst e' (get >>= monadLift ∘ flip f e' >>= set)) e) x