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.

def Lean.ForEachExpr.visit {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.ForEachExpr.visit g e = Lean.checkCache e fun (x : Unit) => do let __do_lift ← liftM (g e) if __do_lift = true then pure () else pure ()

@[inline]

def Lean.Expr.forEach' {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) (f : 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

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

@[inline]

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

Equations

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