docs/cleanups

Author: datokrat

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.ULift
---import all Init.Data.Iterators.Combinators.Monadic.ULift
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 

src/Init/Data/Range/Polymorphic/Lemmas.lean

@@ -819,6 +819,23 @@ public theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α]
         #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
 
+public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
+    [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
+    r.toArray = if r.lower < r.upper then
+        match UpwardEnumerable.succ? r.lower with
+        | none => #[r.lower]
+        | some next => #[r.lower] ++ (next...r.upper).toArray
+      else
+        #[] := by
+  rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]
+  simp only [Internal.iter]
+  split
+  · split
+    · simp [Rxo.Iterator.toArray_eq_match, *]
+    · simp only [*]
+      rfl
+  · rfl
+
 @[deprecated toArray_eq_if_roo (since := "2025-10-29")]
 def toArray_eq_if := @toArray_eq_if_roo
 

src/Init/Data/Slice/Operations.lean

@@ -28,12 +28,22 @@ and use `Std.Slice.iter` instead.
 def Internal.iter (s : Slice γ) [ToIterator s Id β] :=
   ToIterator.iter s
 
+/--
+This type class provides support for the `Slice.size` function.
+-/
 class SliceSize (α : Type u) where
+  /-- Computes the slice of a `Slice`. Use `Slice.size` instead. -/
   size (slice : Slice α) : Nat
 
+/--
+This type class states that the slice's iterator emits exactly `Slice.size` elements before
+terminating.
+-/
 class LawfulSliceSize (α : Type u) [SliceSize α] [∀ s : Slice α, ToIterator s Id β]
     [∀ s : Slice α, Iterator (ToIterator.State s Id) Id β] where
+  /-- The iterator for every `Slice α` is finite. -/
   [finite : ∀ s : Slice α, Finite (ToIterator.State s Id) Id]
+  /-- The iterator of a slice `s` of type `Slice α` emits exactly `SliceSize.size s` elements. -/
   lawful :
       letI (s : Slice α) : IteratorLoop (ToIterator.State s Id) Id Id := .defaultImplementation
       ∀ s : Slice α, SliceSize.size s = (ToIterator.iter s).count

tests/lean/run/rangePolymorphic.lean

@@ -39,8 +39,7 @@ open Std.Iterators
 #eval (2<...<15).iter.stepSize 2 |>.toList
 
 example : (1...5).size = 4 := by
-  rw [← Std.Rco.size_toArray]
-  simp [Std.Rco.toArray_eq_if, Std.Roo.toArray_eq_match_rco]
+  simp [← Std.Rco.size_toArray, Std.Rco.toArray_eq_if_rco]
 
 /-- info: true -/
 #guard_msgs in