structure Lean.Expr.NumApps.State : Type

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

@[reducible, inline]

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

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

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

def Lean.Expr.numApps (e : Lean.Expr) (threshold : optParam Nat 0) : IO (Array (Lake.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.