Documentation

Init.Data.Range

source
structure Std.Range:
Type
source
instance Std.instMembershipNatRange:
Membership Nat Std.Range
Equations
source
@[inline]
def Std.Range.forIn {β : Type u} {m : Type u → Type v} [inst : Monad m] (range : Std.Range) (init : β) (f : Nat → β → m (ForInStep β)) :
m β
Equations
source
@[specialize]
def Std.Range.forIn.loop {β : Type u} {m : Type u → Type v} [inst : Monad m] (f : Nat → β → m (ForInStep β)) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) (b : β) :
m β
Equations
source
instance Std.Range.instForInRangeNat {m : Type u_1 → Type u_2} :
ForIn m Std.Range Nat
Equations
  • Std.Range.instForInRangeNat = { forIn := fun {β} [Monad m] => Std.Range.forIn }
source
@[inline]
def Std.Range.forIn' {β : Type u} {m : Type u → Type v} [inst : Monad m] (range : Std.Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) :
m β
Equations
source
@[specialize]
def Std.Range.forIn'.loop {β : Type u} {m : Type u → Type v} [inst : 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.
source
instance Std.Range.instForIn'RangeNatInferInstanceMembershipInstMembershipNatRange {m : Type u_1 → Type u_2} :
ForIn' m Std.Range Nat inferInstance
Equations
  • Std.Range.instForIn'RangeNatInferInstanceMembershipInstMembershipNatRange = { forIn' := fun {β} [Monad m] => Std.Range.forIn' }
source
@[inline]
def Std.Range.forM {m : Type u → Type v} [inst : Monad m] (range : Std.Range) (f : Nat → m PUnit) :
m PUnit
Equations
source
@[specialize]
def Std.Range.forM.loop {m : Type u → Type v} [inst : Monad m] (f : Nat → m PUnit) (fuel : Nat) (i : Nat) (stop : Nat) (step : Nat) :
m PUnit
Equations
source
instance Std.Range.instForMRangeNat {m : Type u_1 → Type u_2} :
ForM m Std.Range Nat
Equations
  • Std.Range.instForMRangeNat = { forM := fun [Monad m] => Std.Range.forM }
source
def Std.Range.«term[:_]»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Std.Range.«term[_:_]»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Std.Range.«term[:_:_]»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Std.Range.«term[_:_:_]»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) :
i < r.stop
source
theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) :
r.start ≤ i