theorem Std.Iterators.Iter.filterMapWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → PostconditionT m (Option γ)} : filterMapWithPostcondition f it = IterM.filterMapWithPostcondition f it.toIterM

theorem Std.Iterators.Iter.filterWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → PostconditionT m (ULift Bool)} : filterWithPostcondition f it = IterM.filterWithPostcondition f it.toIterM

theorem Std.Iterators.Iter.mapWithPostcondition_eq_toIter_mapWithPostcondition_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → PostconditionT m γ} : mapWithPostcondition f it = IterM.mapWithPostcondition f it.toIterM

theorem Std.Iterators.Iter.filterMapM_eq_toIter_filterMapM_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → m (Option γ)} : filterMapM f it = IterM.filterMapM f it.toIterM

theorem Std.Iterators.Iter.filterM_eq_toIter_filterM_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → m (ULift Bool)} : filterM f it = IterM.filterM f it.toIterM

theorem Std.Iterators.Iter.mapM_eq_toIter_mapM_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → m γ} : mapM f it = IterM.mapM f it.toIterM

theorem Std.Iterators.Iter.filterMap_eq_toIter_filterMap_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → Option γ} : filterMap f it = (IterM.filterMap f it.toIterM).toIter

theorem Std.Iterators.Iter.map_eq_toIter_map_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → γ} : map f it = (IterM.map f it.toIterM).toIter

theorem Std.Iterators.Iter.filter_eq_toIter_filter_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → Bool} : filter f it = (IterM.filter f it.toIterM).toIter

theorem Std.Iterators.Iter.step_filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → PostconditionT n (Option γ)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterMapWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨none, h'⟩ => pure (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯) | ⟨some out', h'⟩ => pure (PlausibleIterStep.yield (filterMapWithPostcondition f it') out' ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_filterWithPostcondition {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → PostconditionT n (ULift Bool)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨{ down := false }, h'⟩ => pure (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯) | ⟨{ down := true }, h'⟩ => pure (PlausibleIterStep.yield (filterWithPostcondition f it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → PostconditionT n γ} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (mapWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let out' ← (f out).operation pure (PlausibleIterStep.yield (mapWithPostcondition f it') out'.val ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (mapWithPostcondition f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_filterMapM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {β' : Type w} {f : β → n (Option β')} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterMapM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out match __do_lift with | none => pure (PlausibleIterStep.skip (filterMapM f it') ⋯) | some out' => pure (PlausibleIterStep.yield (filterMapM f it') out' ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (filterMapM f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_filterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → n (ULift Bool)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out match __do_lift with | { down := false } => pure (PlausibleIterStep.skip (filterM f it') ⋯) | { down := true } => pure (PlausibleIterStep.yield (filterM f it') out ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (filterM f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_mapM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → n γ} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (mapM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let out' ← f out pure (PlausibleIterStep.yield (mapM f it') out' ⋯) | ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (mapM f it') ⋯) | ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)

theorem Std.Iterators.Iter.step_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → Option γ} : (filterMap f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => match h' : f out with | none => PlausibleIterStep.skip (filterMap f it') ⋯ | some out' => PlausibleIterStep.yield (filterMap f it') out' ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (filterMap f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iterators.Iter.step_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → γ} : (map f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield (map f it') (f out) ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (map f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

def Std.Iterators.Iter.step_filter {α β : Type w} [Iterator α Id β] {it : Iter β} {f : β → Bool} : (filter f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => if h' : f out = true then PlausibleIterStep.yield (filter f it') out ⋯ else PlausibleIterStep.skip (filter f it') ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (filter f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

Equations

• ⋯ = ⋯

@[simp]

theorem Std.Iterators.Iter.toList_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Option γ} : (filterMap f it).toList = List.filterMap f it.toList

@[simp]

theorem Std.Iterators.Iter.toList_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → γ} : (map f it).toList = List.map f it.toList

@[simp]

theorem Std.Iterators.Iter.toList_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Bool} : (filter f it).toList = List.filter f it.toList

@[simp]

theorem Std.Iterators.Iter.toListRev_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Option γ} : (filterMap f it).toListRev = List.filterMap f it.toListRev

@[simp]

theorem Std.Iterators.Iter.toListRev_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → γ} : (map f it).toListRev = List.map f it.toListRev

@[simp]

theorem Std.Iterators.Iter.toListRev_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Bool} : (filter f it).toListRev = List.filter f it.toListRev

@[simp]

theorem Std.Iterators.Iter.toArray_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Option γ} : (filterMap f it).toArray = Array.filterMap f it.toArray

@[simp]

theorem Std.Iterators.Iter.toArray_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → γ} : (map f it).toArray = Array.map f it.toArray

@[simp]

theorem Std.Iterators.Iter.toArray_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : β → Bool} : (filter f it).toArray = Array.filter f it.toArray