Documentation

Std.Data.Range.Lemmas

The number of elements contained in a Std.Range.

Equations
Instances For
    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.stepx r)) init fun (x : { x : Nat // x r }) => match (motive := { x : Nat // 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