Documentation

Batteries.Data.Range.Lemmas

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
Instances For
    theorem Std.Range.numElems_stop_le_start (r : Std.Range) :
    r.stop r.startr.numElems = 0
    theorem Std.Range.numElems_step_1 (start : Nat) (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