Documentation

Lean.Util.ForEachExpr

partial def Lean.ForEachExpr.visit {ω : Type} {m : TypeType} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (g : Lean.Exprm Bool) (e : Lean.Expr) :
@[inline]
def Lean.Expr.forEach' {ω : Type} {m : TypeType} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (e : Lean.Expr) (f : Lean.Exprm Bool) :
Equations
@[inline]
def Lean.Expr.forEach {ω : Type} {m : TypeType} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (e : Lean.Expr) (f : Lean.Exprm Unit) :
Equations