@[unbox]

structure Std.Rxc.Iterator (α : Type u) : Type u

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

• next : Option α
• upperBound : α

@[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.

@[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.

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)

@[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.

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

theorem Std.Rxc.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} : it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)

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

theorem Std.Rxc.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} : it.step = ⟨step it, ⋯⟩

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

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

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

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

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

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

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

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

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

instance Std.Rxc.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] : Iterators.Finite (Rxc.Iterator α) Id

instance Std.Rxc.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] : Iterators.Productive (Rxc.Iterator α) Id

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.

instance Std.Rxc.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] : Iterators.LawfulDeterministicIterator (Rxc.Iterator α) Id

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

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

@[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.

@[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.

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.

@[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 γ

@[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

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

@[unbox]

structure Std.Rxo.Iterator (α : Type u) : Type u

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

• next : Option α
• upperBound : α

@[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.

@[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.

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)

@[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.

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

theorem Std.Rxo.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} : it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)

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

theorem Std.Rxo.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} : it.step = ⟨step it, ⋯⟩

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

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

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

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

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

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

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

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

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

instance Std.Rxo.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] : Iterators.Finite (Rxo.Iterator α) Id

instance Std.Rxo.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] : Iterators.Productive (Rxo.Iterator α) Id

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.

instance Std.Rxo.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] : Iterators.LawfulDeterministicIterator (Rxo.Iterator α) Id

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

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

@[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.

@[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.

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.

@[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 γ

@[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

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

@[unbox]

structure Std.Rxi.Iterator (α : Type u) : Type u

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

• next : Option α

@[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.

@[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.

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)

@[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.

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

theorem Std.Rxi.Iterator.Monadic.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] {it : IterM Id α} : it.step = pure (Shrink.deflate ⟨step it, ⋯⟩)

theorem Std.Rxi.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} {step : Iterators.IterStep (Iter α) α} : it.IsPlausibleStep step ↔ step = Iterator.step it

theorem Std.Rxi.Iterator.step_eq_step {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} : it.step = ⟨step it, ⋯⟩

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

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

theorem Std.Rxi.Iterator.Monadic.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : IterM Id α} (h : it.internalState.next = some a) : it.IsPlausibleOutput a

theorem Std.Rxi.Iterator.Monadic.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : IterM Id α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a

theorem Std.Rxi.Iterator.isPlausibleOutput_next {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : Iter α} (h : it.internalState.next = some a) : it.IsPlausibleOutput a

theorem Std.Rxi.Iterator.isPlausibleOutput_iff {α : Type u} {a : α} [PRange.UpwardEnumerable α] {it : Iter α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a

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

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

theorem Std.Rxi.Iterator.isSome_next_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} {out : α} (h : it.IsPlausibleIndirectOutput out) : it.internalState.next.isSome = true

instance Std.Rxi.Iterator.instFinite {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [IsAlwaysFinite α] : Iterators.Finite (Rxi.Iterator α) Id

instance Std.Rxi.Iterator.instProductive {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] : Iterators.Productive (Rxi.Iterator α) Id

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.

instance Std.Rxi.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] : Iterators.LawfulDeterministicIterator (Rxi.Iterator α) Id

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

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

@[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.

@[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.

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.

@[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 γ

@[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

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