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

Equations

• One or more equations did not get rendered due to their size.

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

structure Lean.Meta.DiagSummary : Type

• data : Array Lean.MessageData
• max : Nat

instance Lean.Meta.instInhabitedDiagSummary : Inhabited Lean.Meta.DiagSummary

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.mkDiagSummaryForUsedInstances : Lean.MetaM Lean.Meta.DiagSummary

Equations

• Lean.Meta.mkDiagSummaryForUsedInstances = do let __do_lift ← get Lean.Meta.mkDiagSummary `type_class __do_lift.diag.instanceCounter

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

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

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

def Lean.Meta.reportDiag : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.