structure Std.Legacy.Range : Type

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

@[instance_reducible]

instance Std.Legacy.instMembershipNatRange : Membership Nat Range

Equations

• Std.Legacy.instMembershipNatRange = { mem := fun (r : Std.Legacy.Range) (i : Nat) => r.start ≤ i ∧ i < r.stop ∧ (i - r.start) % r.step = 0 }

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

The number of elements in the range.

Equations

• r.size = (r.stop - r.start + r.step - 1) / r.step

@[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 β

Equations

• range.forIn' init f = Std.Legacy.Range.forIn'.loop✝ range f init range.start ⋯ ⋯

@[instance_reducible]

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

Equations

• Std.Legacy.Range.instForIn'NatInferInstanceMembershipOfMonad = { forIn' := fun {β : Type ?u.2} => Std.Legacy.Range.forIn' }

@[inline]

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

Equations

• range.forM f = Std.Legacy.Range.forM.loop✝ range f range.start

@[instance_reducible]

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

Equations

• Std.Legacy.Range.instForMNatOfMonad = { forM := Std.Legacy.Range.forM }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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