# 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
theorem Std.Iterators.ArrayIterator.ext_iff {α : Type w} {x y : ArrayIterator α} :
x = y ↔ x.array = y.array ∧ x.pos = y.pos
source
theorem Std.Iterators.ArrayIterator.ext {α : Type w} {x y : ArrayIterator α} (array : x.array = y.array) (pos : x.pos = y.pos) :
x = y
source
theorem Std.Iterators.ArrayIterator.exists_iff {α : Type w} {P : ArrayIterator α → Prop} :
(∃ (s : ArrayIterator α), P s) ↔ ∃ (array : Array α), ∃ (pos : Nat), P { array := array, pos := pos }
source
@[match_pattern, 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

- array.iterFromIdxM m pos = Std.Iterators.toIterM { array := array, pos := pos } m α

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

- array.iterM m = array.iterFromIdxM m 0

Instances For

source
@[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.

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'} {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollect (ArrayIterator α) m n
Equations

- Std.Iterators.instIteratorCollectArrayIteratorOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

source
@[inline]
instance Std.Iterators.instIteratorCollectPartialArrayIteratorOfMonad {m : Type w → Type w'} {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollectPartial (ArrayIterator α) m n
Equations

- Std.Iterators.instIteratorCollectPartialArrayIteratorOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
@[inline]
instance Std.Iterators.instIteratorLoopArrayIteratorOfMonad {m : Type w → Type w'} {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoop (ArrayIterator α) m n
Equations

- Std.Iterators.instIteratorLoopArrayIteratorOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

source
@[inline]
instance Std.Iterators.instIteratorLoopPartialArrayIteratorOfMonad {m : Type w → Type w'} {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoopPartial (ArrayIterator α) m n
Equations

- Std.Iterators.instIteratorLoopPartialArrayIteratorOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

source
@[inline]
instance Std.Iterators.instIteratorSizeArrayIterator {m : Type w → Type w'} {α : Type w} [Monad m] :
IteratorSize (ArrayIterator α) m
Equations

- Std.Iterators.instIteratorSizeArrayIterator = Std.Iterators.IteratorSize.defaultImplementation

source
@[inline]
instance Std.Iterators.instIteratorSizePartialArrayIterator {m : Type w → Type w'} {α : Type w} [Monad m] :
IteratorSizePartial (ArrayIterator α) m
Equations

- Std.Iterators.instIteratorSizePartialArrayIterator = Std.Iterators.IteratorSizePartial.defaultImplementation