Documentation

Lean.Util.ForEachExpr

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 : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (g : Lean.Exprm Bool) (e : Lean.Expr) :
Instances For
    @[inline]
    def Lean.Expr.forEach' {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Exprm Bool) :

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

    Equations
    Instances For
      @[inline]
      def Lean.Expr.forEach {ω : Type} {m : TypeType} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Lean.Expr) (f : Lean.Exprm Unit) :
      Equations
      Instances For