Lemmas about list iterators

This module provides lemmas about the interactions of List.iterM with IterM.step and various collectors.

@[simp]

theorem List.step_iterM_nil {m : Type w → Type w'} [Monad m] {β : Type w} : ([].iterM m).step = pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)

@[simp]

theorem List.step_iterM_cons {m : Type w → Type w'} [Monad m] {β : Type w} {x : β} {xs : List β} : ((x :: xs).iterM m).step = pure (Std.Shrink.deflate ⟨Std.IterStep.yield (xs.iterM m) x, ⋯⟩)

theorem List.step_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {l : List β} : (l.iterM m).step = match l with | [] => pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩) | x :: xs => pure (Std.Shrink.deflate ⟨Std.IterStep.yield (xs.iterM m) x, ⋯⟩)

@[simp]

theorem List.toArray_iterM {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} {l : List β} : (l.iterM m).toArray = pure l.toArray

@[simp]

theorem List.toList_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {l : List β} : (l.iterM m).toList = pure l

@[simp]

theorem List.toListRev_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {l : List β} : (l.iterM m).toListRev = pure l.reverse