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

The number of elements contained in a Std.Range.

Equations

• r.numElems = 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 → r.numElems = 0

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

theorem Std.Range.mem_range'_elems {x : Nat} (r : Std.Range) (h : x ∈ List.range' r.start r.numElems 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 r.numElems r.step) ⋯) init fun (x : Subtype (Membership.mem r)) => match (motive := Subtype (Membership.mem r) → β → m (ForInStep β)) x with | ⟨a, 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 r.numElems r.step) init f