source
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.

Instances For

source
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.

Instances For

source
structure Lean.Meta.DiagSummary :
Type

- data : Array MessageData
- max : Nat

Instances For

source
instance Lean.Meta.instInhabitedDiagSummary :
Inhabited DiagSummary
Equations

- Lean.Meta.instInhabitedDiagSummary = { default := Lean.Meta.instInhabitedDiagSummary.default }

source
def Lean.Meta.instInhabitedDiagSummary.default :
DiagSummary
Equations

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

Instances For

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

- s.isEmpty = s.data.isEmpty

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

source
def Lean.Meta.mkDiagSummaryForUsedInstances :
MetaM DiagSummary
Equations

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

Instances For

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

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

Instances For

source
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.

Instances For

source
def Lean.Meta.reportDiag :
MetaM Unit

Logs diagnostics and resets the counters

Equations

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

Instances For