@[inline]

def Std.PRange.Internal.iter {sl su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] (r : PRange { lower := sl, upper := su } α) : Iter α

Internal function that constructs an iterator for a PRange. This is an internal function. Use PRange.iter instead, which requires importing Std.Data.Iterators.

instance Std.PRange.instToStreamMkIterRangeIteratorOfUpwardEnumerableOfBoundedUpwardEnumerable {sl su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] : ToStream (PRange { lower := sl, upper := su } α) (Iter α)

@[inline]

def Std.PRange.toList {sl su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] [SupportsUpperBound su α] (r : PRange { lower := sl, upper := su } α) [Iterators.Iterator (RangeIterator su α) Id α] [Iterators.Finite (RangeIterator su α) Id] [Iterators.IteratorCollect (RangeIterator su α) Id Id] : List α

Returns the elements of the given range as a list in ascending order, given that ranges of the given type and shape support this function and the range is finite.

instance Std.PRange.instIteratorSizeRangeIteratorIdOfRangeSize {su : BoundShape} {α : Type u_1} [RangeSize su α] [UpwardEnumerable α] [SupportsUpperBound su α] : Iterators.IteratorSize (RangeIterator su α) Id

Iterators for ranges implementing RangeSize support the size function.

@[inline]

def Std.PRange.size {sl su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] [SupportsUpperBound su α] (r : PRange { lower := sl, upper := su } α) [Iterators.IteratorSize (RangeIterator su α) Id] : Nat

Returns the number of elements contained in the given range, given that ranges of the given type and shape support this function.

theorem Std.PRange.RangeIterator.isPlausibleIndirectOutput_iff {su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {it : Iter α} {out : α} : it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => UpwardEnumerable.succMany? n x) = some out ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound out

theorem Std.PRange.Internal.isPlausibleIndirectOutput_iter_iff {sl su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] [SupportsLowerBound sl α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] [LawfulUpwardEnumerableLowerBound sl α] {r : PRange { lower := sl, upper := su } α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

theorem Std.PRange.RangeIterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {it : Iter α} {out : α} (hout : it.IsPlausibleIndirectOutput out) : ∃ (a : α), it.internalState.next = some a ∧ UpwardEnumerable.LE a out

instance Std.PRange.instForIn'MkInferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLowerBoundOfLawfulUpwardEnumerableUpperBoundOfMonadOfFiniteRangeIteratorId {sl su : BoundShape} {α : Type u_1} {m : Type u_1 → Type u_2} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] [SupportsLowerBound sl α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α] [Monad m] [Iterators.Finite (RangeIterator su α) Id] : ForIn' m (PRange { lower := sl, upper := su } α) α inferInstance