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 : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (g : Lean.Expr → m Bool) (e : Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit m Unit

@[inline]

def Lean.Expr.forEach' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Expr → m Bool) : m Unit

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

Equations

• Lean.Expr.forEach' e f = Lean.MonadCacheT.run (Lean.ForEachExpr.visit f e)

@[inline]

def Lean.Expr.forEach {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Expr → m Unit) : m Unit

Equations

• Lean.Expr.forEach e f = Lean.Expr.forEach' e fun e => do f e pure true