List iterator

This module provides an iterator for lists that is accessible via List.iterM.

structure Std.Iterators.ListIterator (α : Type w) : Type w

The underlying state of a list iterator. Its contents are internal and should not be used by downstream users of the library.

• list : List α

@[inline]

def List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] : Std.IterM m α

Returns a finite iterator for the given list. The iterator yields the elements of the list in order and then terminates.

@[inline]

instance Std.Iterators.instIteratorListIteratorOfPure {m : Type w → Type w'} {α : Type w} [Pure m] : Iterator (ListIterator α) m α

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