@[inline]

def Vector.iterFromIdx {n : Nat} {α : Type w} (xs : Vector α n) (pos : Nat) : Std.Iter α

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

The monadic version of this iterator is Vector.iterFromIdxM.

Termination properties:

• Finite instance: always

• Productive instance: always

Equations

• xs.iterFromIdx pos = xs.toArray.iterFromIdx pos

@[inline]

def Vector.iter {n : Nat} {α : Type w} (xs : Vector α n) : Std.Iter α

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

The monadic version of this iterator is Vector.iterM.

Termination properties:

• Finite instance: always

• Productive instance: always

Equations

• xs.iter = xs.toArray.iter