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 γ)}
:
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 γ}
:
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 ⋯
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_filter
{α β : Type w}
[Iterator α Id β]
{it : Iter β}
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
[Finite α Id]
{f : β → Bool}
:
@[simp]
theorem
Std.Iterators.Iter.toListRev_filterMap
{α β γ : Type w}
[Iterator α Id β]
{it : Iter β}
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
[Finite α Id]
{f : β → Option γ}
:
@[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_filter
{α β : Type w}
[Iterator α Id β]
{it : Iter β}
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
[Finite α Id]
{f : β → Bool}
: