structure Std.Range : Type

• start : Nat
• stop : Nat
• step : Nat
• step_pos : 0 < self.step

instance Std.instMembershipNatRange : Membership Nat Range

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

The number of elements in the range.

@[inline]

def Std.Range.forIn' {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (range : Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β

@[irreducible, specialize #[]]

def Std.Range.forIn'.loop {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (range : Range) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) (b : β) (i : Nat) (hs : (i - range.start) % range.step = 0) (hl : range.start ≤ i := by omega) : m β

instance Std.Range.instForIn'NatInferInstanceMembership {m : Type u_1 → Type u_2} : ForIn' m Range Nat inferInstance

@[inline]

def Std.Range.forM {m : Type u_1 → Type u_2} [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit

@[irreducible, specialize #[]]

def Std.Range.forM.loop {m : Type u_1 → Type u_2} [Monad m] (range : Range) (f : Nat → m PUnit) (i : Nat) : m PUnit

instance Std.Range.instForMNat {m : Type u_1 → Type u_2} : ForM m Range Nat

def Std.Range.«term[:_]» : Lean.ParserDescr

def Std.Range.«term[_:_]» : Lean.ParserDescr

def Std.Range.«term[:_:_]» : Lean.ParserDescr

def Std.Range.«term[_:_:_]» : Lean.ParserDescr

theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop

theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i

theorem Membership.mem.step {i : Nat} {r : Std.Range} (h : i ∈ r) : (i - r.start) % r.step = 0

theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : i < n