structure Lean.Expr.NumObjs.State : Type

• visited : Lean.PtrSet Lean.Expr
• counter : Nat

@[reducible, inline]

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

Equations

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

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

Equations

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

unsafe def Lean.Expr.NumObjs.main (e : Lean.Expr) : Nat

Equations

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

def Lean.Expr.numObjs (e : Lean.Expr) : IO Nat

Returns the number of allocated Expr objects in the given expression 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

• e.numObjs = pure (Lean.Expr.numObjs.unsafe_impl_1 e)