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.

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