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

The number of elements contained in a Std.Range.

Equations

• Std.Range.numElems r = if r.step = 0 then if r.stop ≤ r.start then 0 else r.stop else (r.stop - r.start + r.step - 1) / r.step

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

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

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

theorem Std.Range.forIn'_eq_forIn_range' {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (r : Std.Range) (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : forIn' r init f = forIn (List.pmap Subtype.mk (List.range' r.start (Std.Range.numElems r) r.step) (_ : ∀ (x : Nat), x ∈ List.range' r.start (Std.Range.numElems r) r.step → x ∈ r)) init fun x => match (motive := { x // x ∈ r } → β → m (ForInStep β)) x with | { val := a, property := h } => f a h

theorem Std.Range.forIn_eq_forIn_range' {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (r : Std.Range) (init : β) (f : Nat → β → m (ForInStep β)) : forIn r init f = forIn (List.range' r.start (Std.Range.numElems r) r.step) init f