PRange.iter

Author: datokrat

src/Std/Data/Iterators/Lemmas/Producers/Range.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Producers.Range
+
+namespace Std.PRange
+
+theorem toList_iter_eq_toList [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    [SupportsUpperBound su α] [HasFiniteRanges su α] [LawfulUpwardEnumerable α]
+    (r : PRange ⟨sl, su⟩ α) :
+    r.iter.toList = r.toList := by
+  rfl
+
+end Std.PRange

src/Std/Data/Iterators/Producers.lean

@@ -8,4 +8,5 @@ import Std.Data.Iterators.Producers.Monadic
 import Std.Data.Iterators.Producers.Array
 import Std.Data.Iterators.Producers.Empty
 import Std.Data.Iterators.Producers.List
+import Std.Data.Iterators.Producers.Range
 import Std.Data.Iterators.Producers.Repeat

src/Std/Data/Iterators/Producers/Range.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.Range.Polymorphic.Basic
+
+/-!
+# Range iterator
+
+This module provides iterators over ranges from `Std.PRange` via `Std.PRange.iter`.
+-/
+
+open Std.PRange
+
+/--
+Returns an iterator over the given range. This iterator will emit the elements of the range
+in increasing order.
+-/
+@[always_inline, inline]
+def Std.PRange.iter [UpwardEnumerable α] [BoundedUpwardEnumerable sl α]
+    (r : PRange ⟨sl, su⟩ α) : Iter (α := RangeIterator su α) α :=
+  ⟨⟨BoundedUpwardEnumerable.init? r.lower, r.upper⟩⟩

tests/lean/run/range.lean

@@ -3,7 +3,7 @@ import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Range.Polymorphic.Basic
 import Init.System.IO
 import Init.Data.Iterators
-import Init
+import Std.Data.Iterators
 
 def ex1 : IO Unit := do
 IO.println "example 1"