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) : Std.Iter α

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

• l.iterFromIdx pos = (l.iterFromIdxM Id pos).toIter

@[inline]

def Array.iter {α : Type w} (l : Array α) : Std.Iter α

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

• l.iter = (l.iterM Id).toIter