structure Lean.Expr.FoldConstsImpl.State : Type

• visited : PtrSet Expr
• visitedConsts : NameHashSet

@[reducible, inline]

unsafe abbrev Lean.Expr.FoldConstsImpl.FoldM (α : Type) : Type

unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Name → α → α) (e : Expr) (acc : α) : FoldM α

unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Name → α → α) (e : Expr) (acc : α) : FoldM α

@[inline]

unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α

@[implemented_by Lean.Expr.FoldConstsImpl.foldUnsafe]

opaque Lean.Expr.foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α

Apply f to every constant occurring in e once.

def Lean.Expr.getUsedConstants (e : Expr) : Array Name

def Lean.Expr.getUsedConstantsAsSet (e : Expr) : NameSet

Like Expr.getUsedConstants, but produce a NameSet.

def Lean.ConstantInfo.getUsedConstantsAsSet (c : ConstantInfo) : NameSet

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