Documentation

Lean.Util.FoldConsts

@[reducible, inline]
unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lean.Nameαα) (e : Lean.Expr) (acc : α) :
unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lean.Nameαα) (e : Lean.Expr) (acc : α) :
@[inline]
unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Nameαα) :
α
@[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.

Like Expr.getUsedConstants, but produce a NameSet.

Equations

Return all names appearing in the type or value of a ConstantInfo.

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