seekIdx? -> atIdxSlow?

Author: datokrat

src/Std/Data/Iterators/Consumers/Access.lean

@@ -15,18 +15,18 @@ before emitting `n` values.
 
 This function requires a `Productive` instance proving that the iterator will always emit a value
 after a finite number of skips. If the iterator is not productive or such an instance is not
-available, consider using `it.allowNontermination.seekIdx?` instead of `it.seekIdx?`. However, it is
-not possible to formally verify the behavior of the partial variant.
+available, consider using `it.allowNontermination.atIdxSlow?` instead of `it.atIdxSlow?`. However,
+it is not possible to formally verify the behavior of the partial variant.
 -/
 @[specialize]
-def Iter.seekIdx? {α β} [Iterator α Id β] [Productive α Id]
+def Iter.atIdxSlow? {α β} [Iterator α Id β] [Productive α Id]
     (n : Nat) (it : Iter (α := α) β) : Option β :=
   match it.step with
   | .yield it' out _ =>
     match n with
     | 0 => some out
-    | k + 1 => it'.seekIdx? k
-  | .skip it' _ => it'.seekIdx? n
+    | k + 1 => it'.atIdxSlow? k
+  | .skip it' _ => it'.atIdxSlow? n
   | .done _ => none
 termination_by (n, it.finitelyManySkips)
 
@@ -36,17 +36,17 @@ returns the `n`-th emitted value, or `none` if `it` finished
 before emitting `n` values.
 
 This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Productive` instance, consider using `Iter.seekIdx?` instead.
+its behavior. If the iterator has a `Productive` instance, consider using `Iter.atIdxSlow?` instead.
 -/
 @[specialize]
-partial def Iter.Partial.seekIdx? {α β} [Iterator α Id β] [Monad Id]
+partial def Iter.Partial.atIdxSlow? {α β} [Iterator α Id β] [Monad Id]
     (n : Nat) (it : Iter.Partial (α := α) β) : Option β := do
   match it.it.step with
   | .yield it' out _ =>
     match n with
     | 0 => some out
-    | k + 1 => (⟨it'⟩ : Iter.Partial (α := α) β).seekIdx? k
-  | .skip it' _ => (⟨it'⟩ : Iter.Partial (α := α) β).seekIdx? n
+    | k + 1 => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? k
+  | .skip it' _ => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? n
   | .done _ => none
 
 end Std.Iterators

src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -86,24 +86,24 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id]
   generalize it.toIterM.step = step
   cases step using PlausibleIterStep.casesOn <;> simp
 
-theorem Iter.getElem?_toList_eq_seekIdx? {α β}
+theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
     [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id]
     {it : Iter (α := α) β} {k : Nat} :
-    it.toList[k]? = it.seekIdx? k := by
+    it.toList[k]? = it.atIdxSlow? k := by
   induction it using Iter.inductSteps generalizing k with | step it ihy ihs =>
-  rw [toList_eq_match_step, seekIdx?]
+  rw [toList_eq_match_step, atIdxSlow?]
   obtain ⟨step, h⟩ := it.step
   cases step
   · cases k <;> simp [ihy h]
   · simp [ihs h]
   · simp
 
-theorem Iter.toList_eq_of_seekIdx?_eq {α₁ α₂ β}
+theorem Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β}
     [Iterator α₁ Id β] [Finite α₁ Id] [IteratorCollect α₁ Id] [LawfulIteratorCollect α₁ Id]
     [Iterator α₂ Id β] [Finite α₂ Id] [IteratorCollect α₂ Id] [LawfulIteratorCollect α₂ Id]
     {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β}
-    (h : ∀ k, it₁.seekIdx? k = it₂.seekIdx? k) :
+    (h : ∀ k, it₁.atIdxSlow? k = it₂.atIdxSlow? k) :
     it₁.toList = it₂.toList := by
-  ext; simp [getElem?_toList_eq_seekIdx?, h]
+  ext; simp [getElem?_toList_eq_atIdxSlow?, h]
 
 end Std.Iterators