@[match_pattern, inline]

def Vector.iterFromIdxM {α : Type w} {n : Nat} (xs : Vector α n) (m : Type w → Type w') (pos : Nat) [Pure m] : Std.IterM m α

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

The pure version of this iterator is Vector.iterFromIdx.

Termination properties:

• Finite instance: always

• Productive instance: always

Equations

• xs.iterFromIdxM m pos = xs.toArray.iterFromIdxM m pos

@[inline]

def Vector.iterM {α : Type u_1} {n : Nat} (xs : Vector α n) (m : Type u_1 → Type u_2) [Pure m] : Std.IterM m α

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

The pure version of this iterator is Vector.iter.

Termination properties:

• Finite instance: always

• Productive instance: always

Equations

• xs.iterM m = xs.toArray.iterM m