structure Lean.Expr.NumApps.State : Type

• visited : Lean.PtrSet Lean.Expr
• counters : Lean.NameMap Nat

@[reducible, inline]

unsafe abbrev Lean.Expr.NumApps.M (α : Type) : Type

Equations

• Lean.Expr.NumApps.M = StateM Lean.Expr.NumApps.State

unsafe def Lean.Expr.NumApps.visit (e : Lean.Expr) : Lean.Expr.NumApps.M Unit

Equations

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

unsafe def Lean.Expr.NumApps.main (e : Lean.Expr) : Lean.NameMap Nat

Equations

• Lean.Expr.NumApps.main e = match StateT.run (Lean.Expr.NumApps.visit e) { visited := Lean.mkPtrSet, counters := ∅ } with | (fst, s) => s.counters

def Lean.Expr.numApps (e : Lean.Expr) (threshold : Nat := 0) : IO (Array (Lean.Name × Nat))

Returns the number of applications for each declaration used in e.

This operation is performed in IO because the result depends on the memory representation of the object.

Note: Use this function primarily for diagnosing performance issues.

Equations

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