Documentation

Lean.Util.NumObjs

Instances For
    @[reducible, inline]
    unsafe abbrev Lean.Expr.NumObjs.M (α : Type) :
    Equations
      Instances For
        Equations
          Instances For
            unsafe def Lean.Expr.NumObjs.main (e : Expr) :
            Equations
              Instances For

                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
                  Instances For