Traversal functions for expressions.

def Lean.Expr.traverseChildren {M : Type → Type u_1} [Applicative M] (f : Lean.Expr → M Lean.Expr) : Lean.Expr → M Lean.Expr

Maps f on each immediate child of the given expression.

def Lean.Expr.foldlM {α : Type} {m : Type → Type u_1} [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.