@[deprecated Std.Range.size (since := "2024-12-19")]

def Std.Range.numElems (r : Range) : Nat

Alias of Std.Range.size.

---

The number of elements in the range.

Equations

• Std.Range.numElems = Std.Range.size

theorem Std.Range.size_stop_le_start (r : Range) : r.stop ≤ r.start → r.size = 0

@[deprecated Std.Range.size_stop_le_start (since := "2024-12-19")]

theorem Std.Range.numElems_stop_le_start (r : Range) : r.stop ≤ r.start → r.size = 0

Alias of Std.Range.size_stop_le_start.

theorem Std.Range.size_step_1 (start stop : Nat) : { start := start, stop := stop, step := 1, step_pos := ⋯ }.size = stop - start

@[deprecated Std.Range.size_step_1 (since := "2024-12-19")]

theorem Std.Range.numElems_step_1 (start stop : Nat) : { start := start, stop := stop, step := 1, step_pos := ⋯ }.size = stop - start

Alias of Std.Range.size_step_1.

@[deprecated Std.Range.mem_of_mem_range' (since := "2024-12-19")]

theorem Std.Range.mem_range'_elems {x : Nat} {r : Range} (h : x ∈ List.range' r.start r.size r.step) : x ∈ r

Alias of Std.Range.mem_of_mem_range'.

@[deprecated Std.Range.forIn'_eq_forIn'_range' (since := "2024-12-19")]

theorem Std.Range.forIn'_eq_forIn_range' {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (r : Range) (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : forIn' r init f = forIn' (List.range' r.start r.size r.step) init fun (a : Nat) (h : a ∈ List.range' r.start r.size r.step) => f a ⋯

Alias of Std.Range.forIn'_eq_forIn'_range'.