theorem Std.IterM.toArray_eq_match_step {α β : Type w} {m : Type w → Type w'} {it : IterM m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] : it.toArray = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toArray pure (#[out] ++ __do_lift) | IterStep.skip it' => it'.toArray | IterStep.done => pure #[]

@[simp]

theorem Std.IterM.toArray_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toArray = it.toArray

theorem Std.IterM.toArray_ensureTermination_eq_match_step {α β : Type w} {m : Type w → Type w'} {it : IterM m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] : it.ensureTermination.toArray = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toArray pure (#[out] ++ __do_lift) | IterStep.skip it' => it'.toArray | IterStep.done => pure #[]

@[simp]

theorem Std.IterM.toList_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toList = it.toList

@[simp]

theorem Std.IterM.toList_toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : Array.toList <$> it.toArray = it.toList

theorem Std.IterM.toList_toArray_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : Array.toList <$> it.ensureTermination.toArray = it.toList

@[simp]

theorem Std.IterM.toArray_toList {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : List.toArray <$> it.toList = it.toArray

theorem Std.IterM.toArray_toList_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : List.toArray <$> it.ensureTermination.toList = it.toArray

theorem Std.IterM.toList_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.toList = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toList pure (out :: __do_lift) | IterStep.skip it' => it'.toList | IterStep.done => pure []

theorem Std.IterM.toList_ensureTermination_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toList = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toList pure (out :: __do_lift) | IterStep.skip it' => it'.toList | IterStep.done => pure []

@[simp]

theorem Std.IterM.toListRev_ensureTermination_eq_toListRev {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toListRev = it.toListRev

theorem Std.IterM.toListRev_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.toListRev = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toListRev pure (__do_lift ++ [out]) | IterStep.skip it' => it'.toListRev | IterStep.done => pure []

theorem Std.IterM.toListRev_ensureTermination_eq_match_step {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toListRev = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' out => do let __do_lift ← it'.toListRev pure (__do_lift ++ [out]) | IterStep.skip it' => it'.toListRev | IterStep.done => pure []

@[simp]

theorem Std.IterM.reverse_toListRev {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : List.reverse <$> it.toListRev = it.toList

@[simp]

theorem Std.IterM.reverse_toListRev_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : List.reverse <$> it.ensureTermination.toListRev = it.toList

theorem Std.IterM.toListRev_eq {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.toListRev = List.reverse <$> it.toList

theorem Std.IterM.toListRev_ensureTermination {α β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} : it.ensureTermination.toListRev = List.reverse <$> it.toList