chore: add comments

Author: wkrozowski

src/Std/Data/DTreeMap/Iterator.lean

@@ -7,17 +7,53 @@ module
 
 prelude
 public import Std.Data.DTreeMap.Raw.Iterator
+
+/-!
+# Iterators on `DTreeMap`
+-/
+
 namespace Std.DTreeMap
 open Std.Iterators
 
+/--
+Returns a finite iterator over the entries of a dependent tree map.
+The iterator yields the elements of the map in order and then terminates.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def iter {α : Type u} {β : α → Type v} [Ord α] (m : DTreeMap α β) :=
   Raw.iter ⟨m.inner⟩
 
+/--
+Returns a finite iterator over the keys of a dependent tree map.
+The iterator yields the keys in order and then terminates.
+
+The key and value types must live in the same universe.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def keysIter {α : Type u} {β : α → Type u} [Ord α] (m : Raw α β) :=
   Raw.keysIter ⟨m.inner⟩
 
+/--
+Returns a finite iterator over the values of a tree map.
+The iterator yields the values in order and then terminates.
+
+The key and value types must live in the same universe.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def valuesIter {α : Type u} {β : Type u} [Ord α](m : Raw α (fun _ => β)) :=
   Raw.valuesIter ⟨m.inner⟩

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

@@ -8,17 +8,53 @@ module
 prelude
 public import Std.Data.DTreeMap.Internal.Zipper
 public import Std.Data.DTreeMap
+
+/-!
+# Iterators on `DTreeMap.Raw`
+-/
+
 namespace Std.DTreeMap.Raw
 open Std.Iterators
 
+/--
+Returns a finite iterator over the entries of a dependent tree map.
+The iterator yields the elements of the map in order and then terminates.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def iter {α : Type u} {β : α → Type v} [Ord α] (m : Raw α β) :=
   (Internal.Zipper.iterOfTree m.inner : Iter ((a : α) × β a))
 
+/--
+Returns a finite iterator over the keys of a dependent tree map.
+The iterator yields the keys in order and then terminates.
+
+The key and value types must live in the same universe.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def keysIter {α : Type u} {β : α → Type u} [Ord α] (m : Raw α β) :=
   (m.iter.map fun e => e.1 : Iter α)
 
+/--
+Returns a finite iterator over the values of a tree map.
+The iterator yields the values in order and then terminates.
+
+The key and value types must live in the same universe.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
 @[inline]
 public def valuesIter {α : Type u} {β : Type u} [Ord α](m : Raw α (fun _ => β)) :=
   (m.iter.map fun e => e.2 : Iter β)

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

@@ -10,6 +10,11 @@ public import Std.Data.DTreeMap.Internal.Ordered
 public import Std.Data.DTreeMap.Internal.Zipper
 public import Std.Data.DTreeMap.Raw.Basic
 
+/-!
+This module provides slice notation for `TreeMap` slices and implements an iterator
+for those slices.
+-/
+
 namespace Std.DTreeMap.Raw
 open Std.Iterators
 
@@ -19,7 +24,8 @@ public instance {α : Type u} {β : α → Type v}
   mkSlice carrier range := ⟨carrier.inner, range⟩
 
 @[simp] public theorem toList_rii {α : Type u} {β : α → Type v}
-    (cmp : α → α → Ordering := by exact compare) {t : Raw α β cmp} : t[*...*].toList = t.toList := by
+    (cmp : α → α → Ordering := by exact compare) {t : Raw α β cmp} :
+    t[*...*].toList = t.toList := by
   apply Internal.toList_rii
 
 public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :

src/Std/Data/DTreeMap/Slice.lean

@@ -7,6 +7,12 @@ module
 
 prelude
 public import Std.Data.DTreeMap.Raw.Slice
+
+/-!
+This module provides slice notation for `TreeMap` slices and implements an iterator
+for those slices.
+-/
+
 namespace Std.DTreeMap
 open Std.Iterators