We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent d112d75 commit 01440c8Copy full SHA for 01440c8
src/Std/Data/Iterators/Combinators/Monadic/Take.lean
@@ -125,11 +125,11 @@ instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
125
Finite (Take α m β) m :=
126
Finite.of_finitenessRelation instFinitenessRelation
127
128
-instance Take.instIteratorToArray [Monad m] [Iterator α m β] [Productive α m] :
+instance Take.instIteratorCollect [Monad m] [Iterator α m β] [Productive α m] :
129
IteratorCollect (Take α m β) m :=
130
.defaultImplementation
131
132
-instance Take.instIteratorToArrayPartial [Monad m] [Iterator α m β] :
+instance Take.instIteratorCollectPartial [Monad m] [Iterator α m β] :
133
IteratorCollectPartial (Take α m β) m :=
134
135
0 commit comments