source
structure Lean.Expr.FoldConstsImpl.State :
Type

- visited : PtrSet Expr
- visitedConsts : NameHashSet

Instances For

source
@[reducible, inline]
unsafe abbrev Lean.Expr.FoldConstsImpl.FoldM (α : Type) :
Type
Equations

- Lean.Expr.FoldConstsImpl.FoldM = StateM Lean.Expr.FoldConstsImpl.State

Instances For

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

- Lean.Expr.FoldConstsImpl.fold f e acc = Lean.Expr.FoldConstsImpl.fold.visit✝ f e acc

Instances For

source
@[inline]
unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Expr) (init : α) (f : Name → α → α) :
α
Equations

- Lean.Expr.FoldConstsImpl.foldUnsafe e init f = StateT.run' (Lean.Expr.FoldConstsImpl.fold f e init) { }

Instances For

source
@[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.

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

- e.getUsedConstants = e.foldConsts #[] fun (c : Lean.Name) (cs : Array Lean.Name) => cs.push c

Instances For

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

Like `Expr.getUsedConstants`, but produce a `NameSet`.

Equations

- e.getUsedConstantsAsSet = e.foldConsts ∅ fun (c : Lean.Name) (cs : Lean.NameSet) => cs.insert c

Instances For

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

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.
- c.getUsedConstantsAsSet = c.type.getUsedConstantsAsSet ++ match c.value? with | some v => v.getUsedConstantsAsSet | none => ∅

Instances For