Lemmas about Std.Legacy.Range

We provide lemmas rewriting for loops over Std.Legacy.Range in terms of List.range'.

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

@[simp]

theorem Std.Legacy.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 ⋯

@[simp]

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

@[simp]

theorem Std.Legacy.Range.forM_eq_forM_range' {m : Type u_1 → Type u_2} [Monad m] (r : Range) (f : Nat → m PUnit) : forM r f = forM (List.range' r.start r.size r.step) f