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 : Lean.PHashMap α Nat) (oldCounters : Lean.PHashMap α Nat) : Lean.PHashMap α Nat

Equations

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

structure Lean.Meta.DiagSummary : Type

• data : Array Lean.MessageData
• max : Nat

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

Equations

• Lean.Meta.instInhabitedDiagSummary = { default := { data := default, max := default } }

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

Equations

• s.isEmpty = s.data.isEmpty

def Lean.Meta.mkDiagSummary (cls : Lake.Name) (counters : Lean.PHashMap Lake.Name Nat) (p : optParam (Lake.Name → Bool) fun (x : Lake.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 Lake.Name Nat) (instances : optParam Bool false) : Lean.MetaM Lean.Meta.DiagSummary

Equations

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

def Lean.Meta.mkDiagSummaryForUnfoldedReducible (counters : Lean.PHashMap Lake.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

Equations

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

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

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

Equations

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

def Lean.Meta.reportDiag : Lean.MetaM Unit

Equations

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