Documentation

Init.Data.Range.Polymorphic.RangeIterator

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.

source
@[unbox]
structure Std.PRange.RangeIterator (shape : BoundShape) (α : Type u) :
Type u

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

Instances For
    source
    @[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
      Instances For
        source
        @[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
          Instances For
            source
            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)
            source
            @[inline]
            instance Std.PRange.instIteratorRangeIteratorIdOfUpwardEnumerableOfSupportsUpperBound {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] :
            Iterators.Iterator (RangeIterator su α) Id α
            Equations
              source
              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
              source
              theorem Std.PRange.RangeIterator.Monadic.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} :
              it.step = pure ⟨step it, ⋯⟩
              source
              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
              source
              theorem Std.PRange.RangeIterator.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} :
              it.step = ⟨step it, ⋯⟩
              source
              @[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
                source
                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
                  source
                  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
                    source
                    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
                      source
                      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
                      source
                      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
                      source
                      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
                      source
                      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
                      source
                      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
                      source
                      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
                      source
                      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
                      source
                      instance Std.PRange.RangeIterator.instFinite {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [HasFiniteRanges su α] :
                      Iterators.Finite (RangeIterator su α) Id
                      source
                      instance Std.PRange.RangeIterator.instProductive {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] :
                      Iterators.Productive (RangeIterator su α) Id
                      source
                      instance Std.PRange.RangeIterator.instIteratorAccess {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] :
                      Iterators.IteratorAccess (RangeIterator su α) Id
                      Equations
                        source
                        instance Std.PRange.RangeIterator.instLawfulDeterministicIterator {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] :
                        Iterators.LawfulDeterministicIterator (RangeIterator su α) Id