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`.

source
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 PUnit.unit

Instances For

source
@[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

Instances For

source
@[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

Instances For