From 7bd937580494311ecdb9502a7b5ab0ccf473bd44 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 27 Mar 2025 14:52:34 +0100
Subject: [PATCH] chore: write tests for the non-verified tree map functions
 (#7680)

This PR provides tests for those tree map functions that are not
verified yet.

---------

Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
---
 src/Std/Data/DTreeMap/Basic.lean            |   34 +-
 src/Std/Data/DTreeMap/Internal/Queries.lean |   24 +-
 src/Std/Data/DTreeMap/Raw/Basic.lean        |   30 +-
 src/Std/Data/TreeMap/Basic.lean             |   34 +-
 src/Std/Data/TreeMap/Raw/Basic.lean         |   30 +-
 src/Std/Data/TreeSet/Basic.lean             |   10 +-
 src/Std/Data/TreeSet/Raw/Basic.lean         |    8 +-
 tests/lean/run/treemap.lean                 | 1891 +++++++++++++++++++
 8 files changed, 2008 insertions(+), 53 deletions(-)

diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index 6b6a7d88de..24d9a733bf 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -419,37 +419,61 @@ def maxKeyD (t : DTreeMap α β cmp) (fallback : α) : α :=
   letI : Ord α := ⟨cmp⟩; t.inner.maxKeyD fallback
 
 /-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`. -/
+@[inline]
 def entryAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.entryAtIdx? n
 
 /-- Returns the key-value pair with the `n`-th smallest key. -/
+@[inline]
 def entryAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; Impl.entryAtIdx t.inner t.wf.balanced n h
 
 /-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`. -/
+@[inline]
 def entryAtIdx! [Inhabited ((a : α) × β a)] (t : DTreeMap α β cmp) (n : Nat) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.entryAtIdx! n
 
 /-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`. -/
+@[inline]
 def entryAtIdxD (t : DTreeMap α β cmp) (n : Nat)
     (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.entryAtIdxD n fallback
 
 /-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`. -/
+@[inline]
+def keyAtIdx? (t : DTreeMap α β cmp) (n : Nat) : Option α :=
+  letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx? t.inner n
+
+@[inline, inherit_doc keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-25")]
 def keyAtIndex? (t : DTreeMap α β cmp) (n : Nat) : Option α :=
-  letI : Ord α := ⟨cmp⟩; Impl.keyAtIndex? t.inner n
+  keyAtIdx? t n
 
 /-- Returns the `n`-th smallest key. -/
+@[inline]
+def keyAtIdx (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
+  letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx t.inner t.wf.balanced n h
+
+@[inline, inherit_doc keyAtIdx, deprecated keyAtIdx (since := "2025-03-25")]
 def keyAtIndex (t : DTreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
-  letI : Ord α := ⟨cmp⟩; Impl.keyAtIndex t.inner t.wf.balanced n h
+  keyAtIdx t n h
 
 /-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`. -/
+@[inline]
+def keyAtIdx! [Inhabited α] (t : DTreeMap α β cmp) (n : Nat) : α :=
+  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdx! n
+
+@[inline, inherit_doc keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-25")]
 def keyAtIndex! [Inhabited α] (t : DTreeMap α β cmp) (n : Nat) : α :=
-  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIndex! n
+  keyAtIdx! t n
 
 /-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`. -/
+@[inline]
+def keyAtIdxD (t : DTreeMap α β cmp) (n : Nat) (fallback : α) : α :=
+  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdxD n fallback
+
+@[inline, inherit_doc keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-25")]
 def keyAtIndexD (t : DTreeMap α β cmp) (n : Nat) (fallback : α) : α :=
-  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIndexD n fallback
+  keyAtIdxD t n fallback
 
 /--
 Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
@@ -1114,7 +1138,7 @@ def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : DTreeMap α Unit cmp) (l : ρ
 end Const
 
 instance [Repr α] [(a : α) → Repr (β a)] : Repr (DTreeMap α β cmp) where
-  reprPrec m prec := Repr.addAppParen ("DTreeMap.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.DTreeMap.ofList " ++ repr m.toList) prec
 
 end DTreeMap
 
diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean
index e53acedc50..8a9e6ed370 100644
--- a/src/Std/Data/DTreeMap/Internal/Queries.lean
+++ b/src/Std/Data/DTreeMap/Internal/Queries.lean
@@ -406,40 +406,40 @@ def entryAtIdxD : Impl α β → Nat → (a : α) × β a → (a : α) × β a
     | .gt => r.entryAtIdxD (n - l.size - 1) fallback
 
 /-- Implementation detail of the tree map -/
-def keyAtIndex : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α
+def keyAtIdx : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α
   | .inner _ k _ l' r', hl, n, h =>
     match h : compare n l'.size with
-    | .lt => keyAtIndex l' hl.left n (by simpa only [Std.Internal.tree_tac] using h)
+    | .lt => keyAtIdx l' hl.left n (by simpa only [Std.Internal.tree_tac] using h)
     | .eq => k
     | .gt =>
-      keyAtIndex r' hl.right (n - l'.size - 1) (by simp_all only [Std.Internal.tree_tac]; omega)
+      keyAtIdx r' hl.right (n - l'.size - 1) (by simp_all only [Std.Internal.tree_tac]; omega)
 
 /-- Implementation detail of the tree map -/
-def keyAtIndex? : Impl α β → Nat → Option α
+def keyAtIdx? : Impl α β → Nat → Option α
   | .leaf, _ => none
   | .inner _ k _ l r, n =>
     match compare n l.size with
-    | .lt => keyAtIndex? l n
+    | .lt => keyAtIdx? l n
     | .eq => some k
-    | .gt => keyAtIndex? r (n - l.size - 1)
+    | .gt => keyAtIdx? r (n - l.size - 1)
 
 /-- Implementation detail of the tree map -/
-def keyAtIndex! [Inhabited α] : Impl α β → Nat → α
+def keyAtIdx! [Inhabited α] : Impl α β → Nat → α
   | .leaf, _ => panic! "Out-of-bounds access"
   | .inner _ k _ l r, n =>
     match compare n l.size with
-    | .lt => keyAtIndex! l n
+    | .lt => keyAtIdx! l n
     | .eq => k
-    | .gt => keyAtIndex! r (n - l.size - 1)
+    | .gt => keyAtIdx! r (n - l.size - 1)
 
 /-- Implementation detail of the tree map -/
-def keyAtIndexD : Impl α β → Nat → α → α
+def keyAtIdxD : Impl α β → Nat → α → α
   | .leaf, _, fallback => fallback
   | .inner _ k _ l r, n, fallback =>
     match compare n l.size with
-    | .lt => keyAtIndexD l n fallback
+    | .lt => keyAtIdxD l n fallback
     | .eq => k
-    | .gt => keyAtIndexD r (n - l.size - 1) fallback
+    | .gt => keyAtIdxD r (n - l.size - 1) fallback
 
 /-- Implementation detail of the tree map -/
 @[inline]
diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean
index 4c4dd7a048..7626aa37b3 100644
--- a/src/Std/Data/DTreeMap/Raw/Basic.lean
+++ b/src/Std/Data/DTreeMap/Raw/Basic.lean
@@ -303,21 +303,33 @@ def entryAtIdx! [Inhabited ((a : α) × β a)] (t : Raw α β cmp) (n : Nat) : (
 def entryAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : (a : α) × β a) : (a : α) × β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.entryAtIdxD n fallback
 
-@[inline, inherit_doc DTreeMap.keyAtIndex?]
+@[inline, inherit_doc DTreeMap.keyAtIdx?]
+def keyAtIdx? (t : Raw α β cmp) (n : Nat) : Option α :=
+  letI : Ord α := ⟨cmp⟩; Impl.keyAtIdx? t.inner n
+
+@[inline, inherit_doc DTreeMap.keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-25")]
 def keyAtIndex? (t : Raw α β cmp) (n : Nat) : Option α :=
-  letI : Ord α := ⟨cmp⟩; Impl.keyAtIndex? t.inner n
+  keyAtIdx? t n
 
 /-!
-We do not provide `keyAtIndex` for the raw trees.
+We do not provide `keyAtIdx` for the raw trees.
 -/
 
-@[inline, inherit_doc DTreeMap.keyAtIndex!]
-def keyAtIndex! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
-  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIndex! n
+@[inline, inherit_doc DTreeMap.keyAtIdx!]
+def keyAtIdx! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
+  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdx! n
 
-@[inline, inherit_doc DTreeMap.keyAtIndexD]
+@[inline, inherit_doc DTreeMap.keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-25")]
+def keyAtIndex! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
+  keyAtIdx! t n
+
+@[inline, inherit_doc DTreeMap.keyAtIdxD]
+def keyAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
+  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIdxD n fallback
+
+@[inline, inherit_doc DTreeMap.keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-25")]
 def keyAtIndexD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
-  letI : Ord α := ⟨cmp⟩; t.inner.keyAtIndexD n fallback
+  keyAtIdxD t n fallback
 
 @[inline, inherit_doc DTreeMap.getEntryGE?]
 def getEntryGE? (t : Raw α β cmp) (k : α) : Option ((a : α) × β a) :=
@@ -805,7 +817,7 @@ def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : Raw α Unit cmp) (l : ρ) : R
 end Const
 
 instance [Repr α] [(a : α) → Repr (β a)] : Repr (Raw α β cmp) where
-  reprPrec m prec := Repr.addAppParen ("DTreeMap.Raw.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.DTreeMap.Raw.ofList " ++ repr m.toList) prec
 
 end Raw
 
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 020ff2a485..177becd389 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -292,21 +292,37 @@ def entryAtIdx! [Inhabited (α × β)] (t : TreeMap α β cmp) (n : Nat) : α ×
 def entryAtIdxD (t : TreeMap α β cmp) (n : Nat) (fallback : α × β) : α × β :=
   DTreeMap.Const.entryAtIdxD t.inner n fallback
 
-@[inline, inherit_doc DTreeMap.keyAtIndex?]
+@[inline, inherit_doc DTreeMap.keyAtIdx?]
+def keyAtIdx? (t : TreeMap α β cmp) (n : Nat) : Option α :=
+  DTreeMap.keyAtIdx? t.inner n
+
+@[inline, inherit_doc DTreeMap.keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-25")]
 def keyAtIndex? (t : TreeMap α β cmp) (n : Nat) : Option α :=
-  DTreeMap.keyAtIndex? t.inner n
+  keyAtIdx? t n
 
-@[inline, inherit_doc DTreeMap.keyAtIndex]
+@[inline, inherit_doc DTreeMap.keyAtIdx]
+def keyAtIdx (t : TreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
+  DTreeMap.keyAtIdx t.inner n h
+
+@[inline, inherit_doc DTreeMap.keyAtIdx, deprecated keyAtIdx (since := "2025-03-25")]
 def keyAtIndex (t : TreeMap α β cmp) (n : Nat) (h : n < t.size) : α :=
-  DTreeMap.keyAtIndex t.inner n h
+  keyAtIdx t n h
 
-@[inline, inherit_doc DTreeMap.keyAtIndex!]
+@[inline, inherit_doc DTreeMap.keyAtIdx!]
+def keyAtIdx! [Inhabited α] (t : TreeMap α β cmp) (n : Nat) : α :=
+  DTreeMap.keyAtIdx! t.inner n
+
+@[inline, inherit_doc DTreeMap.keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-25")]
 def keyAtIndex! [Inhabited α] (t : TreeMap α β cmp) (n : Nat) : α :=
-  DTreeMap.keyAtIndex! t.inner n
+  keyAtIdx! t n
 
-@[inline, inherit_doc DTreeMap.keyAtIndexD]
+@[inline, inherit_doc DTreeMap.keyAtIdxD]
+def keyAtIdxD (t : TreeMap α β cmp) (n : Nat) (fallback : α) : α :=
+  DTreeMap.keyAtIdxD t.inner n fallback
+
+@[inline, inherit_doc DTreeMap.keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-25")]
 def keyAtIndexD (t : TreeMap α β cmp) (n : Nat) (fallback : α) : α :=
-  DTreeMap.keyAtIndexD t.inner n fallback
+  keyAtIdxD t n fallback
 
 @[inline, inherit_doc DTreeMap.Const.getEntryGE?]
 def getEntryGE? (t : TreeMap α β cmp) (k : α) : Option (α × β) :=
@@ -551,7 +567,7 @@ def eraseMany {ρ} [ForIn Id ρ α] (t : TreeMap α β cmp) (l : ρ) : TreeMap 
   ⟨t.inner.eraseMany l⟩
 
 instance [Repr α] [Repr β] : Repr (TreeMap α β cmp) where
-  reprPrec m prec := Repr.addAppParen ("TreeMap.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.TreeMap.ofList " ++ repr m.toList) prec
 
 end TreeMap
 
diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean
index 2ec148a3d1..4b309b3109 100644
--- a/src/Std/Data/TreeMap/Raw/Basic.lean
+++ b/src/Std/Data/TreeMap/Raw/Basic.lean
@@ -300,21 +300,33 @@ def entryAtIdx! [Inhabited (α × β)] (t : Raw α β cmp) (n : Nat) : α × β
 def entryAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : α × β) : α × β :=
   DTreeMap.Raw.Const.entryAtIdxD t.inner n fallback
 
-@[inline, inherit_doc DTreeMap.Raw.keyAtIndex?]
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdx?]
+def keyAtIdx? (t : Raw α β cmp) (n : Nat) : Option α :=
+  DTreeMap.Raw.keyAtIdx? t.inner n
+
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdx?, deprecated keyAtIdx? (since := "2025-03-26")]
 def keyAtIndex? (t : Raw α β cmp) (n : Nat) : Option α :=
-  DTreeMap.Raw.keyAtIndex? t.inner n
+  keyAtIdx? t n
 
 /-!
-We do not provide `keyAtIndex` for the raw trees.
+We do not provide `keyAtIdx` for the raw trees.
 -/
 
-@[inline, inherit_doc DTreeMap.Raw.keyAtIndex!]
-def keyAtIndex! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
-  DTreeMap.Raw.keyAtIndex! t.inner n
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdx!]
+def keyAtIdx! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
+  DTreeMap.Raw.keyAtIdx! t.inner n
 
-@[inline, inherit_doc DTreeMap.Raw.keyAtIndexD]
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdx!, deprecated keyAtIdx! (since := "2025-03-26")]
+def keyAtIndex! [Inhabited α] (t : Raw α β cmp) (n : Nat) : α :=
+  keyAtIdx! t n
+
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdxD]
+def keyAtIdxD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
+  DTreeMap.Raw.keyAtIdxD t.inner n fallback
+
+@[inline, inherit_doc DTreeMap.Raw.keyAtIdxD, deprecated keyAtIdxD (since := "2025-03-26")]
 def keyAtIndexD (t : Raw α β cmp) (n : Nat) (fallback : α) : α :=
-  DTreeMap.Raw.keyAtIndexD t.inner n fallback
+  keyAtIdxD t n fallback
 
 @[inline, inherit_doc DTreeMap.Raw.Const.getEntryGE?]
 def getEntryGE? (t : Raw α β cmp) (k : α) : Option (α × β) :=
@@ -549,7 +561,7 @@ def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α β cmp) (l : ρ) : Raw α β cmp
   ⟨t.inner.eraseMany l⟩
 
 instance [Repr α] [Repr β] : Repr (Raw α β cmp) where
-  reprPrec m prec := Repr.addAppParen ("TreeMap.Raw.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.TreeMap.Raw.ofList " ++ repr m.toList) prec
 
 end Raw
 
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index 65bc5fda0c..a44c620904 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -238,22 +238,22 @@ def maxD (t : TreeSet α cmp) (fallback : α) : α :=
 /-- Returns the `n`-th smallest element, or `none` if `n` is at least `t.size`. -/
 @[inline]
 def atIdx? (t : TreeSet α cmp) (n : Nat) : Option α :=
-  TreeMap.keyAtIndex? t.inner n
+  TreeMap.keyAtIdx? t.inner n
 
 /-- Returns the `n`-th smallest element. -/
 @[inline]
 def atIdx (t : TreeSet α cmp) (n : Nat) (h : n < t.size) : α :=
-  TreeMap.keyAtIndex t.inner n h
+  TreeMap.keyAtIdx t.inner n h
 
 /-- Returns the `n`-th smallest element, or panics if `n` is at least `t.size`. -/
 @[inline]
 def atIdx! [Inhabited α] (t : TreeSet α cmp) (n : Nat) : α :=
-  TreeMap.keyAtIndex! t.inner n
+  TreeMap.keyAtIdx! t.inner n
 
 /-- Returns the `n`-th smallest element, or `fallback` if `n` is at least `t.size`. -/
 @[inline]
 def atIdxD (t : TreeSet α cmp) (n : Nat) (fallback : α) : α :=
-  TreeMap.keyAtIndexD t.inner n fallback
+  TreeMap.keyAtIdxD t.inner n fallback
 
 /--
 Tries to retrieve the smallest element that is greater than or equal to the
@@ -495,7 +495,7 @@ def eraseMany {ρ} [ForIn Id ρ α] (t : TreeSet α cmp) (l : ρ) : TreeSet α c
   ⟨t.inner.eraseMany l⟩
 
 instance [Repr α] : Repr (TreeSet α cmp) where
-  reprPrec m prec := Repr.addAppParen ("TreeSet.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.TreeSet.ofList " ++ repr m.toList) prec
 
 end TreeSet
 
diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean
index a1418d233a..1123186669 100644
--- a/src/Std/Data/TreeSet/Raw/Basic.lean
+++ b/src/Std/Data/TreeSet/Raw/Basic.lean
@@ -183,7 +183,7 @@ def maxD (t : Raw α cmp) (fallback : α) : α :=
 
 @[inline, inherit_doc TreeSet.atIdx?]
 def atIdx? (t : Raw α cmp) (n : Nat) : Option α :=
-  TreeMap.Raw.keyAtIndex? t.inner n
+  TreeMap.Raw.keyAtIdx? t.inner n
 
 /-!
 We do not provide `entryAtIdx` for the raw trees.
@@ -191,11 +191,11 @@ We do not provide `entryAtIdx` for the raw trees.
 
 @[inline, inherit_doc TreeSet.atIdx!]
 def atIdx! [Inhabited α] (t : Raw α cmp) (n : Nat) : α :=
-  TreeMap.Raw.keyAtIndex! t.inner n
+  TreeMap.Raw.keyAtIdx! t.inner n
 
 @[inline, inherit_doc TreeSet.atIdxD]
 def atIdxD (t : Raw α cmp) (n : Nat) (fallback : α) : α :=
-  TreeMap.Raw.keyAtIndexD t.inner n fallback
+  TreeMap.Raw.keyAtIdxD t.inner n fallback
 
 @[inline, inherit_doc TreeSet.getGE?]
 def getGE? (t : Raw α cmp) (k : α) : Option α :=
@@ -346,7 +346,7 @@ def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α cmp) (l : ρ) : Raw α cmp :=
   ⟨t.inner.eraseMany l⟩
 
 instance [Repr α] : Repr (Raw α cmp) where
-  reprPrec m prec := Repr.addAppParen ("TreeSet.Raw.ofList " ++ repr m.toList) prec
+  reprPrec m prec := Repr.addAppParen ("Std.TreeSet.Raw.ofList " ++ repr m.toList) prec
 
 end Raw
 
diff --git a/tests/lean/run/treemap.lean b/tests/lean/run/treemap.lean
index f91b717c29..5b54373db0 100644
--- a/tests/lean/run/treemap.lean
+++ b/tests/lean/run/treemap.lean
@@ -5,6 +5,10 @@ Authors: Paul Reichert
 -/
 import Std.Data.TreeSet.Basic
 import Std.Data.TreeSet.Lemmas
+import Std.Data.TreeSet.Raw.Basic
+import Std.Data.DTreeMap.Raw.AdditionalOperations
+import Std.Data.TreeMap.Raw.AdditionalOperations
+import Std.Data.TreeMap.AdditionalOperations
 
 open Std
 
@@ -39,3 +43,1890 @@ example [TransOrd α] (a : α) (b : β) : (mkDTreeMapSingleton a b).contains a :
 
 example [TransOrd α] (a : α) : (mkTreeSetSingleton a).contains a := by
   simp [mkTreeSetSingleton, Id.run]
+
+namespace DTreeMap.Raw
+
+def t : DTreeMap.Raw Nat (fun _ => Nat) :=
+  .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]
+
+/-- info: [⟨2, 8⟩] -/
+#guard_msgs in
+#eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/
+#guard_msgs in
+#eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [⟨3, 6⟩] -/
+#guard_msgs in
+#eval (t.filter fun _ v => v > 4).toList
+
+/-- info: [(3, 6), (2, 4), (1, 2)] -/
+#guard_msgs in
+#eval Id.run do
+  let mut ans : List (Nat × Nat) := []
+  for ⟨k, v⟩ in t do
+    ans := (k, v) :: ans
+  return ans
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.toList t
+
+/-- info: #[(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.toArray t
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keys
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.keysArray
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.values
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval (DTreeMap.Raw.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList
+
+/-- info: Std.DTreeMap.Raw.ofList [⟨1, 4⟩] -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.ofList [(1, 2), (1, 4)]
+
+local instance : Inhabited ((_ : Nat) × Nat) where
+  default := ⟨0, 0⟩
+
+/-- info: some ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdx? 1
+
+/-- info: some (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.entryAtIdx? t 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.entryAtIdx? 3
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.entryAtIdx? t 3
+
+/-- info: ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdx! 1
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.entryAtIdx! t 1
+
+/-- info: ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdxD 1 ⟨42, 3⟩
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.entryAtIdxD t 1 ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval t.entryAtIdxD 3 ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.entryAtIdxD t 3 ⟨42, 3⟩
+
+-- TODO: keyAtIdx
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.keyAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.keyAtIdx? 3
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.keyAtIdxD 3 42
+
+/-- info: [none, none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x
+
+/-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLT? t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getEntryLT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLT! t x
+
+/-- info: [⟨42, 3⟩, ⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩
+
+/-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLTD t x (42, 3)
+
+/-- info: [none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, some ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x
+
+/-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLE? t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getEntryLE! x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLE! t x
+
+/-- info: [⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩
+
+/-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLED t x ⟨42, 3⟩
+
+/-- info: [some ⟨1, 2⟩, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x
+
+/-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGE? t x
+
+/-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getEntryGE! x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => DTreeMap.Raw.Const.getEntryGE! t x
+
+/-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGED t x ⟨42, 3⟩
+
+/-- info: [some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x
+
+/-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGT? t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getEntryGT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => DTreeMap.Raw.Const.getEntryGT! t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩, ⟨42, 3⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩
+
+/-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGTD t x ⟨42, 3⟩
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getKeyLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getKeyLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getKeyGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getKeyGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42
+
+/-- info: some ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntry?
+
+/-- info: some (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.minEntry? t
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.minEntry? (∅ : DTreeMap.Raw Nat fun _ => Nat)
+
+/-- info: ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntry!
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.minEntry! t
+
+/-- info: ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntryD ⟨42, 3⟩
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.minEntryD t ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.minEntryD (∅ : DTreeMap.Raw Nat fun _ => Nat) ⟨42, 3⟩
+
+/-- info: some ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntry?
+
+/-- info: some (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.maxEntry? t
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.maxEntry? (∅ : DTreeMap.Raw Nat fun _ => Nat)
+
+/-- info: ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntry!
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.maxEntry! t
+
+/-- info: ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntryD ⟨42, 3⟩
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.maxEntryD t ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntryD ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval DTreeMap.Raw.maxEntryD (∅ : DTreeMap.Raw Nat fun _ => Nat) ⟨42, 3⟩
+
+/-- info: (Std.DTreeMap.Raw.ofList [⟨3, 6⟩], Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩]) -/
+#guard_msgs in
+#eval t.partition fun k v => k + 3 == v
+
+/-- info: (Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩], Std.DTreeMap.Raw.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ _ => true
+
+/-- info: (Std.DTreeMap.Raw.ofList [], Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]) -/
+#guard_msgs in
+#eval t.partition fun _ _ => false
+
+/-- info: (Std.DTreeMap.Raw.ofList [], Std.DTreeMap.Raw.ofList []) -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).partition fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k v => k + 5 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k v => k + k == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k v => k + 3 == v
+
+/-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.DTreeMap.Raw.ofList [⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.DTreeMap.Raw.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+-- We can't prove the non-Const variant yet because Nat doesn't have a LawfulEqOrd instance
+/-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.mergeWith (fun _ v _ => v) t ∅
+
+/-- info: Std.DTreeMap.Raw.ofList [⟨0, 0⟩, ⟨1, 0⟩, ⟨2, 0⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval DTreeMap.Raw.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
+
+end DTreeMap.Raw
+
+namespace DTreeMap
+
+def t : DTreeMap Nat (fun _ => Nat) :=
+  .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]
+
+/-- info: [⟨2, 8⟩] -/
+#guard_msgs in
+#eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/
+#guard_msgs in
+#eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [⟨3, 6⟩] -/
+#guard_msgs in
+#eval (t.filter fun _ v => v > 4).toList
+
+/-- info: [(3, 6), (2, 4), (1, 2)] -/
+#guard_msgs in
+#eval Id.run do
+  let mut ans : List (Nat × Nat) := []
+  for ⟨k, v⟩ in t do
+    ans := (k, v) :: ans
+  return ans
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval DTreeMap.Const.toList t
+
+/-- info: #[(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval DTreeMap.Const.toArray t
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keys
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.keysArray
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.values
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval (DTreeMap.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList
+
+/-- info: Std.DTreeMap.ofList [⟨1, 4⟩] -/
+#guard_msgs in
+#eval DTreeMap.Const.ofList [(1, 2), (1, 4)]
+
+local instance : Inhabited ((_ : Nat) × Nat) where
+  default := ⟨0, 0⟩
+
+/-- info: some ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdx? 1
+
+/-- info: some (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Const.entryAtIdx? t 1
+
+/--
+info: ⟨2, 4⟩
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.entryAtIdx 1 sorry
+
+/--
+info: (2, 4)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! DTreeMap.Const.entryAtIdx t 1 sorry
+
+/-- info: none -/
+#guard_msgs in
+#eval t.entryAtIdx? 3
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Const.entryAtIdx? t 3
+
+/-- info: ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdx! 1
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Const.entryAtIdx! t 1
+
+/-- info: ⟨2, 4⟩ -/
+#guard_msgs in
+#eval t.entryAtIdxD 1 ⟨42, 3⟩
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval DTreeMap.Const.entryAtIdxD t 1 ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval t.entryAtIdxD 3 ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval DTreeMap.Const.entryAtIdxD t 3 ⟨42, 3⟩
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.keyAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.keyAtIdx? 3
+
+/--
+info: 2
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.keyAtIdx 1 sorry
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.keyAtIdxD 3 42
+
+/-- info: [none, none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x
+
+/-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLT? t x
+
+/-
+Cannot test `getEntryLT` etc. as of writing (2025-03-25) because
+`TransOrd Nat` is not implemented yet.
+-/
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getEntryLT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => DTreeMap.Const.getEntryLT! t x
+
+/-- info: [⟨42, 3⟩, ⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩
+
+/-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLTD t x (42, 3)
+
+/-- info: [none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, some ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x
+
+/-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLE? t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getEntryLE! x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLE! t x
+
+/-- info: [⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩
+
+/-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLED t x ⟨42, 3⟩
+
+/-- info: [some ⟨1, 2⟩, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x
+
+/-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGE? t x
+
+/-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getEntryGE! x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => DTreeMap.Const.getEntryGE! t x
+
+/-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGED t x ⟨42, 3⟩
+
+/-- info: [some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x
+
+/-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGT? t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getEntryGT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => DTreeMap.Const.getEntryGT! t x
+
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩, ⟨42, 3⟩] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩
+
+/-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGTD t x ⟨42, 3⟩
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getKeyLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getKeyLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getKeyGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getKeyGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42
+
+/-- info: some ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntry?
+
+/-- info: some (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Const.minEntry? t
+
+/--
+info: ⟨1, 2⟩
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.minEntry sorry
+
+/--
+info: (1, 2)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! DTreeMap.Const.minEntry t sorry
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Const.minEntry? (∅ : DTreeMap Nat fun _ => Nat)
+
+/-- info: ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntry!
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Const.minEntry! t
+
+/-- info: ⟨1, 2⟩ -/
+#guard_msgs in
+#eval t.minEntryD ⟨42, 3⟩
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval DTreeMap.Const.minEntryD t ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval DTreeMap.Const.minEntryD (∅ : DTreeMap Nat fun _ => Nat) ⟨42, 3⟩
+
+/-- info: some ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntry?
+
+/-- info: some (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Const.maxEntry? t
+
+/--
+info: ⟨3, 6⟩
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.maxEntry sorry
+
+/--
+info: (3, 6)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! DTreeMap.Const.maxEntry t sorry
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : DTreeMap Nat fun _ => Nat).maxEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval DTreeMap.Const.maxEntry? (∅ : DTreeMap Nat fun _ => Nat)
+
+/-- info: ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntry!
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Const.maxEntry! t
+
+/-- info: ⟨3, 6⟩ -/
+#guard_msgs in
+#eval t.maxEntryD ⟨42, 3⟩
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval DTreeMap.Const.maxEntryD t ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntryD ⟨42, 3⟩
+
+/-- info: ⟨42, 3⟩ -/
+#guard_msgs in
+#eval DTreeMap.maxEntryD (∅ : DTreeMap Nat fun _ => Nat) ⟨42, 3⟩
+
+/-- info: (Std.DTreeMap.ofList [⟨3, 6⟩], Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩]) -/
+#guard_msgs in
+#eval t.partition fun k v => k + 3 == v
+
+/-- info: (Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩], Std.DTreeMap.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ _ => true
+
+/-- info: (Std.DTreeMap.ofList [], Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]) -/
+#guard_msgs in
+#eval t.partition fun _ _ => false
+
+/-- info: (Std.DTreeMap.ofList [], Std.DTreeMap.ofList []) -/
+#guard_msgs in
+#eval (∅ : DTreeMap Nat fun _ => Nat).partition fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k v => k + 5 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k v => k + k == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k v => k + 3 == v
+
+/-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.DTreeMap.ofList [⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.DTreeMap.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+-- We can't prove the non-Const variant yet because Nat doesn't have a LawfulEqOrd instance
+/-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval DTreeMap.Const.mergeWith (fun _ v _ => v) t ∅
+
+/-- info: Std.DTreeMap.ofList [⟨0, 0⟩, ⟨1, 0⟩, ⟨2, 0⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval DTreeMap.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
+
+end DTreeMap
+
+namespace TreeMap.Raw
+
+def t : TreeMap.Raw Nat Nat :=
+  .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]
+
+/-- info: [(2, 8)] -/
+#guard_msgs in
+#eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [(1, none), (2, some 8), (3, none)] -/
+#guard_msgs in
+#eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [(3, 6)] -/
+#guard_msgs in
+#eval (t.filter fun _ v => v > 4).toList
+
+/-- info: [(3, 6), (2, 4), (1, 2)] -/
+#guard_msgs in
+#eval Id.run do
+  let mut ans : List (Nat × Nat) := []
+  for ⟨k, v⟩ in t do
+    ans := (k, v) :: ans
+  return ans
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keys
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.keysArray
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.values
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval (TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)]).toList
+
+/-- info: Std.TreeMap.Raw.ofList [(1, 4)] -/
+#guard_msgs in
+#eval TreeMap.Raw.ofList [(1, 2), (1, 4)]
+
+local instance : Inhabited ((_ : Nat) × Nat) where
+  default := ⟨0, 0⟩
+
+/-- info: some (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.entryAtIdx? 3
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdx! 1
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdxD 1 ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval t.entryAtIdxD 3 ⟨42, 3⟩
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.keyAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.keyAtIdx? 3
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.keyAtIdxD 3 42
+
+/-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getEntryLT! x
+
+/-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩
+
+/-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getEntryLE! x
+
+/-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩
+
+/-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getEntryGE! x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩
+
+/-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getEntryGT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getKeyLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getKeyLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getKeyGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getKeyGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42
+
+/-- info: some (1, 2) -/
+#guard_msgs in
+#eval t.minEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : TreeMap.Raw Nat Nat).minEntry?
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval t.minEntry!
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval t.minEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval (∅ : TreeMap.Raw Nat Nat).minEntryD ⟨42, 3⟩
+
+/-- info: some (3, 6) -/
+#guard_msgs in
+#eval t.maxEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : TreeMap.Raw Nat Nat).maxEntry?
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval t.maxEntry!
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval t.maxEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval (∅ : TreeMap.Raw Nat Nat).maxEntryD ⟨42, 3⟩
+
+/-- info: (Std.TreeMap.Raw.ofList [(3, 6)], Std.TreeMap.Raw.ofList [(1, 2), (2, 4)]) -/
+#guard_msgs in
+#eval t.partition fun k v => k + 3 == v
+
+/-- info: (Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)], Std.TreeMap.Raw.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ _ => true
+
+/-- info: (Std.TreeMap.Raw.ofList [], Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)]) -/
+#guard_msgs in
+#eval t.partition fun _ _ => false
+
+/-- info: (Std.TreeMap.Raw.ofList [], Std.TreeMap.Raw.ofList []) -/
+#guard_msgs in
+#eval (∅ : TreeMap.Raw Nat Nat).partition fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k v => k + 5 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k v => k + k == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k v => k + 3 == v
+
+/-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.TreeMap.Raw.ofList [(2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.TreeMap.Raw.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+/-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval TreeMap.Raw.mergeWith (fun _ v _ => v) t ∅
+
+/-- info: Std.TreeMap.Raw.ofList [(0, 0), (1, 0), (2, 0), (3, 6)] -/
+#guard_msgs in
+#eval TreeMap.Raw.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
+
+end TreeMap.Raw
+
+namespace TreeMap
+
+def t : TreeMap Nat Nat :=
+  .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]
+
+/-- info: [(2, 8)] -/
+#guard_msgs in
+#eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [(1, none), (2, some 8), (3, none)] -/
+#guard_msgs in
+#eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
+
+/-- info: [(3, 6)] -/
+#guard_msgs in
+#eval (t.filter fun _ v => v > 4).toList
+
+/-- info: [(3, 6), (2, 4), (1, 2)] -/
+#guard_msgs in
+#eval Id.run do
+  let mut ans : List (Nat × Nat) := []
+  for ⟨k, v⟩ in t do
+    ans := (k, v) :: ans
+  return ans
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keys
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.keysArray
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.values
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval (TreeMap.ofList [(1, 2), (2, 4), (3, 6)]).toList
+
+/-- info: Std.TreeMap.ofList [(1, 4)] -/
+#guard_msgs in
+#eval TreeMap.ofList [(1, 2), (1, 4)]
+
+local instance : Inhabited ((_ : Nat) × Nat) where
+  default := ⟨0, 0⟩
+
+/-- info: some (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.entryAtIdx? 3
+
+/--
+info: (2, 4)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.entryAtIdx 1 sorry
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdx! 1
+
+/-- info: (2, 4) -/
+#guard_msgs in
+#eval t.entryAtIdxD 1 ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval t.entryAtIdxD 3 ⟨42, 3⟩
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.keyAtIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.keyAtIdx? 3
+
+/--
+info: 2
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.keyAtIdx 1 sorry
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.keyAtIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.keyAtIdxD 3 42
+
+/-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getEntryLT! x
+
+/-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩
+
+/-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getEntryLE! x
+
+/-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩
+
+/-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getEntryGE! x
+
+/-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩
+
+/-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x
+
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getEntryGT! x
+
+/-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getKeyLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getKeyLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getKeyGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getKeyGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42
+
+/-- info: some (1, 2) -/
+#guard_msgs in
+#eval t.minEntry?
+
+/--
+info: (1, 2)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.minEntry sorry
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : TreeMap Nat Nat).minEntry?
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval t.minEntry!
+
+/-- info: (1, 2) -/
+#guard_msgs in
+#eval t.minEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval (∅ : TreeMap Nat Nat).minEntryD ⟨42, 3⟩
+
+/-- info: some (3, 6) -/
+#guard_msgs in
+#eval t.maxEntry?
+
+/-- info: none -/
+#guard_msgs in
+#eval (∅ : TreeMap Nat Nat).maxEntry?
+
+/--
+info: (3, 6)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.maxEntry sorry
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval t.maxEntry!
+
+/-- info: (3, 6) -/
+#guard_msgs in
+#eval t.maxEntryD ⟨42, 3⟩
+
+/-- info: (42, 3) -/
+#guard_msgs in
+#eval (∅ : TreeMap Nat Nat).maxEntryD ⟨42, 3⟩
+
+/-- info: (Std.TreeMap.ofList [(3, 6)], Std.TreeMap.ofList [(1, 2), (2, 4)]) -/
+#guard_msgs in
+#eval t.partition fun k v => k + 3 == v
+
+/-- info: (Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)], Std.TreeMap.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ _ => true
+
+/-- info: (Std.TreeMap.ofList [], Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)]) -/
+#guard_msgs in
+#eval t.partition fun _ _ => false
+
+/-- info: (Std.TreeMap.ofList [], Std.TreeMap.ofList []) -/
+#guard_msgs in
+#eval (∅ : TreeMap Nat Nat).partition fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k v => k + 3 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k v => k + 5 == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k v => k + k == v
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k v => k + 3 == v
+
+/-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.TreeMap.ofList [(2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.TreeMap.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+/-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval TreeMap.mergeWith (fun _ v _ => v) t ∅
+
+/-- info: Std.TreeMap.ofList [(0, 0), (1, 0), (2, 0), (3, 6)] -/
+#guard_msgs in
+#eval TreeMap.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
+
+end TreeMap
+
+namespace TreeSet.Raw
+
+def t : TreeSet.Raw Nat :=
+  .ofList [1, 2, 3]
+
+/-- info: [3] -/
+#guard_msgs in
+#eval (t.filter fun k => k > 2).toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval (TreeSet.Raw.ofList [1, 2, 3]).toList
+
+/-- info: Std.TreeSet.Raw.ofList [1] -/
+#guard_msgs in
+#eval TreeSet.Raw.ofList [1, 1]
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.atIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.atIdx? 3
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.atIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.atIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.atIdxD 3 42
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGTD x 42
+
+/-- info: (Std.TreeSet.Raw.ofList [3], Std.TreeSet.Raw.ofList [1, 2]) -/
+#guard_msgs in
+#eval t.partition fun k => k == 3
+
+/-- info: (Std.TreeSet.Raw.ofList [1, 2, 3], Std.TreeSet.Raw.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ => true
+
+/-- info: (Std.TreeSet.Raw.ofList [], Std.TreeSet.Raw.ofList [1, 2, 3]) -/
+#guard_msgs in
+#eval t.partition fun _ => false
+
+/-- info: (Std.TreeSet.Raw.ofList [], Std.TreeSet.Raw.ofList []) -/
+#guard_msgs in
+#eval (∅ : TreeSet.Raw Nat).partition fun k => k == 3
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k => k == 3
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k => k == 5
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k => k < 6
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k => k == 3
+
+/-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.TreeSet.Raw.ofList [2, 3] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.TreeSet.Raw.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+/-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval TreeSet.Raw.merge t ∅
+
+/-- info: Std.TreeSet.Raw.ofList [0, 1, 2, 3] -/
+#guard_msgs in
+#eval TreeSet.Raw.merge t (.ofList [0, 1, 2])
+
+end TreeSet.Raw
+
+namespace TreeSet
+
+def t : TreeSet Nat :=
+  .ofList [1, 2, 3]
+
+/-- info: [3] -/
+#guard_msgs in
+#eval (t.filter fun k => k > 2).toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.toList
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval t.toArray
+
+/-- info: some 2 -/
+#guard_msgs in
+#eval t.atIdx? 1
+
+/-- info: none -/
+#guard_msgs in
+#eval t.atIdx? 3
+
+/--
+info: 2
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+#eval! t.atIdx 1 sorry
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.atIdx! 1
+
+/-- info: 2 -/
+#guard_msgs in
+#eval t.atIdxD 1 42
+
+/-- info: 42 -/
+#guard_msgs in
+#eval t.atIdxD 3 42
+
+/-- info: [none, none, some 1, some 2, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [2, 3, 4].map fun x => t.getLT! x
+
+/-- info: [42, 42, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLTD x 42
+
+/-- info: [none, some 1, some 2, some 3, some 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLE? x
+
+/-- info: [1, 2, 3, 3] -/
+#guard_msgs in
+#eval [1, 2, 3, 4].map fun x => t.getLE! x
+
+/-- info: [42, 1, 2, 3, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getLED x 42
+
+/-- info: [some 1, some 1, some 2, some 3, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGE? x
+
+/-- info: [1, 1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2, 3].map fun x => t.getGE! x
+
+/-- info: [1, 1, 2, 3, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGED x 42
+
+/-- info: [some 1, some 2, some 3, none, none] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGT? x
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [0, 1, 2].map fun x => t.getGT! x
+
+/-- info: [1, 2, 3, 42, 42] -/
+#guard_msgs in
+#eval [0, 1, 2, 3, 4].map fun x => t.getGTD x 42
+
+/-- info: (Std.TreeSet.ofList [3], Std.TreeSet.ofList [1, 2]) -/
+#guard_msgs in
+#eval t.partition fun k => k == 3
+
+/-- info: (Std.TreeSet.ofList [1, 2, 3], Std.TreeSet.ofList []) -/
+#guard_msgs in
+#eval t.partition fun _ => true
+
+/-- info: (Std.TreeSet.ofList [], Std.TreeSet.ofList [1, 2, 3]) -/
+#guard_msgs in
+#eval t.partition fun _ => false
+
+/-- info: (Std.TreeSet.ofList [], Std.TreeSet.ofList []) -/
+#guard_msgs in
+#eval (∅ : TreeSet Nat).partition fun k => k == 3
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.any fun k => k == 3
+
+/-- info: false -/
+#guard_msgs in
+#eval t.any fun k => k == 5
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun _ => false
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun _ => true
+
+/-- info: true -/
+#guard_msgs in
+#eval t.all fun k => k < 6
+
+/-- info: false -/
+#guard_msgs in
+#eval t.all fun k => k == 3
+
+/-- info: Std.TreeSet.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval t.eraseMany []
+
+/-- info: Std.TreeSet.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval t.eraseMany [0]
+
+/-- info: Std.TreeSet.ofList [2, 3] -/
+#guard_msgs in
+#eval t.eraseMany [1]
+
+/-- info: Std.TreeSet.ofList [] -/
+#guard_msgs in
+#eval t.eraseMany [1, 2, 3]
+
+/-- info: Std.TreeSet.ofList [1, 2, 3] -/
+#guard_msgs in
+#eval TreeSet.merge t ∅
+
+/-- info: Std.TreeSet.ofList [0, 1, 2, 3] -/
+#guard_msgs in
+#eval TreeSet.merge t (.ofList [0, 1, 2])
+
+end TreeSet