Documentation

Lean.Util.NumApps

Instances For
    @[reducible, inline]
    unsafe abbrev Lean.Expr.NumApps.M (α : Type) :
    Instances For
      def Lean.Expr.numApps (e : Lean.Expr) (threshold : Nat := 0) :

      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.

      Instances For