List iterator

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

structure Std.Iterators.Types.ListIterator (α : 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.

• list : List α

theorem Std.Iterators.Types.ListIterator.ext {α : Type w} {x y : ListIterator α} (list : x.list = y.list) : x = y

theorem Std.Iterators.Types.ListIterator.ext_iff {α : Type w} {x y : ListIterator α} : x = y ↔ x.list = y.list

@[inline]

def List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] : Std.IterM m α

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

The non-monadic version of this iterator is List.iter.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• l.iterM m = { internalState := { list := l } }

@[instance_reducible, inline]

instance Std.Iterators.Types.ListIterator.instIterator {m : Type w → Type w'} {α : Type w} [Pure m] : Iterator (ListIterator α) m α

Equations

• One or more equations did not get rendered due to their size.

instance Std.Iterators.Types.ListIterator.instFinite {α : Type w} {m : Type w → Type w'} [Pure m] : Finite (ListIterator α) m

@[instance_reducible, inline]

instance Std.Iterators.Types.ListIterator.instIteratorLoop {m : Type w → Type w'} {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] : IteratorLoop (ListIterator α) m n

Equations

• Std.Iterators.Types.ListIterator.instIteratorLoop = Std.IteratorLoop.defaultImplementation