structure Lean.Expr.NumObjs.State : Type

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

@[reducible, inline]

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

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

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

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)