source
@[unbox]
structure Std.Rxc.Iterator (α : Type u) :
Type u

Internal state of the range iterators. Do not depend on its internals.

- next : Option α
- upperBound : α

Instances For

source
@[inline]
def Std.Rxc.Iterator.Monadic.step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] (it : IterM Id α) :
Iterators.IterStep (IterM Id α) α

The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for iterators of type `Iter`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def Std.Rxc.Iterator.step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] (it : Iter α) :
Iterators.IterStep (Iter α) α

The pure function mapping a range iterator of type `Iter` to the next step of the iterator.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Std.Rxc.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} :
step it = Iterators.IterStep.mapIterator Iterators.IterM.toIter (Monadic.step it.toIterM)
source
@[inline]
instance Std.Rxc.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLE {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] :
Iterators.Iterator (Rxc.Iterator α) Id α
Equations

- One or more equations did not get rendered due to their size.

source
theorem Std.Rxc.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} {step : Iterators.IterStep (IterM Id α) α} :
it.IsPlausibleStep step ↔ step = Monadic.step it
source
theorem Std.Rxc.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} :
it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)
source
theorem Std.Rxc.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} {step : Iterators.IterStep (Iter α) α} :
it.IsPlausibleStep step ↔ step = Iterator.step it
source
theorem Std.Rxc.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} :
it.step = ⟨step it, ⋯⟩
source
instance Std.Rxc.Iterator.instIteratorCollect {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollect (Rxc.Iterator α) Id n
Equations

- Std.Rxc.Iterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

source
instance Std.Rxc.Iterator.instIteratorCollectPartial {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollectPartial (Rxc.Iterator α) Id n
Equations

- Std.Rxc.Iterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
theorem Std.Rxc.Iterator.Monadic.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} (h : it.internalState.next = some a) (hP : a ≤ it.internalState.upperBound) :
it.IsPlausibleOutput a
source
theorem Std.Rxc.Iterator.Monadic.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a ≤ it.internalState.upperBound
source
theorem Std.Rxc.Iterator.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} (h : it.internalState.next = some a) (hP : a ≤ it.internalState.upperBound) :
it.IsPlausibleOutput a
source
theorem Std.Rxc.Iterator.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a ≤ it.internalState.upperBound
source
theorem Std.Rxc.Iterator.Monadic.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it' it : IterM Id α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ a ≤ it.internalState.upperBound ∧ PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
source
theorem Std.Rxc.Iterator.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it' it : Iter α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ a ≤ it.internalState.upperBound ∧ PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
source
theorem Std.Rxc.Iterator.isSome_next_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} {out : α} (h : it.IsPlausibleIndirectOutput out) :
it.internalState.next.isSome = true
source
instance Std.Rxc.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] :
Iterators.Finite (Rxc.Iterator α) Id
source
instance Std.Rxc.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] :
Iterators.Productive (Rxc.Iterator α) Id
source
instance Std.Rxc.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] :
Iterators.IteratorAccess (Rxc.Iterator α) Id
Equations

- One or more equations did not get rendered due to their size.

source
instance Std.Rxc.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] :
Iterators.LawfulDeterministicIterator (Rxc.Iterator α) Id
source
theorem Std.Rxc.Iterator.Monadic.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerable α] {it : IterM Id α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out ∧ out ≤ it.internalState.upperBound
source
theorem Std.Rxc.Iterator.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out ∧ out ≤ it.internalState.upperBound
source
@[inline]
instance Std.Rxc.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoop (Rxc.Iterator α) Id n

An efficient `IteratorLoop` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[irreducible, specialize #[]]
def Std.Rxc.Iterator.instIteratorLoop.loop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (wf : Iterators.IteratorLoop.WellFounded (Rxc.Iterator α) Id Pl) (upperBound least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n { s : ForInStep γ // Pl out c s }) (next : α) (hl : PRange.UpwardEnumerable.LE least next) (hu : next ≤ upperBound) :
n γ
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Std.Rxc.Iterator.instIteratorLoopPartial {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoopPartial (Rxc.Iterator α) Id n

An efficient `IteratorLoop` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[specialize #[]]
partial def Std.Rxc.Iterator.instIteratorLoopPartial.loop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (upperBound least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → out ≤ upperBound → γ → n (ForInStep γ)) (next : α) (hl : PRange.UpwardEnumerable.LE least next) (hu : next ≤ upperBound) :
n γ
source
@[irreducible]
theorem Std.Rxc.Iterator.instIteratorLoop.loop_eq {α : Type u} {least : α} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u} {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ} [Internal.LawfulMonadLiftBindFunction lift] {PlausibleForInStep : α → γ → ForInStep γ → Prop} {upperBound next : α} {hl : PRange.UpwardEnumerable.LE least next} {hu : next ≤ upperBound} {f : (out : α) → PRange.UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n { s : ForInStep γ // PlausibleForInStep out c s }} {acc : γ} {wf : Iterators.IteratorLoop.WellFounded (Rxc.Iterator α) Id PlausibleForInStep} :
loop γ PlausibleForInStep wf upperBound least acc f next hl hu = do let __do_lift ← f next hl hu acc match __do_lift with | ⟨ForInStep.yield c, property⟩ => Iterators.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep wf { internalState := { next := PRange.succ? next, upperBound := upperBound } } c { internalState := { next := PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput ⋯ fun (b : α) (h : { internalState := { next := PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput b) (c : γ) => f b ⋯ ⋯ c | ⟨ForInStep.done c, property⟩ => pure c
source
instance Std.Rxc.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] [LawfulMonad n] :
Iterators.LawfulIteratorLoop (Rxc.Iterator α) Id n
source
@[unbox]
structure Std.Rxo.Iterator (α : Type u) :
Type u

Internal state of the range iterators. Do not depend on its internals.

- next : Option α
- upperBound : α

Instances For

source
@[inline]
def Std.Rxo.Iterator.Monadic.step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] (it : IterM Id α) :
Iterators.IterStep (IterM Id α) α

The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for iterators of type `Iter`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def Std.Rxo.Iterator.step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] (it : Iter α) :
Iterators.IterStep (Iter α) α

The pure function mapping a range iterator of type `Iter` to the next step of the iterator.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Std.Rxo.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} :
step it = Iterators.IterStep.mapIterator Iterators.IterM.toIter (Monadic.step it.toIterM)
source
@[inline]
instance Std.Rxo.instIteratorIteratorIdOfUpwardEnumerableOfDecidableLT {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] :
Iterators.Iterator (Rxo.Iterator α) Id α
Equations

- One or more equations did not get rendered due to their size.

source
theorem Std.Rxo.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} {step : Iterators.IterStep (IterM Id α) α} :
it.IsPlausibleStep step ↔ step = Monadic.step it
source
theorem Std.Rxo.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} :
it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)
source
theorem Std.Rxo.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} {step : Iterators.IterStep (Iter α) α} :
it.IsPlausibleStep step ↔ step = Iterator.step it
source
theorem Std.Rxo.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} :
it.step = ⟨step it, ⋯⟩
source
instance Std.Rxo.Iterator.instIteratorCollect {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollect (Rxo.Iterator α) Id n
Equations

- Std.Rxo.Iterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

source
instance Std.Rxo.Iterator.instIteratorCollectPartial {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollectPartial (Rxo.Iterator α) Id n
Equations

- Std.Rxo.Iterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
theorem Std.Rxo.Iterator.Monadic.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} (h : it.internalState.next = some a) (hP : a < it.internalState.upperBound) :
it.IsPlausibleOutput a
source
theorem Std.Rxo.Iterator.Monadic.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a < it.internalState.upperBound
source
theorem Std.Rxo.Iterator.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} (h : it.internalState.next = some a) (hP : a < it.internalState.upperBound) :
it.IsPlausibleOutput a
source
theorem Std.Rxo.Iterator.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a < it.internalState.upperBound
source
theorem Std.Rxo.Iterator.Monadic.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it' it : IterM Id α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ a < it.internalState.upperBound ∧ PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
source
theorem Std.Rxo.Iterator.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it' it : Iter α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ a < it.internalState.upperBound ∧ PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
source
theorem Std.Rxo.Iterator.isSome_next_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} {out : α} (h : it.IsPlausibleIndirectOutput out) :
it.internalState.next.isSome = true
source
instance Std.Rxo.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] :
Iterators.Finite (Rxo.Iterator α) Id
source
instance Std.Rxo.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] :
Iterators.Productive (Rxo.Iterator α) Id
source
instance Std.Rxo.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] :
Iterators.IteratorAccess (Rxo.Iterator α) Id
Equations

- One or more equations did not get rendered due to their size.

source
instance Std.Rxo.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] :
Iterators.LawfulDeterministicIterator (Rxo.Iterator α) Id
source
theorem Std.Rxo.Iterator.Monadic.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerable α] {it : IterM Id α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out ∧ out < it.internalState.upperBound
source
theorem Std.Rxo.Iterator.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out ∧ out < it.internalState.upperBound
source
@[inline]
instance Std.Rxo.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoop (Rxo.Iterator α) Id n

An efficient `IteratorLoop` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[irreducible, specialize #[]]
def Std.Rxo.Iterator.instIteratorLoop.loop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (wf : Iterators.IteratorLoop.WellFounded (Rxo.Iterator α) Id Pl) (upperBound least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n { s : ForInStep γ // Pl out c s }) (next : α) (hl : PRange.UpwardEnumerable.LE least next) (hu : next < upperBound) :
n γ
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Std.Rxo.Iterator.instIteratorLoopPartial {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoopPartial (Rxo.Iterator α) Id n

An efficient `IteratorLoopPartial` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[specialize #[]]
partial def Std.Rxo.Iterator.instIteratorLoopPartial.loop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (upperBound least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → out < upperBound → γ → n (ForInStep γ)) (next : α) (hl : PRange.UpwardEnumerable.LE least next) (hu : next < upperBound) :
n γ
source
@[irreducible]
theorem Std.Rxo.Iterator.instIteratorLoop.loop_eq {α : Type u} {least : α} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u} {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ} [Internal.LawfulMonadLiftBindFunction lift] {PlausibleForInStep : α → γ → ForInStep γ → Prop} {upperBound next : α} {hl : PRange.UpwardEnumerable.LE least next} {hu : next < upperBound} {f : (out : α) → PRange.UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n { s : ForInStep γ // PlausibleForInStep out c s }} {acc : γ} {wf : Iterators.IteratorLoop.WellFounded (Rxo.Iterator α) Id PlausibleForInStep} :
loop γ PlausibleForInStep wf upperBound least acc f next hl hu = do let __do_lift ← f next hl hu acc match __do_lift with | ⟨ForInStep.yield c, property⟩ => Iterators.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep wf { internalState := { next := PRange.succ? next, upperBound := upperBound } } c { internalState := { next := PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput ⋯ fun (b : α) (h : { internalState := { next := PRange.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput b) (c : γ) => f b ⋯ ⋯ c | ⟨ForInStep.done c, property⟩ => pure c
source
instance Std.Rxo.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] [LawfulMonad n] :
Iterators.LawfulIteratorLoop (Rxo.Iterator α) Id n
source
@[unbox]
structure Std.Rxi.Iterator (α : Type u) :
Type u

Internal state of the range iterators. Do not depend on its internals.

- next : Option α

Instances For

source
@[inline]
def Std.Rxi.Iterator.Monadic.step {α : Type u} [PRange.UpwardEnumerable α] (it : IterM Id α) :
Iterators.IterStep (IterM Id α) α

The pure function mapping a range iterator of type `IterM` to the next step of the iterator.

This function is prefixed with `Monadic` in order to disambiguate it from the version for iterators of type `Iter`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def Std.Rxi.Iterator.step {α : Type u} [PRange.UpwardEnumerable α] (it : Iter α) :
Iterators.IterStep (Iter α) α

The pure function mapping a range iterator of type `Iter` to the next step of the iterator.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Std.Rxi.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} :
step it = Iterators.IterStep.mapIterator Iterators.IterM.toIter (Monadic.step it.toIterM)
source
@[inline]
instance Std.Rxi.instIteratorIteratorIdOfUpwardEnumerable {α : Type u} [PRange.UpwardEnumerable α] :
Iterators.Iterator (Rxi.Iterator α) Id α
Equations

- One or more equations did not get rendered due to their size.

source
theorem Std.Rxi.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] {it : IterM Id α} {step : Iterators.IterStep (IterM Id α) α} :
it.IsPlausibleStep step ↔ step = Monadic.step it
source
theorem Std.Rxi.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] {it : IterM Id α} :
it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)
source
theorem Std.Rxi.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} {step : Iterators.IterStep (Iter α) α} :
it.IsPlausibleStep step ↔ step = Iterator.step it
source
theorem Std.Rxi.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} :
it.step = ⟨step it, ⋯⟩
source
instance Std.Rxi.Iterator.instIteratorCollect {α : Type u} [PRange.UpwardEnumerable α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollect (Rxi.Iterator α) Id n
Equations

- Std.Rxi.Iterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

source
instance Std.Rxi.Iterator.instIteratorCollectPartial {α : Type u} [PRange.UpwardEnumerable α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorCollectPartial (Rxi.Iterator α) Id n
Equations

- Std.Rxi.Iterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
theorem Std.Rxi.Iterator.Monadic.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : IterM Id α} (h : it.internalState.next = some a) :
it.IsPlausibleOutput a
source
theorem Std.Rxi.Iterator.Monadic.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : IterM Id α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a
source
theorem Std.Rxi.Iterator.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : Iter α} (h : it.internalState.next = some a) :
it.IsPlausibleOutput a
source
theorem Std.Rxi.Iterator.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : Iter α} :
it.IsPlausibleOutput a ↔ it.internalState.next = some a
source
theorem Std.Rxi.Iterator.Monadic.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] {it' it : IterM Id α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ PRange.succ? a = it'.internalState.next
source
theorem Std.Rxi.Iterator.isPlausibleSuccessorOf_iff {α : Type u} [PRange.UpwardEnumerable α] {it' it : Iter α} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ PRange.succ? a = it'.internalState.next
source
theorem Std.Rxi.Iterator.isSome_next_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} {out : α} (h : it.IsPlausibleIndirectOutput out) :
it.internalState.next.isSome = true
source
instance Std.Rxi.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] :
Iterators.Finite (Rxi.Iterator α) Id
source
instance Std.Rxi.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] :
Iterators.Productive (Rxi.Iterator α) Id
source
instance Std.Rxi.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] :
Iterators.IteratorAccess (Rxi.Iterator α) Id
Equations

- One or more equations did not get rendered due to their size.

source
instance Std.Rxi.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] :
Iterators.LawfulDeterministicIterator (Rxi.Iterator α) Id
source
theorem Std.Rxi.Iterator.Monadic.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {it : IterM Id α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out
source
theorem Std.Rxi.Iterator.isPlausibleIndirectOutput_iff {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {it : Iter α} {out : α} :
it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => PRange.succMany? n x) = some out
source
@[inline]
instance Std.Rxi.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoop (Rxi.Iterator α) Id n

An efficient `IteratorLoop` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[irreducible, specialize #[]]
def Std.Rxi.Iterator.instIteratorLoop.loop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (wf : Iterators.IteratorLoop.WellFounded (Rxi.Iterator α) Id Pl) (least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → (c : γ) → n { s : ForInStep γ // Pl out c s }) (next : α) (hl : PRange.UpwardEnumerable.LE least next) :
n γ
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Std.Rxi.Iterator.instIteratorLoopPartial {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] :
Iterators.IteratorLoopPartial (Rxi.Iterator α) Id n

An efficient `IteratorLoopPartial` instance: As long as the compiler cannot optimize away the `Option` in the internal state, we use a special loop implementation.

Equations

- One or more equations did not get rendered due to their size.

source
@[specialize #[]]
partial def Std.Rxi.Iterator.instIteratorLoopPartial.loop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (least : α) (acc : γ) (f : (out : α) → PRange.UpwardEnumerable.LE least out → γ → n (ForInStep γ)) (next : α) (hl : PRange.UpwardEnumerable.LE least next) :
n γ
source
@[irreducible]
theorem Std.Rxi.Iterator.instIteratorLoop.loop_eq {α : Type u} {least : α} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u} {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ} [Internal.LawfulMonadLiftBindFunction lift] {PlausibleForInStep : α → γ → ForInStep γ → Prop} {next : α} {hl : PRange.UpwardEnumerable.LE least next} {f : (out : α) → PRange.UpwardEnumerable.LE least out → (c : γ) → n { s : ForInStep γ // PlausibleForInStep out c s }} {acc : γ} {wf : Iterators.IteratorLoop.WellFounded (Rxi.Iterator α) Id PlausibleForInStep} :
loop γ PlausibleForInStep wf least acc f next hl = do let __do_lift ← f next hl acc match __do_lift with | ⟨ForInStep.yield c, property⟩ => Iterators.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep wf { internalState := { next := PRange.succ? next } } c { internalState := { next := PRange.succ? next } }.IsPlausibleIndirectOutput ⋯ fun (b : α) (h : { internalState := { next := PRange.succ? next } }.IsPlausibleIndirectOutput b) (c : γ) => f b ⋯ c | ⟨ForInStep.done c, property⟩ => pure c
source
instance Std.Rxi.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] [LawfulMonad n] :
Iterators.LawfulIteratorLoop (Rxi.Iterator α) Id n