@[inline]

def Std.Rcc.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Rcc α) : Iter α

Internal function that constructs an iterator for a closed range lo...=hi. This is an internal function. Use Rcc.iter instead, which requires importing Std.Data.Iterators.

Equations

• Std.Rcc.Internal.iter r = { internalState := { next := some r.lower, upperBound := r.upper } }

@[inline]

def Std.Rcc.toList {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Rcc α) : List α

Returns the elements of the given closed range as a list in ascending order.

Equations

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

@[inline]

def Std.Rcc.toArray {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Rcc α) : Array α

Returns the elements of the given closed range as an array in ascending order.

Equations

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

@[inline]

def Std.Rcc.size {α : Type u} [Rxc.HasSize α] (r : Rcc α) : Nat

Returns the number of elements contained in the given closed range.

Equations

• r.size = Std.Rxc.HasSize.size r.lower r.upper

theorem Std.Rcc.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {r : Rcc α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

theorem Std.Rxc.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter α} {out : α} (hout : it.IsPlausibleIndirectOutput out) : ∃ (a : α), it.internalState.next = some a ∧ PRange.UpwardEnumerable.LE a out

instance Std.Rcc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Monad m] [Iterators.Finite (Rxc.Iterator α) Id] : ForIn' m (Rcc α) α inferInstance

Equations

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

@[inline]

def Std.Rco.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Rco α) : Iter α

Internal function that constructs an iterator for a closed range lo...hi. This is an internal function. Use Rco.iter instead, which requires importing Std.Data.Iterators.

Equations

• Std.Rco.Internal.iter r = { internalState := { next := some r.lower, upperBound := r.upper } }

@[inline]

def Std.Rco.toList {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Rco α) : List α

Returns the elements of the given left-closed right-open range as a list in ascending order.

Equations

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

@[inline]

def Std.Rco.toArray {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Rco α) : Array α

Returns the elements of the given left-closed right-open range as an array in ascending order.

Equations

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

@[inline]

def Std.Rco.size {α : Type u} [Rxo.HasSize α] (r : Rco α) : Nat

Returns the number of elements contained in the given left-closed right-open range.

Equations

• r.size = Std.Rxo.HasSize.size r.lower r.upper

theorem Std.Rco.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLE α] {r : Rco α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

theorem Std.Rxo.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter α} {out : α} (hout : it.IsPlausibleIndirectOutput out) : ∃ (a : α), it.internalState.next = some a ∧ PRange.UpwardEnumerable.LE a out

instance Std.Rco.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LE α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] [Monad m] [Iterators.Finite (Rxo.Iterator α) Id] : ForIn' m (Rco α) α inferInstance

Equations

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

@[inline]

def Std.Rci.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Rci α) : Iter α

Internal function that constructs an iterator for a closed range lo...*. This is an internal function. Use Rcc.iter instead, which requires importing Std.Data.Iterators.

Equations

• Std.Rci.Internal.iter r = { internalState := { next := some r.lower } }

@[inline]

def Std.Rci.toList {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Rci α) : List α

Returns the elements of the given left-closed right-unbounded range as a list in ascending order.

Equations

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

@[inline]

def Std.Rci.toArray {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Rci α) : Array α

Returns the elements of the given left-closed right-unbounded range as an array in ascending order.

Equations

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

@[inline]

def Std.Rci.size {α : Type u} [Rxi.HasSize α] (r : Rci α) : Nat

Returns the number of elements contained in the given left-closed right-unbounded range.

Equations

• r.size = Std.Rxi.HasSize.size r.lower

theorem Std.Rci.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {r : Rci α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

theorem Std.Rxi.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] {it : Iter α} {out : α} (hout : it.IsPlausibleIndirectOutput out) : ∃ (a : α), it.internalState.next = some a ∧ PRange.UpwardEnumerable.LE a out

instance Std.Rci.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Monad m] [Iterators.Finite (Rxi.Iterator α) Id] : ForIn' m (Rci α) α inferInstance

Equations

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

@[inline]

def Std.Roc.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Roc α) : Iter α

Internal function that constructs an iterator for a left-open right-closed range lo<...=hi. This is an internal function. Use Roc.iter instead, which requires importing Std.Data.Iterators.

Equations

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

@[inline]

def Std.Roc.toList {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Roc α) : List α

Returns the elements of the given left-open right-closed range as a list in ascending order.

Equations

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

@[inline]

def Std.Roc.toArray {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Roc α) : Array α

Returns the elements of the given left-open right-closed range as an array in ascending order.

Equations

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

@[inline]

def Std.Roc.size {α : Type u} [Rxc.HasSize α] [PRange.UpwardEnumerable α] (r : Roc α) : Nat

Returns the number of elements contained in the given left-open right-closed range.

Equations

• r.size = match Std.PRange.succ? r.lower with | none => 0 | some lower => Std.Rxc.HasSize.size lower r.upper

theorem Std.Roc.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [LT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {r : Roc α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Roc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [LT α] [PRange.LawfulUpwardEnumerableLT α] [Monad m] [Iterators.Finite (Rxc.Iterator α) Id] : ForIn' m (Roc α) α inferInstance

Equations

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

@[inline]

def Std.Roo.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Roo α) : Iter α

Internal function that constructs an iterator for an open range lo<...hi. This is an internal function. Use Roo.iter instead, which requires importing Std.Data.Iterators.

Equations

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

@[inline]

def Std.Roo.toList {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Roo α) : List α

Returns the elements of the given open range as a list in ascending order.

Equations

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

@[inline]

def Std.Roo.toArray {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Roo α) : Array α

Returns the elements of the given open range as an array in ascending order.

Equations

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

@[inline]

def Std.Roo.size {α : Type u} [Rxo.HasSize α] [PRange.UpwardEnumerable α] (r : Roo α) : Nat

Returns the number of elements contained in the given open range.

Equations

• r.size = match Std.PRange.succ? r.lower with | none => 0 | some lower => Std.Rxo.HasSize.size lower r.upper

theorem Std.Roo.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLT α] {r : Roo α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Roo.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Monad m] [Iterators.Finite (Rxo.Iterator α) Id] : ForIn' m (Roo α) α inferInstance

Equations

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

@[inline]

def Std.Roi.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] (r : Roi α) : Iter α

Internal function that constructs an iterator for a closed range lo<...*. This is an internal function. Use Roi.iter instead, which requires importing Std.Data.Iterators.

Equations

• Std.Roi.Internal.iter r = { internalState := { next := Std.PRange.succ? r.lower } }

@[inline]

def Std.Roi.toList {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Roi α) : List α

Returns the elements of the given left-open right-unbounded range as a list in ascending order.

Equations

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

@[inline]

def Std.Roi.toArray {α : Type u} [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Roi α) : Array α

Returns the elements of the given left-open right-unbounded range as an array in ascending order.

Equations

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

@[inline]

def Std.Roi.size {α : Type u} [Rxi.HasSize α] [PRange.UpwardEnumerable α] (r : Roi α) : Nat

Returns the number of elements contained in the given left-open right-unbounded range.

Equations

• r.size = match Std.PRange.succ? r.lower with | none => 0 | some lower => Std.Rxi.HasSize.size lower

theorem Std.Roi.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {r : Roi α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Roi.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LT α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [Monad m] [Iterators.Finite (Rxi.Iterator α) Id] : ForIn' m (Roi α) α inferInstance

Equations

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

@[inline]

def Std.Ric.Internal.iter {α : Type u} [PRange.Least? α] (r : Ric α) : Iter α

Internal function that constructs an iterator for a left-unbounded right-closed range *...=hi. This is an internal function. Use Ric.iter instead, which requires importing Std.Data.Iterators.

Equations

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

@[inline]

def Std.Ric.toList {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Ric α) : List α

Returns the elements of the given closed range as a list in ascending order.

Equations

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

@[inline]

def Std.Ric.toArray {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] (r : Ric α) : Array α

Returns the elements of the given closed range as an array in ascending order.

Equations

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

@[inline]

def Std.Ric.size {α : Type u} [Rxc.HasSize α] [PRange.Least? α] (r : Ric α) : Nat

Returns the number of elements contained in the given closed range.

Equations

• r.size = match Std.PRange.least? with | none => 0 | some least => Std.Rxc.HasSize.size least r.upper

theorem Std.Ric.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] [LE α] [DecidableLE α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] {r : Ric α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Ric.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [PRange.Least? α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Iterators.Finite (Rxc.Iterator α) Id] : ForIn' m (Ric α) α inferInstance

Equations

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

@[inline]

def Std.Rio.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] (r : Rio α) : Iter α

Internal function that constructs an iterator for a left-unbounded right-open range *...hi. This is an internal function. Use Rio.iter instead, which requires importing Std.Data.Iterators.

Equations

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

@[inline]

def Std.Rio.toList {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Rio α) : List α

Returns the elements of the given closed range as a list in ascending order.

Equations

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

@[inline]

def Std.Rio.toArray {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] (r : Rio α) : Array α

Returns the elements of the given closed range as an array in ascending order.

Equations

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

@[inline]

def Std.Rio.size {α : Type u} [Rxo.HasSize α] [PRange.Least? α] (r : Rio α) : Nat

Returns the number of elements contained in the given closed range.

Equations

• r.size = match Std.PRange.least? with | none => 0 | some least => Std.Rxo.HasSize.size least r.upper

theorem Std.Rio.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.Least? α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] {r : Rio α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Rio.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [PRange.Least? α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] [PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Iterators.Finite (Rxo.Iterator α) Id] : ForIn' m (Rio α) α inferInstance

Equations

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

@[inline]

def Std.Rii.Internal.iter {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] : Rii α → Iter α

Internal function that constructs an iterator for the full range *...*. This is an internal function. Use Rio.iter instead, which requires importing Std.Data.Iterators.

Equations

• Std.Rii.Internal.iter x✝ = { internalState := { next := Std.PRange.least? } }

@[inline]

def Std.Rii.toList {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] (r : Rii α) [Iterators.Iterator (Rxi.Iterator α) Id α] [Iterators.Finite (Rxi.Iterator α) Id] [Iterators.IteratorCollect (Rxi.Iterator α) Id Id] : List α

Returns the elements of the given full range as a list in ascending order.

Equations

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

@[inline]

def Std.Rii.toArray {α : Type u_1} [PRange.UpwardEnumerable α] [PRange.Least? α] (r : Rii α) [Iterators.Iterator (Rxi.Iterator α) Id α] [Iterators.Finite (Rxi.Iterator α) Id] [Iterators.IteratorCollect (Rxi.Iterator α) Id Id] : Array α

Returns the elements of the given full range as an array in ascending order.

Equations

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

@[inline]

def Std.Rii.size {α : Type u} : Rii α → [PRange.Least? α] → [Rxi.HasSize α] → Nat

Returns the number of elements contained in the full range.

Equations

• x✝.size = match Std.PRange.least? with | none => 0 | some least => Std.Rxi.HasSize.size least

theorem Std.Rii.Internal.isPlausibleIndirectOutput_iter_iff {α : Type u} [PRange.UpwardEnumerable α] [PRange.Least? α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {r : Rii α} {a : α} : (iter r).IsPlausibleIndirectOutput a ↔ a ∈ r

instance Std.Rii.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId {α : Type u} {m : Type u → Type u_1} [PRange.UpwardEnumerable α] [PRange.Least? α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Iterators.Finite (Rxi.Iterator α) Id] : ForIn' m (Rii α) α inferInstance

Equations

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