# List iterator #

This module provides an iterator for lists that is accessible via `List.iter`.

source
@[inline]
def List.iter {α : Type w} (l : List α) :
Std.Iter α

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

The monadic version of this iterator is `List.iterM`.

Termination properties:

- `Finite` instance: always
- `Productive` instance: always

Equations

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

Instances For