chore: add iterator tests

Author: wkrozowski

src/Std/Data/DTreeMap/Iterator.lean

@@ -26,8 +26,8 @@ The iterator yields the elements of the map in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u} {β : α → Type v}
-    (cmp : α → α → Ordering := by exact compare) (m : DTreeMap α β cmp) :=
-  Raw.iter cmp ⟨m.inner⟩
+    {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :=
+  @Raw.iter _ _ cmp ⟨m.inner⟩
 
 /--
 Returns a finite iterator over the keys of a dependent tree map.
@@ -41,9 +41,8 @@ The key and value types must live in the same universe.
 * `Productive` instance: always
 -/
 @[inline]
-public def keysIter {α : Type u} {β : α → Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : DTreeMap α β cmp) :=
-  Raw.keysIter cmp ⟨m.inner⟩
+public def keysIter {α : Type u} {β : α → Type u} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :=
+  @Raw.keysIter _ _ cmp ⟨m.inner⟩
 
 /--
 Returns a finite iterator over the values of a tree map.
@@ -57,20 +56,20 @@ The key and value types must live in the same universe.
 * `Productive` instance: always
 -/
 @[inline]
-public def valuesIter {α : Type u} {β : Type u} (cmp : α → α → Ordering := by exact compare)
+public def valuesIter {α : Type u} {β : Type u} {cmp : α → α → Ordering}
     (m : DTreeMap α (fun _ => β) cmp) :=
-  Raw.valuesIter cmp ⟨m.inner⟩
+  @Raw.valuesIter _ _ cmp  ⟨m.inner⟩
 
 @[simp]
 public theorem iter_toList {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :
-    (m.iter cmp).toList = m.toList := Raw.iter_toList ⟨m.inner⟩
+    m.iter.toList = m.toList := Raw.iter_toList ⟨m.inner⟩
 
 @[simp]
-public theorem keysIter_toList {α β} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :
-    (m.keysIter cmp).toList = m.keys := Raw.keysIter_toList ⟨m.inner⟩
+public theorem keysIter_toList {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :
+    m.keysIter.toList = m.keys := Raw.keysIter_toList ⟨m.inner⟩
 
 @[simp]
-public theorem valuesIter_toList {α β} {cmp : α → α → Ordering} (m : DTreeMap α (fun _ => β) cmp) :
-    (m.valuesIter cmp).toList = m.values := Raw.valuesIter_toList ⟨m.inner⟩
+public theorem valuesIter_toList {cmp : α → α → Ordering} (m : DTreeMap α (fun _ => β) cmp) :
+    m.valuesIter.toList = m.values := Raw.valuesIter_toList ⟨m.inner⟩
 
 end Std.DTreeMap

src/Std/Data/DTreeMap/Raw/Iterator.lean

@@ -27,7 +27,7 @@ The iterator yields the elements of the map in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u} {β : α → Type v}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α β cmp) :=
+    {cmp : α → α → Ordering} (m : Raw α β cmp) :=
   (Internal.Zipper.iterOfTree m.inner : Iter ((a : α) × β a))
 
 /--
@@ -43,8 +43,8 @@ The key and value types must live in the same universe.
 -/
 @[inline]
 public def keysIter {α : Type u} {β : α → Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α β cmp) :=
-  ((m.iter cmp).map fun e => e.1 : Iter α)
+    {cmp : α → α → Ordering} (m : Raw α β cmp) :=
+  (m.iter.map fun e => e.1 : Iter α)
 
 /--
 Returns a finite iterator over the values of a tree map.
@@ -59,24 +59,24 @@ The key and value types must live in the same universe.
 -/
 @[inline]
 public def valuesIter {α : Type u} {β : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α (fun _ => β) cmp) :=
-  ((m.iter cmp).map fun e => e.2 : Iter β)
+    {cmp : α → α → Ordering} (m : Raw α (fun _ => β) cmp) :=
+  (m.iter.map fun e => e.2 : Iter β)
 
 @[simp]
 public theorem iter_toList {cmp : α → α → Ordering} (m : Raw α β cmp) :
-    (m.iter cmp).toList = m.toList := by
+    (m.iter).toList = m.toList := by
   rw [iter, toList]
   apply Internal.Zipper.toList.iterOfTree
 
 @[simp]
-public theorem keysIter_toList {α β} {cmp : α → α → Ordering} (m : Raw α β cmp) :
-    (m.keysIter cmp).toList = m.keys := by
+public theorem keysIter_toList {cmp : α → α → Ordering} (m : Raw α β cmp) :
+    (m.keysIter).toList = m.keys := by
   rw [keysIter, keys, iter, ← Internal.Impl.map_fst_toList_eq_keys]
   apply Internal.Zipper.map_iterOfTree_eq_tree_toList_map
 
 @[simp]
-public theorem valuesIter_toList {α β} {cmp : α → α → Ordering} (m : Raw α (fun _ => β) cmp) :
-    (m.valuesIter cmp).toList = m.values := by
+public theorem valuesIter_toList {cmp : α → α → Ordering} (m : Raw α (fun _ => β) cmp) :
+    (m.valuesIter).toList = m.values := by
   rw [valuesIter, values, iter, Internal.Impl.values_eq_map_snd, ← Internal.Impl.toList_eq_toListModel]
   apply Internal.Zipper.map_iterOfTree_eq_tree_toList_map
 

src/Std/Data/TreeMap/Iterator.lean

@@ -27,8 +27,8 @@ The iterator yields the elements of the map in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u} {β : Type v}
-    (cmp : α → α → Ordering := by exact compare) (m : TreeMap α β cmp) :=
-  ((m.inner.iter cmp).map fun e => (e.1, e.2) : Iter (α × β))
+    {cmp : α → α → Ordering} (m : TreeMap α β cmp) :=
+  (m.inner.iter.map fun e => (e.1, e.2) : Iter (α × β))
 
 /--
 Returns a finite iterator over the keys of a tree map.
@@ -43,8 +43,8 @@ The key and value types must live in the same universe.
 -/
 @[inline]
 public def keysIter {α : Type u} {β : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : TreeMap α β cmp) :=
-  m.inner.keysIter cmp
+    {cmp : α → α → Ordering} (m : TreeMap α β cmp) :=
+  m.inner.keysIter
 
 /--
 Returns a finite iterator over the values of a tree map.
@@ -58,26 +58,26 @@ The key and value types must live in the same universe.
 * `Productive` instance: always
 -/
 @[inline]
-public def valuesIter {α : Type u} {β : Type u} (cmp : α → α → Ordering := by exact compare)
+public def valuesIter {α : Type u} {β : Type u} {cmp : α → α → Ordering}
     (m : TreeMap α β cmp) :=
-  m.inner.valuesIter cmp
+  m.inner.valuesIter
 
 @[simp]
 public theorem iter_toList {cmp : α → α → Ordering} (m : TreeMap α β cmp) :
-    (m.iter cmp).toList = m.toList := by
+    m.iter.toList = m.toList := by
   simp only [iter, Iter.toList_map, DTreeMap.iter_toList, DTreeMap.toList,
     DTreeMap.Internal.Impl.toList_eq_toListModel, toList, DTreeMap.Const.toList,
     DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map]
 
 
 @[simp]
 public theorem keysIter_toList {α β} {cmp : α → α → Ordering} (m : TreeMap α β cmp) :
-    (m.keysIter cmp).toList = m.keys :=
+    m.keysIter.toList = m.keys :=
   m.inner.keysIter_toList
 
 @[simp]
 public theorem valuesIter_toList {α β} {cmp : α → α → Ordering} (m : TreeMap α β cmp) :
-    (m.valuesIter cmp).toList = m.values :=
+    m.valuesIter.toList = m.values :=
   m.inner.valuesIter_toList
 
 end Std.TreeMap

src/Std/Data/TreeMap/Raw/Iterator.lean

@@ -27,8 +27,8 @@ The iterator yields the elements of the map in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u} {β : Type v}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α β cmp) :=
-  ((m.inner.iter cmp).map fun e => (e.1, e.2) : Iter (α × β))
+    {cmp : α → α → Ordering} (m : Raw α β cmp) :=
+  (m.inner.iter.map fun e => (e.1, e.2) : Iter (α × β))
 
 /--
 Returns a finite iterator over the keys of a tree map.
@@ -43,8 +43,8 @@ The key and value types must live in the same universe.
 -/
 @[inline]
 public def keysIter {α : Type u} {β : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α β cmp) :=
-  (DTreeMap.Raw.keysIter cmp m.inner : Iter α)
+    {cmp : α → α → Ordering} (m : Raw α β cmp) :=
+  (m.inner.keysIter : Iter α)
 
 /--
 Returns a finite iterator over the values of a tree map.
@@ -59,24 +59,24 @@ The key and value types must live in the same universe.
 -/
 @[inline]
 public def valuesIter {α : Type u} {β : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α β cmp) :=
-  (DTreeMap.Raw.valuesIter cmp m.inner : Iter β)
+    {cmp : α → α → Ordering} (m : Raw α β cmp) :=
+  (m.inner.valuesIter : Iter β)
 
 @[simp]
 public theorem iter_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Raw α β cmp) :
-    ((m.iter cmp).toList) = m.toList := by
+    (m.iter.toList) = m.toList := by
   simp only [iter, Iter.toList_map, DTreeMap.Raw.iter_toList]
   simp only [DTreeMap.Raw.toList, DTreeMap.Internal.Impl.toList_eq_toListModel, toList,
     DTreeMap.Raw.Const.toList, DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map]
 
 @[simp]
 public theorem keysIter_toList {α β} {cmp : α → α → Ordering} (m : Raw α β cmp) :
-    (m.keysIter cmp).toList = m.keys :=
+    m.keysIter.toList = m.keys :=
   DTreeMap.Raw.keysIter_toList m.inner
 
 @[simp]
 public theorem valuesIter_toList {α β} {cmp : α → α → Ordering} (m : Raw α β cmp) :
-    (m.valuesIter cmp).toList = m.values :=
+    m.valuesIter.toList = m.values :=
   DTreeMap.Raw.valuesIter_toList m.inner
 
 end Std.TreeMap.Raw

src/Std/Data/TreeSet/Iterator.lean

@@ -28,12 +28,12 @@ The iterator yields the elements of the set in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : TreeSet α cmp) :=
-  ((m.inner.iter cmp).map fun e => e.1 : Iter α)
+    {cmp : α → α → Ordering} (m : TreeSet α cmp) :=
+  (m.inner.iter.map fun e => e.1 : Iter α)
 
 @[simp]
 public theorem iter_toList {cmp : α → α → Ordering} (m : TreeSet α cmp) :
-    (m.iter cmp).toList = m.toList := by
+    m.iter.toList = m.toList := by
   rw [iter, Iter.toList_map, TreeMap.iter_toList, toList, TreeMap.toList, TreeMap.keys, Std.DTreeMap.Const.map_fst_toList_eq_keys]
 
 end Std.TreeSet

src/Std/Data/TreeSet/Raw/Iterator.lean

@@ -28,12 +28,12 @@ The iterator yields the elements of the set in order and then terminates.
 -/
 @[inline]
 public def iter {α : Type u}
-    (cmp : α → α → Ordering := by exact compare) (m : Raw α cmp) :=
-  ((m.inner.iter cmp).map fun e => e.1 : Iter α)
+    {cmp : α → α → Ordering} (m : Raw α cmp) :=
+  (m.inner.iter.map fun e => e.1 : Iter α)
 
 @[simp]
 public theorem iter_toList {cmp : α → α → Ordering} (m : Raw α cmp) :
-    (m.iter cmp).toList = m.toList := by
+    m.iter.toList = m.toList := by
   rw [iter, Iter.toList_map, TreeMap.Raw.iter_toList, TreeMap.Raw.toList]
   rw [TreeSet.Raw.toList]
   rw [Std.DTreeMap.Internal.Impl.foldr_eq_foldr_toList]

tests/lean/run/treemap.lean

@@ -9,7 +9,12 @@ import Std.Data.TreeSet.Raw.Basic
 import Std.Data.DTreeMap.Raw.AdditionalOperations
 import Std.Data.TreeMap.Raw.AdditionalOperations
 import Std.Data.TreeMap.AdditionalOperations
-
+import Std.Data.DTreeMap.Iterator
+import Std.Data.DTreeMap.Raw.Iterator
+import Std.Data.TreeMap.Iterator
+import Std.Data.TreeMap.Raw.Iterator
+import Std.Data.TreeSet.Iterator
+import Std.Data.TreeSet.Raw.Iterator
 open Std
 
 variable {α : Type u} {β : Type v} [Ord α]
@@ -467,6 +472,18 @@ local instance : Inhabited ((_ : Nat) × Nat) where
 #guard_msgs in
 #eval DTreeMap.Raw.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
 
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.iter.toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keysIter.toList
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.valuesIter.toList
+
 end DTreeMap.Raw
 
 namespace DTreeMap
@@ -951,6 +968,18 @@ warning: declaration uses 'sorry'
 #guard_msgs in
 #eval DTreeMap.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
 
+/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
+#guard_msgs in
+#eval t.iter.toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keysIter.toList
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.valuesIter.toList
+
 end DTreeMap
 
 namespace TreeMap.Raw
@@ -1257,6 +1286,19 @@ local instance : Inhabited ((_ : Nat) × Nat) where
 #guard_msgs in
 #eval TreeMap.Raw.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
 
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.iter.toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keysIter.toList
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.valuesIter.toList
+
+
 end TreeMap.Raw
 
 namespace TreeMap
@@ -1595,6 +1637,18 @@ warning: declaration uses 'sorry'
 #guard_msgs in
 #eval TreeMap.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩])
 
+/-- info: [(1, 2), (2, 4), (3, 6)] -/
+#guard_msgs in
+#eval t.iter.toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.keysIter.toList
+
+/-- info: [2, 4, 6] -/
+#guard_msgs in
+#eval t.valuesIter.toList
+
 end TreeMap
 
 namespace TreeSet.Raw
@@ -1762,6 +1816,10 @@ def t : TreeSet.Raw Nat :=
 #guard_msgs in
 #eval TreeSet.Raw.merge t (.ofList [0, 1, 2])
 
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval t.iter.toList
+
 end TreeSet.Raw
 
 namespace TreeSet