structure Std.Range : Type

• start : Nat
• stop : Nat
• step : Nat

instance Std.instMembershipNatRange : Membership Nat Std.Range

@[inline]

def Std.Range.forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Std.Range) (init : β) (f : Nat → β → m (ForInStep β)) : m β

@[specialize #[]]

def Std.Range.forIn.loop {β : Type u} {m : Type u → Type v} [Monad m] (f : Nat → β → m (ForInStep β)) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.
• Std.Range.forIn.loop f 0 i stop step b = if i ≥ stop then pure b else pure b

instance Std.Range.instForInRangeNat {m : Type u_1 → Type u_2} : ForIn m Std.Range Nat

@[inline]

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

@[specialize #[]]

def Std.Range.forIn'.loop {β : Type u} {m : Type u → Type v} [Monad m] (start : Nat) (stop : Nat) (step : Nat) (f : (i : Nat) → start ≤ i ∧ i < stop → β → m (ForInStep β)) (fuel : Nat) (i : Nat) (hl : start ≤ i) (b : β) : m β

Equations

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

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

@[inline]

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

@[specialize #[]]

def Std.Range.forM.loop {m : Type u → Type v} [Monad m] (f : Nat → m PUnit) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) : m PUnit

Equations

• Std.Range.forM.loop f 0 i stop step = if i ≥ stop then pure PUnit.unit else pure PUnit.unit
• Std.Range.forM.loop f (Nat.succ fuel_2) i stop step = if i ≥ stop then pure PUnit.unit else do f i Std.Range.forM.loop f fuel_2 (i + step) stop step

instance Std.Range.instForMRangeNat {m : Type u_1 → Type u_2} : ForM m Std.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