# Documentation

Lean.Util.FoldConsts

@[inline]
Equations
Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lean.Nameαα) (size : USize) (e : Lean.Expr) (acc : α) :
Equations
unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lean.Nameαα) (size : USize) (e : Lean.Expr) (acc : α) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Nameαα) :
α
Equations
@[implemented_by Lean.Expr.FoldConstsImpl.foldUnsafe]
opaque Lean.Expr.foldConsts {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Nameαα) :
α

Apply f to every constant occurring in e once.

Equations
Equations
• One or more equations did not get rendered due to their size.