theorem
Std.Iterators.IterM.DefaultConsumers.forIn_eq_match_step
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
{n : Type w → Type w''}
[Monad n]
{lift : (γ : Type w) → m γ → n γ}
{γ : Type w}
{plausible_forInStep : β → γ → ForInStep γ → Prop}
{wf : IteratorLoop.WellFounded α m plausible_forInStep}
{it : IterM m β}
{init : γ}
{f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))}
:
forIn lift γ plausible_forInStep wf it init f = do
let __do_lift ← lift it.Step it.step
match __do_lift with
| ⟨IterStep.yield it' out, property⟩ => do
let __do_lift ← f out init
match __do_lift with
| ⟨ForInStep.yield c, property⟩ => forIn lift γ plausible_forInStep wf it' c f
| ⟨ForInStep.done c, property⟩ => pure c
| ⟨IterStep.skip it', property⟩ => forIn lift γ plausible_forInStep wf it' init f
| ⟨IterStep.done, property⟩ => pure init
theorem
Std.Iterators.IterM.forIn_eq
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[IteratorLoop α m n]
[hl : LawfulIteratorLoop α m n]
[MonadLiftT m n]
{γ : Type w}
{it : IterM m β}
{init : γ}
{f : β → γ → n (ForInStep γ)}
:
theorem
Std.Iterators.IterM.forIn_eq_match_step
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[LawfulMonad n]
[IteratorLoop α m n]
[LawfulIteratorLoop α m n]
[MonadLiftT m n]
{γ : Type w}
{it : IterM m β}
{init : γ}
{f : β → γ → n (ForInStep γ)}
:
forIn it init f = do
let __do_lift ← liftM it.step
match __do_lift with
| ⟨IterStep.yield it' out, property⟩ => do
let __do_lift ← f out init
match __do_lift with
| ForInStep.yield c => forIn it' c f
| ForInStep.done c => pure c
| ⟨IterStep.skip it', property⟩ => forIn it' init f
| ⟨IterStep.done, property⟩ => pure init
theorem
Std.Iterators.IterM.forM_eq_forIn
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[LawfulMonad n]
[IteratorLoop α m n]
[LawfulIteratorLoop α m n]
[MonadLiftT m n]
{it : IterM m β}
{f : β → n PUnit}
:
forM it f = forIn it PUnit.unit fun (out : β) (x : PUnit) => do
f out
pure (ForInStep.yield PUnit.unit)
theorem
Std.Iterators.IterM.forM_eq_match_step
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[LawfulMonad n]
[IteratorLoop α m n]
[LawfulIteratorLoop α m n]
[MonadLiftT m n]
{it : IterM m β}
{f : β → n PUnit}
:
forM it f = do
let __do_lift ← liftM it.step
match __do_lift with
| ⟨IterStep.yield it' out, property⟩ => do
f out
forM it' f
| ⟨IterStep.skip it', property⟩ => forM it' f
| ⟨IterStep.done, property⟩ => pure PUnit.unit
theorem
Std.Iterators.IterM.foldM_eq_forIn
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[IteratorLoop α m n]
[MonadLiftT m n]
{f : γ → β → n γ}
{init : γ}
{it : IterM m β}
:
theorem
Std.Iterators.IterM.forIn_yield_eq_foldM
{α β γ δ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[LawfulMonad n]
[IteratorLoop α m n]
[LawfulIteratorLoop α m n]
[MonadLiftT m n]
{f : β → γ → n δ}
{g : β → γ → δ → γ}
{init : γ}
{it : IterM m β}
:
theorem
Std.Iterators.IterM.foldM_eq_match_step
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
{n : Type w → Type w''}
[Monad n]
[LawfulMonad n]
[IteratorLoop α m n]
[LawfulIteratorLoop α m n]
[MonadLiftT m n]
{f : γ → β → n γ}
{init : γ}
{it : IterM m β}
:
theorem
Std.Iterators.IterM.fold_eq_forIn
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[IteratorLoop α m m]
{f : γ → β → γ}
{init : γ}
{it : IterM m β}
:
theorem
Std.Iterators.IterM.fold_eq_foldM
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
{f : γ → β → γ}
{init : γ}
{it : IterM m β}
:
@[simp]
theorem
Std.Iterators.IterM.forIn_pure_yield_eq_fold
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
{f : β → γ → γ}
{init : γ}
{it : IterM m β}
:
(forIn it init fun (c : β) (b : γ) => pure (ForInStep.yield (f c b))) = fold (fun (b : γ) (c : β) => f c b) init it
theorem
Std.Iterators.IterM.fold_eq_match_step
{α β γ : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
{f : γ → β → γ}
{init : γ}
{it : IterM m β}
:
fold f init it = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, property⟩ => fold f (f init out) it'
| ⟨IterStep.skip it', property⟩ => fold f init it'
| ⟨IterStep.done, property⟩ => pure init
theorem
Std.Iterators.IterM.toList_eq_fold
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
[IteratorCollect α m m]
[LawfulIteratorCollect α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_fold
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[IteratorLoop α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_foldM
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_forIn
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[IteratorLoop α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_match_step
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
{it : IterM m β}
:
it.drain = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, property⟩ => it'.drain
| ⟨IterStep.skip it', property⟩ => it'.drain
| ⟨IterStep.done, property⟩ => pure PUnit.unit
theorem
Std.Iterators.IterM.drain_eq_map_toList
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
[IteratorCollect α m m]
[LawfulIteratorCollect α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_map_toListRev
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
[IteratorCollect α m m]
[LawfulIteratorCollect α m m]
{it : IterM m β}
:
theorem
Std.Iterators.IterM.drain_eq_map_toArray
{α β : Type w}
{m : Type w → Type w'}
[Iterator α m β]
[Finite α m]
[Monad m]
[LawfulMonad m]
[IteratorLoop α m m]
[LawfulIteratorLoop α m m]
[IteratorCollect α m m]
[LawfulIteratorCollect α m m]
{it : IterM m β}
: