Documentation

Lean.Util.NumObjs

@[reducible, inline]
unsafe abbrev Lean.Expr.NumObjs.M (α : Type) :

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