Equations
- Std.instMembershipNatRange = { mem := fun i r => r.start ≤ i ∧ i < r.stop }
@[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 = Std.Range.forIn.loop f range.stop range.start range.stop range.step init
@[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
@[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
- Std.Range.forIn' range init f = Std.Range.forIn'.loop range.start range.stop range.step f range.stop range.start (_ : range.start ≤ range.start) init
@[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
- Std.Range.forIn'.loop start stop step f 0 i hl b = if hu : i < stop then pure b else pure b
- Std.Range.forIn'.loop start stop step f (Nat.succ fuel_2) i hl b = if hu : i < stop then do let a ← f i (_ : start ≤ i ∧ i < stop) b match a with | ForInStep.done b => pure b | ForInStep.yield b => Std.Range.forIn'.loop start stop step f fuel_2 (i + step) (_ : start ≤ i + step) b else pure b
@[inline]
def
Std.Range.forM
{m : Type u → Type v}
[inst : Monad m]
(range : Std.Range)
(f : Nat → m PUnit)
:
m PUnit
Equations
- Std.Range.forM range f = Std.Range.forM.loop f range.stop range.start range.stop range.step
@[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
- 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
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 "]"))
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 "]"))
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 "]"))
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 "]"))