Skip to content

Commit e75744d

Browse files
committed
fix typo
1 parent 5550763 commit e75744d

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/Init/Data/Iterators/Consumers/Collect.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ lists are prepend-only, this `toListRev` is usually more efficient that `toList`
7878
7979
This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
8080
-/
81-
@[always_inline, inline, deprecated Iter.toListRev (since := "2025-10-16")]
81+
@[always_inline, inline, deprecated Iter.toListRev (since := "2025-10-23")]
8282
def Iter.Partial.toListRev {α : Type w} {β : Type w}
8383
[Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
8484
it.it.toListRev

src/Init/Data/Iterators/Consumers/Monadic/Collect.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ where
8484
| .done => return acc) it acc
8585

8686
/--
87-
This is the default implementation of the `IteratorLoop` class.
87+
This is the default implementation of the `IteratorCollect` class.
8888
It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
8989
data structure. For certain iterators, more efficient implementations are possible and should be
9090
used instead.

0 commit comments

Comments
 (0)