Equations
- Subarray.popFront s = if h : s.start < s.stop then { as := s.as, start := s.start + 1, stop := s.stop, h₁ := (_ : s.start + 1 ≤ s.stop), h₂ := (_ : s.stop ≤ Array.size s.as) } else s
@[inline]
unsafe def
Subarray.forInUnsafe
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(s : Subarray α)
(b : β)
(f : α → β → m (ForInStep β))
:
m β
Equations
- Subarray.forInUnsafe s b f = let sz := USize.ofNat s.stop; (fun loop => loop (USize.ofNat s.start) b) (Subarray.forInUnsafe.loop s f sz)
@[specialize]
unsafe def
Subarray.forInUnsafe.loop
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(s : Subarray α)
(f : α → β → m (ForInStep β))
(sz : USize)
(i : USize)
(b : β)
:
m β
Equations
- Subarray.forInUnsafe.loop s f sz i b = if i < sz then let a := Array.uget s.as i (_ : USize.toNat i < Array.size s.as); do let a ← f a b match a with | ForInStep.done b => pure b | ForInStep.yield b => Subarray.forInUnsafe.loop s f sz (i + 1) b else pure b
@[implementedBy Subarray.forInUnsafe]
constant
Subarray.forIn
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(s : Subarray α)
(b : β)
(f : α → β → m (ForInStep β))
:
m β
@[inline]
def
Subarray.foldlM
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(f : β → α → m β)
(init : β)
(as : Subarray α)
:
m β
Equations
- Subarray.foldlM f init as = Array.foldlM f init as.as as.start as.stop
@[inline]
def
Subarray.foldrM
{α : Type u}
{β : Type v}
{m : Type v → Type w}
[inst : Monad m]
(f : α → β → m β)
(init : β)
(as : Subarray α)
:
m β
Equations
- Subarray.foldrM f init as = Array.foldrM f init as.as as.stop as.start
@[inline]
def
Subarray.anyM
{α : Type u}
{m : Type → Type w}
[inst : Monad m]
(p : α → m Bool)
(as : Subarray α)
:
m Bool
Equations
- Subarray.anyM p as = Array.anyM p as.as as.start as.stop
@[inline]
def
Subarray.allM
{α : Type u}
{m : Type → Type w}
[inst : Monad m]
(p : α → m Bool)
(as : Subarray α)
:
m Bool
Equations
- Subarray.allM p as = Array.allM p as.as as.start as.stop
@[inline]
def
Subarray.forM
{α : Type u}
{m : Type v → Type w}
[inst : Monad m]
(f : α → m PUnit)
(as : Subarray α)
:
m PUnit
Equations
- Subarray.forM f as = Array.forM f as.as as.start as.stop
@[inline]
def
Subarray.forRevM
{α : Type u}
{m : Type v → Type w}
[inst : Monad m]
(f : α → m PUnit)
(as : Subarray α)
:
m PUnit
Equations
- Subarray.forRevM f as = Array.forRevM f as.as as.stop as.start
@[inline]
Equations
- Subarray.foldl f init as = Id.run (Subarray.foldlM f init as)
@[inline]
Equations
- Subarray.foldr f init as = Id.run (Subarray.foldrM f init as)
@[inline]
Equations
- Subarray.any p as = Id.run (Subarray.anyM p as)
@[inline]
Equations
- Subarray.all p as = Id.run (Subarray.allM p as)
def
Array.toSubarray
{α : Type u}
(as : Array α)
(start : optParam Nat 0)
(stop : optParam Nat (Array.size as))
:
Subarray α
Equations
- Array.toSubarray as start stop = if h₂ : stop ≤ Array.size as then if h₁ : start ≤ stop then { as := as, start := start, stop := stop, h₁ := h₁, h₂ := h₂ } else { as := as, start := stop, stop := stop, h₁ := (_ : stop ≤ stop), h₂ := h₂ } else if h₁ : start ≤ Array.size as then { as := as, start := start, stop := Array.size as, h₁ := h₁, h₂ := (_ : Array.size as ≤ Array.size as) } else { as := as, start := Array.size as, stop := Array.size as, h₁ := (_ : Array.size as ≤ Array.size as), h₂ := (_ : Array.size as ≤ Array.size as) }
Equations
- Array.ofSubarray s = Id.run (let as := Array.mkEmpty (s.stop - s.start); do let r ← forIn s as fun a r => let as := r; let as := Array.push as a; do pure PUnit.unit pure (ForInStep.yield as) let x : Array α := r let as : Array α := x pure as)
Equations
- Array.extract as start stop = Array.ofSubarray (Array.toSubarray as start stop)
Equations
- Array.«term__[_:_]» = Lean.ParserDescr.trailingNode `Array.«term__[_:_]» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "[")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))
Equations
- Array.«term__[_:]» = Lean.ParserDescr.trailingNode `Array.«term__[_:]» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "[")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.symbol "]"))
Equations
- Array.«term__[:_]» = Lean.ParserDescr.trailingNode `Array.«term__[:_]» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "[")) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))
Equations
Equations
- instAppendSubarray = { append := fun x y => let a := Subarray.toArray x ++ Subarray.toArray y; Array.toSubarray a 0 (Array.size a) }
Equations
- instReprSubarray = { reprPrec := fun s x => repr (Subarray.toArray s) ++ Std.Format.text ".toSubarray" }
Equations
- instToStringSubarray = { toString := fun s => toString (Subarray.toArray s) }