partial def
Lean.ForEachExpr.visit
{ω : Type}
{m : Type → Type}
[inst : STWorld ω m]
[inst : MonadLiftT (ST ω) m]
[inst : Monad m]
(g : Lean.Expr → m Bool)
(e : Lean.Expr)
:
@[inline]
def
Lean.Expr.forEach'
{ω : Type}
{m : Type → Type}
[inst : STWorld ω m]
[inst : MonadLiftT (ST ω) m]
[inst : 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
@[inline]
def
Lean.Expr.forEach
{ω : Type}
{m : Type → Type}
[inst : STWorld ω m]
[inst : MonadLiftT (ST ω) m]
[inst : 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