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

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 α) : 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 = IterStep.mapIterator IterM.toIter (Monadic.step it.toIterM)

@[inline]

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

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

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

Equations

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

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.

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 α) : 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 = IterStep.mapIterator IterM.toIter (Monadic.step it.toIterM)

@[inline]

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

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

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

Equations

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

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.

Equations

• Std.Rxi.Iterator.Monadic.step it = match it.internalState.next with | none => Std.IterStep.done | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next

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

Equations

• Std.Rxi.Iterator.step it = match it.internalState.next with | none => Std.IterStep.done | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next

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

@[inline]

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

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

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

Equations

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

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