source
theorem Std.Iterators.stepAsHetT_filterMapWithPostcondition {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α β γ : Type u_1} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → PostconditionT n (Option γ)} {it : IterM m β} :
(IterM.filterMapWithPostcondition f it).stepAsHetT = (HetT.liftInner n it.stepAsHetT).bind fun (x : IterStep (IterM m β) β) => match x with | IterStep.yield it' out => do let __do_lift ← HetT.ofPostconditionT (f out) match __do_lift with | some out' => pure (IterStep.yield (IterM.filterMapWithPostcondition f it') out') | none => pure (IterStep.skip (IterM.filterMapWithPostcondition f it')) | IterStep.skip it' => pure (IterStep.skip (IterM.filterMapWithPostcondition f it')) | IterStep.done => pure IterStep.done
source
theorem Std.Iterators.IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → PostconditionT n (Option γ)} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filterMapWithPostcondition f ita).Equiv (IterM.filterMapWithPostcondition f itb)
source
theorem Std.Iterators.IterM.Equiv.filterWithPostcondition {α₁ α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → PostconditionT n (ULift Bool)} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filterWithPostcondition f ita).Equiv (IterM.filterWithPostcondition f itb)
source
theorem Std.Iterators.IterM.Equiv.mapWithPostcondition {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → PostconditionT n γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.mapWithPostcondition f ita).Equiv (IterM.mapWithPostcondition f itb)
source
theorem Std.Iterators.IterM.Equiv.filterMapM {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filterMapM f ita).Equiv (IterM.filterMapM f itb)
source
theorem Std.Iterators.IterM.Equiv.filterM {α₁ α₂ β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift Bool)} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filterM f ita).Equiv (IterM.filterM f itb)
source
theorem Std.Iterators.IterM.Equiv.mapM {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Iterator α₁ m β] [Iterator α₂ m β] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.mapM f ita).Equiv (IterM.mapM f itb)
source
theorem Std.Iterators.IterM.Equiv.filterMap {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {f : β → Option γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filterMap f ita).Equiv (IterM.filterMap f itb)
source
theorem Std.Iterators.IterM.Equiv.filter {α₁ α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {f : β → Bool} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.filter f ita).Equiv (IterM.filter f itb)
source
theorem Std.Iterators.IterM.Equiv.map {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {f : β → γ} {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) :
(IterM.map f ita).Equiv (IterM.map f itb)