beq

Mathlib.Tactic.Linarith.Parsing

URI: https://scilib.ai/kg/mathlib#Std.TreeMap.beq

Lean4

/-- Returns true if the two maps have the same size and the same keys and values
(with keys compared using the ordering, and values compared using `BEq`). -/
def beq {α β : Type*} [BEq β] {c : α → α → Ordering} (m₁ m₂ : TreeMap α β c) : Bool :=
  m₁.size == m₂.size &&
    Id.run
      (do
        -- This could be made more efficient by simultaneously traversing both maps.

        for (k, v) in m₁ do
          if let some v' := m₂[k]? then
            if v != v' then
              return false
          else
            return false
        return true)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru