Documentation

Std.Data.Iterators.Producers.Monadic.Array

Array iterator #

This module provides an iterator for arrays that is accessible via Array.iterM.

source
@[unbox]
structure Std.Iterators.ArrayIterator (α : 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.

  • array : Array α

    Internal implementation detail of the iterator library.

  • pos : Nat

    Internal implementation detail of the iterator library.

Instances For
    source
    @[inline]
    def Array.iterFromIdxM {α : Type w} (array : Array α) (m : Type w → Type w') (pos : Nat) [Pure m] :
    Std.IterM m α

    Returns a finite monadic iterator for the given array starting at the given index. The iterator yields the elements of the array in order and then terminates.

    The pure version of this iterator is Array.iterFromIdx.

    Termination properties:

    • Finite instance: always
    • Productive instance: always
    Equations
      Instances For
        source
        @[inline]
        def Array.iterM {α : Type w} (array : Array α) (m : Type w → Type w') [Pure m] :
        Std.IterM m α

        Returns a finite monadic iterator for the given array. The iterator yields the elements of the array in order and then terminates. There are no side effects.

        The pure version of this iterator is Array.iter.

        Termination properties:

        • Finite instance: always
        • Productive instance: always
        Equations
          Instances For
            source
            @[inline]
            instance Std.Iterators.instIteratorArrayIteratorOfPure {m : Type w → Type w'} {α : Type w} [Pure m] :
            Iterator (ArrayIterator α) m α
            Equations
              source
              instance Std.Iterators.instFiniteArrayIterator {α : Type w} {m : Type w → Type w'} [Pure m] :
              Finite (ArrayIterator α) m
              source
              @[inline]
              instance Std.Iterators.instIteratorCollectArrayIteratorOfMonad {m : Type w → Type w'} {n : Type w → Type u_1} {α : Type w} [Monad m] [Monad n] :
              IteratorCollect (ArrayIterator α) m n
              Equations
                source
                @[inline]
                instance Std.Iterators.instIteratorCollectPartialArrayIteratorOfMonad {m : Type w → Type w'} {n : Type w → Type u_1} {α : Type w} [Monad m] [Monad n] :
                IteratorCollectPartial (ArrayIterator α) m n
                Equations
                  source
                  @[inline]
                  instance Std.Iterators.instIteratorLoopArrayIteratorOfMonad {m : Type w → Type w'} {n : Type w → Type u_1} {α : Type w} [Monad m] [Monad n] :
                  IteratorLoop (ArrayIterator α) m n
                  Equations
                    source
                    @[inline]
                    instance Std.Iterators.instIteratorLoopPartialArrayIteratorOfMonad {m : Type w → Type w'} {n : Type w → Type u_1} {α : Type w} [Monad m] [Monad n] :
                    IteratorLoopPartial (ArrayIterator α) m n
                    Equations