# Documentation

Mathlib.Lean.Expr.Traverse

# Traversal functions for expressions. #

def Lean.Expr.traverseChildren {M : TypeType u_1} [inst : ] (f : ) :

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 : TypeType u_1} [inst : ] (f : αLean.Exprm α) (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