def Lean.Meta.collectAboveThreshold {α : Type u_1} [BEq α] [Hashable α] (counters : 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 : PHashMap α Nat) : PHashMap α Nat

Equations

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

structure Lean.Meta.DiagSummary : Type

• data : Array MessageData
• max : Nat

Instances For

• Lean.Meta.instInhabitedDiagSummary

instance Lean.Meta.instInhabitedDiagSummary : Inhabited DiagSummary

Equations

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

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

Equations

• s.isEmpty = s.data.isEmpty

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.mkDiagSummaryForUsedInstances : MetaM DiagSummary

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.reportDiag : MetaM Unit

Equations

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