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.Iterators.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.Iterators.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.Iterators.IterStep.done, ⋯⟩ | x :: xs => pure ⟨Std.Iterators.IterStep.yield (xs.iterM m) x, ⋯⟩

theorem Std.Iterators.ListIterator.toArrayMapped_iterM {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] {β γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ} [Internal.LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} : IteratorCollect.toArrayMapped lift f (l.iterM m) = List.toArray <$> List.mapM f l

@[simp]

theorem List.toArray_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {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

theorem Std.Iterators.ListIterator.stepAsHetT_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {l : List β} : (l.iterM m).stepAsHetT = match l with | [] => pure IterStep.done | x :: xs => pure (IterStep.yield (xs.iterM m) x)