Documentation

Lean.Meta.ForEachExpr

source
@[inline]
abbrev Lean.Meta.ForEachExpr.M (α : Type) :
Type
Equations
source
partial def Lean.Meta.ForEachExpr.visit (fn : Lean.Expr → Lean.MetaM Bool) (e : Lean.Expr) :
Lean.Meta.ForEachExpr.M Unit
source
def Lean.Meta.forEachExpr' (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Bool) :
Lean.MetaM Unit
Equations
source
def Lean.Meta.forEachExpr (e : Lean.Expr) (f : Lean.Expr → Lean.MetaM Unit) :
Lean.MetaM Unit
Equations