def Lean.Meta.collectAboveThreshold {α : Type u_1} [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α → Bool) (lt : α → α → Bool) : Array (α × Nat)

def Lean.Meta.subCounters {α : Type u_1} [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat

structure Lean.Meta.DiagSummary : Type

• data : Array MessageData
• max : Nat

instance Lean.Meta.instInhabitedDiagSummary : Inhabited DiagSummary

def Lean.Meta.DiagSummary.isEmpty (s : DiagSummary) : Bool

def Lean.Meta.mkDiagSummary (cls : Name) (counters : PHashMap Name Nat) (p : Name → Bool := fun (x : Name) => true) : MetaM DiagSummary

def Lean.Meta.mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances : Bool := false) : MetaM DiagSummary

def Lean.Meta.mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary

def Lean.Meta.mkDiagSummaryForUsedInstances : MetaM DiagSummary

def Lean.Meta.mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM DiagSummary

def Lean.Meta.appendSection (m : Array MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary : Bool := true) : Array MessageData

We use below that this returns m unchanged if s.isEmpty

def Lean.Meta.reportDiag : MetaM Unit