Documentation

Std.Data.Iterators.Lemmas.Combinators.FilterMap

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 γ)} :
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)} :
theorem Std.Iterators.Iter.mapM_eq_toIter_mapM_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : βm γ} :
theorem Std.Iterators.Iter.map_eq_toIter_map_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : βγ} :
theorem Std.Iterators.Iter.filter_eq_toIter_filter_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : βBool} :
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] :
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] :
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_liftf 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_liftf 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
def 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
Equations
  • =
Instances For
    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
    • =
    Instances For
      @[simp]
      theorem Std.Iterators.Iter.toList_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βOption γ} :
      @[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} :
      @[simp]
      @[simp]
      theorem Std.Iterators.Iter.toListRev_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βγ} :
      @[simp]
      theorem Std.Iterators.Iter.toListRev_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βBool} :
      @[simp]
      theorem Std.Iterators.Iter.toArray_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βOption γ} :
      @[simp]
      theorem Std.Iterators.Iter.toArray_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βγ} :
      @[simp]
      theorem Std.Iterators.Iter.toArray_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] [Finite α Id] {f : βBool} :