Documentation

Std.Data.Iterators.Producers.Array

Array iterator #

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

@[inline]
def Array.iterFromIdx {α : Type w} (l : Array α) (pos : Nat) :

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

The monadic version of this iterator is Array.iterFromIdxM.

Termination properties:

  • Finite instance: always
  • Productive instance: always
Equations
    Instances For
      @[inline]
      def Array.iter {α : Type w} (l : Array α) :

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

      The monadic version of this iterator is Array.iterM.

      Termination properties:

      • Finite instance: always
      • Productive instance: always
      Equations
        Instances For