Documentation

Mathlib.Lean.Expr.Traverse

Traversal functions for expressions. #

def Lean.Expr.traverseChildren {M : TypeType u_1} [inst : Applicative M] (f : Lean.ExprM 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 : TypeType u_1} [inst : Monad m] (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