Documentation

Lean.Meta.Diagnostics

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.
Instances For
    def Lean.Meta.subCounters {α : Type u_1} [BEq α] [Hashable α] (newCounters : Lean.PHashMap α Nat) (oldCounters : Lean.PHashMap α Nat) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Instances For
        Equations
        Equations
        • s.isEmpty = s.data.isEmpty
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For