source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerYield_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ it₁' : IterM m β} {it₂' : IterM m γ} {b : β} (h : it₁.IsPlausibleStep (IterStep.yield it₁' b)) :
(IterM.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁' (some it₂')))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerSkip_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ it₁' : IterM m β} (h : it₁.IsPlausibleStep (IterStep.skip it₁')) :
(IterM.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁' none))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerDone_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} (h : it₁.IsPlausibleStep IterStep.done) :
(IterM.flatMapAfterM f it₁ none).IsPlausibleStep IterStep.done
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerYield_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ it₂' : IterM m γ} {b : γ} (h : it₂.IsPlausibleStep (IterStep.yield it₂' b)) :
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (IterM.flatMapAfterM f it₁ (some it₂')) b)
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerSkip_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ it₂' : IterM m γ} (h : it₂.IsPlausibleStep (IterStep.skip it₂')) :
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁ (some it₂')))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerDone_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ : IterM m γ} (h : it₂.IsPlausibleStep IterStep.done) :
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁ none))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerYield_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ it₁' : IterM m β} {b : β} (h : it₁.IsPlausibleStep (IterStep.yield it₁' b)) :
(IterM.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁' (some (f b))))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerSkip_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ it₁' : IterM m β} (h : it₁.IsPlausibleStep (IterStep.skip it₁')) :
(IterM.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁' none))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.outerDone_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} (h : it₁.IsPlausibleStep IterStep.done) :
(IterM.flatMapAfter f it₁ none).IsPlausibleStep IterStep.done
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerYield_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ it₂' : IterM m γ} {b : γ} (h : it₂.IsPlausibleStep (IterStep.yield it₂' b)) :
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (IterM.flatMapAfter f it₁ (some it₂')) b)
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerSkip_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ it₂' : IterM m γ} (h : it₂.IsPlausibleStep (IterStep.skip it₂')) :
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁ (some it₂')))
source
theorem Std.Iterators.Flatten.IsPlausibleStep.innerDone_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ : IterM m γ} (h : it₂.IsPlausibleStep IterStep.done) :
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁ none))
source
theorem Std.Iterators.IterM.step_flatMapAfterM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).step = match it₂ with | none => do let __do_lift ← it₁.step match __do_lift.inflate with | ⟨IterStep.yield it₁' b, h⟩ => do let __do_lift ← f b pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some __do_lift)) ⋯)) | ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' none) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯)) | some it₂ => do let __do_lift ← it₂.step match __do_lift.inflate with | ⟨IterStep.yield it₂' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (flatMapAfterM f it₁ (some it₂')) out ⋯)) | ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ (some it₂')) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ none) ⋯))
source
theorem Std.Iterators.IterM.step_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : IterM m β} :
(flatMapM f it₁).step = do let __do_lift ← it₁.step match __do_lift.inflate with | ⟨IterStep.yield it₁' b, h⟩ => do let __do_lift ← f b pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some __do_lift)) ⋯)) | ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' none) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
source
theorem Std.Iterators.IterM.step_flatMapAfter {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfter f it₁ it₂).step = match it₂ with | none => do let __do_lift ← it₁.step match __do_lift.inflate with | ⟨IterStep.yield it₁' b, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯)) | ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯)) | some it₂ => do let __do_lift ← it₂.step match __do_lift.inflate with | ⟨IterStep.yield it₂' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (flatMapAfter f it₁ (some it₂')) out ⋯)) | ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁ (some it₂')) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁ none) ⋯))
source
theorem Std.Iterators.IterM.step_flatMap {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] {f : β → IterM m γ} {it₁ : IterM m β} :
(flatMap f it₁).step = do let __do_lift ← it₁.step match __do_lift.inflate with | ⟨IterStep.yield it₁' b, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯)) | ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
source
theorem Std.Iterators.IterM.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).toList = match it₂ with | none => List.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toList) it₁).toList | some it₂ => do let __do_lift ← it₂.toList let __do_lift_1 ← List.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toList) it₁).toList pure (__do_lift ++ __do_lift_1)
source
theorem Std.Iterators.IterM.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → m (IterM m γ)} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).toArray = match it₂ with | none => Array.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toArray) it₁).toArray | some it₂ => do let __do_lift ← it₂.toArray let __do_lift_1 ← Array.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toArray) it₁).toArray pure (__do_lift ++ __do_lift_1)
source
theorem Std.Iterators.IterM.toList_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → m (IterM m γ)} {it₁ : IterM m β} :
(flatMapM f it₁).toList = List.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toList) it₁).toList
source
theorem Std.Iterators.IterM.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → m (IterM m γ)} {it₁ : IterM m β} :
(flatMapM f it₁).toArray = Array.flatten <$> (mapM (fun (b : β) => do let __do_lift ← f b __do_lift.toArray) it₁).toArray
source
theorem Std.Iterators.IterM.toList_flatMapAfter {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfter f it₁ it₂).toList = match it₂ with | none => List.flatten <$> (mapM (fun (b : β) => (f b).toList) it₁).toList | some it₂ => do let __do_lift ← it₂.toList let __do_lift_1 ← List.flatten <$> (mapM (fun (b : β) => (f b).toList) it₁).toList pure (__do_lift ++ __do_lift_1)
source
theorem Std.Iterators.IterM.toArray_flatMapAfter {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → IterM m γ} {it₁ : IterM m β} {it₂ : Option (IterM m γ)} :
(flatMapAfter f it₁ it₂).toArray = match it₂ with | none => Array.flatten <$> (mapM (fun (b : β) => (f b).toArray) it₁).toArray | some it₂ => do let __do_lift ← it₂.toArray let __do_lift_1 ← Array.flatten <$> (mapM (fun (b : β) => (f b).toArray) it₁).toArray pure (__do_lift ++ __do_lift_1)
source
theorem Std.Iterators.IterM.toList_flatMap {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → IterM m γ} {it₁ : IterM m β} :
(flatMap f it₁).toList = List.flatten <$> (mapM (fun (b : β) => (f b).toList) it₁).toList
source
theorem Std.Iterators.IterM.toArray_flatMap {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m] [IteratorCollect α m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m] {f : β → IterM m γ} {it₁ : IterM m β} :
(flatMap f it₁).toArray = Array.flatten <$> (mapM (fun (b : β) => (f b).toArray) it₁).toArray