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

Equations

• Std.PRange.Internal.iter r = { internalState := { next := Std.PRange.init? r.lower, upperBound := r.upper } }

@[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 are finite and support this function.

Equations

• r.toList = (Std.PRange.Internal.iter r).toList

@[inline]

def Std.PRange.toArray {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] : Array α

Returns the elements of the given range as an array in ascending order, given that ranges of the given type and shape are finite and support this function.

Equations

• r.toArray = (Std.PRange.Internal.iter r).toArray

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.

Equations

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

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

Equations

• r.size = (Std.PRange.Internal.iter r).size

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

Equations

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