Documentation

Mathlib.Lean.Expr.Traverse

Traversal functions for expressions. #

Maps f on each immediate child of the given expression.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Lean.Expr.foldlM {α : Type} {m : TypeType u_1} [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
    • One or more equations did not get rendered due to their size.
    Instances For