@[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 α) : 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.

@[inline]

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

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

theorem Std.Rxc.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} : step it = IterStep.mapIterator IterM.toIter (Monadic.step it.toIterM)

@[implicit_reducible, inline]

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

theorem Std.Rxc.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : IterM Id α} {step : 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 α} : Std.Iterator.step it = pure (Shrink.deflate ⟨step it, ⋯⟩)

theorem Std.Rxc.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] {it : Iter α} {step : 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, ⋯⟩

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

@[implicit_reducible]

instance Std.Rxc.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] : IteratorAccess (Rxc.Iterator α) Id

instance Std.Rxc.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] : 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

@[implicit_reducible, inline]

instance Std.Rxc.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] : 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.

@[inline]

def Std.Rxc.Iterator.instIteratorLoop.loop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next) (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ

instance Std.Rxc.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : 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 α) : 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.

@[inline]

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

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

theorem Std.Rxo.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} : step it = IterStep.mapIterator IterM.toIter (Monadic.step it.toIterM)

@[implicit_reducible, inline]

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

theorem Std.Rxo.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : IterM Id α} {step : 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 α} : Std.Iterator.step it = pure (Shrink.deflate ⟨step it, ⋯⟩)

theorem Std.Rxo.Iterator.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] {it : Iter α} {step : 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, ⋯⟩

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

@[implicit_reducible]

instance Std.Rxo.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] : IteratorAccess (Rxo.Iterator α) Id

instance Std.Rxo.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] : 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

@[implicit_reducible, inline]

instance Std.Rxo.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] : 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.

@[inline]

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) (LargeEnough : α → Prop) (hl : ∀ (a b : α), PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next) (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ

instance Std.Rxo.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : 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 α) : 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.

@[inline]

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

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

theorem Std.Rxi.Iterator.step_eq_monadicStep {α : Type u} [PRange.UpwardEnumerable α] {it : Iter α} : step it = IterStep.mapIterator IterM.toIter (Monadic.step it.toIterM)

@[implicit_reducible, inline]

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

theorem Std.Rxi.Iterator.Monadic.isPlausibleStep_iff {α : Type u} [PRange.UpwardEnumerable α] {it : IterM Id α} {step : 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 : 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, ⋯⟩

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

@[implicit_reducible]

instance Std.Rxi.Iterator.instIteratorAccess {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] : IteratorAccess (Rxi.Iterator α) Id

instance Std.Rxi.Iterator.instLawfulDeterministicIterator {α : Type u} [PRange.UpwardEnumerable α] : 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

@[implicit_reducible, inline]

instance Std.Rxi.Iterator.instIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] : 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.

@[inline]

def Std.Rxi.Iterator.instIteratorLoop.loop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ (a b : α), PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α) (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))) : n γ

instance Std.Rxi.Iterator.instLawfulIteratorLoop {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : LawfulIteratorLoop (Rxi.Iterator α) Id n