@[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.BoundedUpwardEnumerable.init? r.lower, upperBound := r.upper } }
Instances For
instance
Std.PRange.instToStreamMkIterRangeIteratorOfUpwardEnumerableOfBoundedUpwardEnumerable
{sl su : BoundShape}
{α : Type u_1}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
:
Equations
- Std.PRange.instToStreamMkIterRangeIteratorOfUpwardEnumerableOfBoundedUpwardEnumerable = { toStream := fun (r : Std.PRange { lower := sl, upper := su } α) => Std.PRange.Internal.iter r }
@[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.
Equations
Instances For
instance
Std.PRange.instIteratorSizeRangeIteratorIdOfRangeSize
{su : BoundShape}
{α : Type u_1}
[RangeSize su α]
[UpwardEnumerable α]
[SupportsUpperBound su α]
:
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]
:
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
Instances For
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 : α}
:
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)
:
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.