Array iterator #
This module provides an iterator for arrays that is accessible via Array.iterM
.
@[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: alwaysProductive
instance: always
Equations
- array.iterFromIdxM m pos = Std.Iterators.toIterM { array := array, pos := pos } m α
Instances For
@[inline]
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: alwaysProductive
instance: always
Equations
- array.iterM m = array.iterFromIdxM m 0
Instances For
@[inline]
instance
Std.Iterators.instIteratorArrayIteratorOfPure
{m : Type w → Type w'}
{α : Type w}
[Pure m]
:
Iterator (ArrayIterator α) m α
Equations
- One or more equations did not get rendered due to their size.
instance
Std.Iterators.instFiniteArrayIterator
{α : Type w}
{m : Type w → Type w'}
[Pure m]
:
Finite (ArrayIterator α) m
@[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
@[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
@[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
@[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