Documentation

Std.Data.Iterators.Producers.Monadic.List

List iterator #

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

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

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

Instances For
    @[inline]
    def List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :

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

    Equations
    Instances For
      @[inline]
      instance Std.Iterators.instIteratorListIteratorOfPure {m : Type w → Type w'} {α : Type w} [Pure 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] :