Range iterator

This module implements an iterator for ranges (Std.PRange).

This iterator is publicly available via PRange.iter after importing Std.Data.Iterators and it internally powers many functions on ranges such as PRange.toList.

@[unbox]

structure Std.PRange.RangeIterator (shape : BoundShape) (α : Type u) : Type u

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

• next : Option α
• upperBound : Bound shape α

@[inline]

def Std.PRange.RangeIterator.Monadic.step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] (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.PRange.RangeIterator.step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] (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.PRange.RangeIterator.step_eq_monadicStep {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : step it = Iterators.IterStep.mapIterator Iterators.IterM.toIter (Monadic.step it.toIterM)

@[inline]

instance Std.PRange.instIteratorRangeIteratorIdOfUpwardEnumerableOfSupportsUpperBound {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] : Iterators.Iterator (RangeIterator su α) Id α

Equations

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

theorem Std.PRange.RangeIterator.Monadic.isPlausibleStep_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} {step : Iterators.IterStep (IterM Id α) α} : it.IsPlausibleStep step ↔ step = Monadic.step it

theorem Std.PRange.RangeIterator.Monadic.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} : it.step = pure ⟨step it, ⋯⟩

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

theorem Std.PRange.RangeIterator.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : it.step = ⟨step it, ⋯⟩

@[inline]

instance Std.PRange.RepeatIterator.instIteratorLoop {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorLoop (RangeIterator su α) Id n

Equations

• Std.PRange.RepeatIterator.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.PRange.RepeatIterator.instIteratorLoopPartial {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorLoopPartial (RangeIterator su α) Id n

Equations

• Std.PRange.RepeatIterator.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

instance Std.PRange.RepeatIterator.instIteratorCollect {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorCollect (RangeIterator su α) Id n

Equations

• Std.PRange.RepeatIterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.PRange.RepeatIterator.instIteratorCollectPartial {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorCollectPartial (RangeIterator su α) Id n

Equations

• Std.PRange.RepeatIterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

theorem Std.PRange.RangeIterator.Monadic.isPlausibleOutput_next {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} (h : it.internalState.next = some a) (hP : SupportsUpperBound.IsSatisfied it.internalState.upperBound a) : it.IsPlausibleOutput a

theorem Std.PRange.RangeIterator.Monadic.isPlausibleOutput_iff {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a

theorem Std.PRange.RangeIterator.isPlausibleOutput_next {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} (h : it.internalState.next = some a) (hP : SupportsUpperBound.IsSatisfied it.internalState.upperBound a) : it.IsPlausibleOutput a

theorem Std.PRange.RangeIterator.isPlausibleOutput_iff {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a

theorem Std.PRange.RangeIterator.Monadic.isPlausibleSuccessorOf_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it' it : IterM Id α} : it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a ∧ UpwardEnumerable.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound

theorem Std.PRange.RangeIterator.isPlausibleSuccessorOf_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it' it : Iter α} : it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a ∧ UpwardEnumerable.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound

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

instance Std.PRange.RangeIterator.instFinite {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [HasFiniteRanges su α] : Iterators.Finite (RangeIterator su α) Id

instance Std.PRange.RangeIterator.instProductive {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] : Iterators.Productive (RangeIterator su α) Id

instance Std.PRange.RangeIterator.instIteratorAccess {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] : Iterators.IteratorAccess (RangeIterator su α) Id

Equations

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

instance Std.PRange.RangeIterator.instLawfulDeterministicIterator {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] : Iterators.LawfulDeterministicIterator (RangeIterator su α) Id