Documentation

Init.Data.Range

structure Std.Range :

Type

start : Nat
stop : Nat
step : Nat

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

Std.Range.forIn range init f = (fun loop => loop range.stop range.start range.stop range.step init) (Std.Range.forIn.loop f)

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

Std.Range.forIn.loop f 0 i stop step b = if i ≥ stop then pure b else pure b
Std.Range.forIn.loop f (Nat.succ fuel_2) i stop step b = if i ≥ stop then pure b else do let a ← f i b match a with | ForInStep.done b => pure b | ForInStep.yield b => Std.Range.forIn.loop f fuel_2 (i + step) stop step b

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 }

@[inline]

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

Equations

Std.Range.forM range f = (fun loop => loop range.stop range.start range.stop range.step) (Std.Range.forM.loop f)

@[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) :

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

Equations

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

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

Lean.ParserDescr

Equations

Std.Range.«term[:_]» = Lean.ParserDescr.node `Std.Range.«term[:_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))

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

Lean.ParserDescr

Equations

Std.Range.«term[_:_]» = Lean.ParserDescr.node `Std.Range.«term[_:_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))

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

Lean.ParserDescr

Equations

Std.Range.«term[:_:_]» = Lean.ParserDescr.node `Std.Range.«term[:_:_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))

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

Lean.ParserDescr

Equations

Std.Range.«term[_:_:_]» = Lean.ParserDescr.node `Std.Range.«term[_:_:_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))