List iterator

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

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