We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b72f7b9 commit 0e755c7Copy full SHA for 0e755c7
src/Std/Data/DTreeMap/Basic.lean
@@ -1050,6 +1050,7 @@ instance : Inter (DTreeMap α β cmp) := ⟨inter⟩
1050
1051
/--
1052
Compares two tree maps using Boolean equality on keys and values.
1053
+
1054
Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
1055
-/
1056
def beq [LawfulEqCmp cmp] [∀ k, BEq (β k)] (t₁ t₂ : DTreeMap α β cmp) : Bool :=
src/Std/Data/TreeSet/Basic.lean
@@ -505,6 +505,7 @@ instance : Inter (TreeSet α cmp) := ⟨inter⟩
505
506
507
Compares two tree sets using Boolean equality on keys.
508
509
Returns `true` if the sets contain the same keys, `false` otherwise.
510
511
def beq (t₁ t₂ : TreeSet α cmp) : Bool :=
0 commit comments