corrections

Author: datokrat

src/Init/Data/Iterators/Combinators/Attach.lean

@@ -14,10 +14,12 @@ namespace Std.Iterators
 @[always_inline, inline, inherit_doc IterM.attachWith]
 def Iter.attachWith {α β : Type w}
     [Iterator α Id β]
-    (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :=
-  haveI h' : ∀ out, it.toIterM.IsPlausibleIndirectOutput out → P out := by
+    (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :
+  Iter (α := Types.Attach α Id P) { out : β // P out } :=
+  (it.toIterM.attachWith P ?h).toIter
+where finally
+  case h =>
     simp only [← isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM]
     exact h
-  ((it.toIterM.attachWith P h').toIter : Iter { out : β // P out })
 
 end Std.Iterators

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -118,8 +118,8 @@ instance {α β : Type w} {m : Type w → Type w'} [Monad m]
 end Types
 
 /--
-“Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning a list
-of iterators in the corresponding subtype `{ x // P x }`.
+“Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning an
+iterator with values in the corresponding subtype `{ x // P x }`.
 
 **Termination properties:**
 

src/Init/Data/Iterators/ToIterator.lean

@@ -15,7 +15,7 @@ converted into iterators.
 
 open Std.Iterators
 
-namespace Std.Slice
+namespace Std.Iterators
 
 /--
 This typeclass provides an iterator for the given element `x : γ`. Usually, instances are provided
@@ -107,4 +107,4 @@ instance {x : γ} {State : Type w} {iter}
     IteratorSizePartial (α := i.State) m :=
   inferInstanceAs <| IteratorSizePartial (α := State) m
 
-end Std.Slice
+end Std.Iterators

src/Init/Data/Slice/Array.lean

@@ -19,7 +19,7 @@ This module provides slice notation for array slices (a.k.a. `Subarray`) and imp
 for those slices.
 -/
 
-open Std Slice PRange
+open Std Slice PRange Iterators
 
 instance {shape} {α : Type u} [ClosedOpenIntersection shape Nat] :
     Sliceable shape (Array α) Nat (Subarray α) where

src/Init/Data/Slice/Operations.lean

@@ -29,7 +29,7 @@ def Internal.iter (s : Slice γ) [ToIterator s Id β] :=
 /--
 Returns the number of elements with distinct indices in the given slice.
 
-Example: `#[1, 1, 1][0...2] = 2`.
+Example: `#[1, 1, 1][0...2].size = 2`.
 -/
 @[always_inline, inline]
 def size (s : Slice g) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β]

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

@@ -12,7 +12,7 @@ import Init.Data.Slice.Operations
 This module provides iterators over slices from `Std.Slice` via `Std.Slice.iter`.
 -/
 
-open Std.Slice
+open Std Slice Iterators
 
 /--
 Returns an iterator over the given slice. This iterator will emit the elements of the slice

tests/lean/run/slice.lean

@@ -27,3 +27,5 @@ example : #[1, 2, 3][1...=1].toList = [2] := by native_decide
 example : #[1, 2, 3][1...<10].size = 2 := by native_decide
 
 example : (#[1, 2, 3][1...*].take 1).toList = [2] := by native_decide
+
+example : #[1, 1, 1][0...2].size = 2 := by native_decide