class Std.PRange.RangeSize (shape : BoundShape) (α : Type u) : Type u

This typeclass provides support for the PRange.size function.

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulRangeSize.

• size (upperBound : Bound shape α) (init : α) : Nat

  Returns the number of elements starting from init that satisfy the given upper bound.

class Std.PRange.LawfulRangeSize (su : BoundShape) (α : Type u) [UpwardEnumerable α] [SupportsUpperBound su α] [RangeSize su α] [LawfulUpwardEnumerable α] [HasFiniteRanges su α] : Prop

This typeclass ensures that a RangeSize instance returns the correct size for all ranges.

• size_eq_zero_of_not_satisfied (upperBound : Bound su α) (init : α) (h : ¬SupportsUpperBound.IsSatisfied upperBound init) : RangeSize.size upperBound init = 0

  If the smallest value in the range is beyond the upper bound, the size is zero.

• size_eq_one_of_succ?_eq_none (upperBound : Bound su α) (init : α) (h : SupportsUpperBound.IsSatisfied upperBound init) (h' : UpwardEnumerable.succ? init = none) : RangeSize.size upperBound init = 1

  If the smallest value in the range satisfies the upper bound and has no successor, the size is one.

• size_eq_succ_of_succ?_eq_some {a : α} (upperBound : Bound su α) (init : α) (h : SupportsUpperBound.IsSatisfied upperBound init) (h' : UpwardEnumerable.succ? init = some a) : RangeSize.size upperBound init = RangeSize.size upperBound a + 1

  If the smallest value in the range satisfies the upper bound and has a successor, the size is one larger than the size of the range starting at the successor.

@[inline]

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

Checks whether the range contains any value.

This function returns a meaningful value for all range types defined by the standard library and for all range types that satisfy the properties encoded in the LawfulUpwardEnumerable, LawfulUpwardEnumerableLowerBound and LawfulUpwardEnumerableUpperBound typeclasses.

Equations

• r.isEmpty = Option.all (fun (x : α) => !decide (Std.PRange.SupportsUpperBound.IsSatisfied r.upper x)) (Std.PRange.BoundedUpwardEnumerable.init? r.lower)

theorem Std.PRange.le_upper_of_mem {sl : BoundShape} {α : Type u_1} [LE α] [DecidableLE α] [SupportsLowerBound sl α] {a : α} {r : PRange { lower := sl, upper := BoundShape.closed } α} (h : a ∈ r) : a ≤ r.upper

theorem Std.PRange.lt_upper_of_mem {sl : BoundShape} {α : Type u_1} [LT α] [DecidableLT α] [SupportsLowerBound sl α] {a : α} {r : PRange { lower := sl, upper := BoundShape.open } α} (h : a ∈ r) : a < r.upper

theorem Std.PRange.lower_le_of_mem {su : BoundShape} {α : Type u_1} [LE α] [DecidableLE α] [SupportsUpperBound su α] {a : α} {r : PRange { lower := BoundShape.closed, upper := su } α} (h : a ∈ r) : r.lower ≤ a

theorem Std.PRange.lower_lt_of_mem {su : BoundShape} {α : Type u_1} [LT α] [DecidableLT α] [SupportsUpperBound su α] {a : α} {r : PRange { lower := BoundShape.open, upper := su } α} (h : a ∈ r) : r.lower < a

theorem Std.PRange.Internal.get_elem_helper_upper_open {sl : BoundShape} {α : Type u_1} [SupportsLowerBound sl α] [LT α] [DecidableLT α] {a n : α} {r : PRange { lower := sl, upper := BoundShape.open } α} (h₁ : a ∈ r) (h₂ : r.upper = n) : a < n