structure Std.Legacy.Range : Type

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

instance Std.Legacy.instMembershipNatRange : Membership Nat Range

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

The number of elements in the range.

@[inline]

def Std.Legacy.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 β

instance Std.Legacy.Range.instForIn'NatInferInstanceMembershipOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn' m Range Nat inferInstance

@[inline]

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

instance Std.Legacy.Range.instForMNatOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForM m Range Nat

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

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

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

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

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

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

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

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