structure Std.Range : Type

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

instance Std.instMembershipNatRange : Membership Nat Std.Range

Equations

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

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

The number of elements in the range.

Equations

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

@[inline]

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

Equations

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

@[irreducible, specialize #[]]

def Std.Range.forIn'.loop {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (range : Std.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 β

Equations

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

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

Equations

• Std.Range.instForIn'NatInferInstanceMembership = { forIn' := fun {β : Type ?u.14} [Monad m] => Std.Range.forIn' }

@[inline]

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

• Std.Range.forM.loop range f i = if i < range.stop then do f i have this : 0 < range.step := ⋯ Std.Range.forM.loop range f (i + range.step) else pure PUnit.unit

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

Equations

• Std.Range.instForMNat = { forM := fun [Monad m] => Std.Range.forM }

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

Equations

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

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

Equations

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

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

Equations

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

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