Lemmas about list iterators

This module provides lemmas about the interactions of List.iter with Iter.step and various collectors.

@[simp]

theorem List.step_iter_nil {β : Type w} : [].iter.step = ⟨Std.Iterators.IterStep.done, ⋯⟩

@[simp]

theorem List.step_iter_cons {β : Type w} {x : β} {xs : List β} : (x :: xs).iter.step = ⟨Std.Iterators.IterStep.yield xs.iter x, ⋯⟩

@[simp]

theorem List.toArray_iter {β : Type w} {l : List β} : l.iter.toArray = l.toArray

@[simp]

theorem List.toList_iter {β : Type w} {l : List β} : l.iter.toList = l

@[simp]

theorem List.toListRev_iter {β : Type w} {l : List β} : l.iter.toListRev = l.reverse