Documentation

Lean.Util.ForEachExpr

Remark: we cannot use the caching trick used at FindExpr and ReplaceExpr because they may visit the same expression multiple times if they are stored in different memory addresses. Note that the following code is parametric in a monad m.

partial def Lean.ForEachExpr.visit {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (g : Lean.Exprm Bool) (e : Lean.Expr) :
@[inline]
def Lean.Expr.forEach' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Exprm Bool) :

Apply f to each sub-expression of e. If f t returns false, then t's children are not visited.

Equations
Instances For
    @[inline]
    def Lean.Expr.forEach {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Exprm Unit) :
    Equations
    Instances For