List iterator #
This module provides an iterator for lists that is accessible via List.iterM
.
The underlying state of a list iterator. Its contents are internal and should not be used by downstream users of the library.
- list : List α
Instances For
@[inline]
instance
Std.Iterators.instIteratorListIteratorOfPure
{m : Type w → Type w'}
{α : Type w}
[Pure m]
:
Iterator (ListIterator α) m α
Equations
- One or more equations did not get rendered due to their size.
instance
Std.Iterators.instFiniteListIterator
{α : Type w}
{m : Type w → Type w'}
[Pure m]
:
Finite (ListIterator α) m
@[inline]
instance
Std.Iterators.instIteratorCollectListIteratorOfMonad
{m : Type w → Type w'}
{n : Type w → Type w''}
{α : Type w}
[Monad m]
[Monad n]
:
IteratorCollect (ListIterator α) m n
@[inline]
instance
Std.Iterators.instIteratorCollectPartialListIteratorOfMonad
{m : Type w → Type w'}
{n : Type w → Type w''}
{α : Type w}
[Monad m]
[Monad n]
:
IteratorCollectPartial (ListIterator α) m n
@[inline]
instance
Std.Iterators.instIteratorLoopListIteratorOfMonad
{m : Type w → Type w'}
{n : Type w → Type w''}
{α : Type w}
[Monad m]
[Monad n]
:
IteratorLoop (ListIterator α) m n
@[inline]
instance
Std.Iterators.instIteratorLoopPartialListIteratorOfMonad
{m : Type w → Type w'}
{n : Type w → Type w''}
{α : Type w}
[Monad m]
[Monad n]
:
IteratorLoopPartial (ListIterator α) m n