Documentation

Init.Data.Array.Subarray

structure Subarray (α : Type u) :
Type u
def Subarray.size {α : Type u_1} (s : Subarray α) :
Equations
def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin (Subarray.size s)) :
α
Equations
@[inline]
def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) :
α
Equations
def Subarray.get! {α : Type u_1} [inst : Inhabited α] (s : Subarray α) (i : Nat) :
α
Equations
def Subarray.getOp {α : Type u_1} [inst : Inhabited α] (self : Subarray α) (idx : Nat) :
α
Equations
def Subarray.popFront {α : Type u_1} (s : Subarray α) :
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 vType w} [inst : Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
m β
Equations
@[specialize]
unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (s : Subarray α) (f : αβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
m β
Equations
@[implementedBy Subarray.forInUnsafe]
constant Subarray.forIn {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
m β
instance Subarray.instForInSubarray {m : Type u_1Type u_2} {α : Type u_3} :
ForIn m (Subarray α) α
Equations
  • Subarray.instForInSubarray = { forIn := fun {β} [Monad m] => Subarray.forIn }
@[inline]
def Subarray.foldlM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : βαm β) (init : β) (as : Subarray α) :
m β
Equations
@[inline]
def Subarray.foldrM {α : Type u} {β : Type v} {m : Type vType w} [inst : Monad m] (f : αβm β) (init : β) (as : Subarray α) :
m β
Equations
@[inline]
def Subarray.anyM {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Subarray α) :
Equations
@[inline]
def Subarray.allM {α : Type u} {m : TypeType w} [inst : Monad m] (p : αm Bool) (as : Subarray α) :
Equations
@[inline]
def Subarray.forM {α : Type u} {m : Type vType w} [inst : Monad m] (f : αm PUnit) (as : Subarray α) :
Equations
@[inline]
def Subarray.forRevM {α : Type u} {m : Type vType w} [inst : Monad m] (f : αm PUnit) (as : Subarray α) :
Equations
@[inline]
def Subarray.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Subarray α) :
β
Equations
@[inline]
def Subarray.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Subarray α) :
β
Equations
@[inline]
def Subarray.any {α : Type u} (p : αBool) (as : Subarray α) :
Equations
@[inline]
def Subarray.all {α : Type u} (p : αBool) (as : Subarray α) :
Equations
def Array.toSubarray {α : Type u} (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
Equations
def Array.ofSubarray {α : Type u} (s : Subarray α) :
Equations
def Array.extract {α : Type u} (as : Array α) (start : Nat) (stop : Nat) :
Equations
instance Array.instCoeSubarrayArray {α : Type u} :
Coe (Subarray α) (Array α)
Equations
  • Array.instCoeSubarrayArray = { coe := Array.ofSubarray }
def Subarray.toArray {α : Type u_1} (s : Subarray α) :
Equations
instance instAppendSubarray {α : Type u_1} :
Equations
instance instReprSubarray {α : Type u_1} [inst : Repr α] :
Equations
instance instToStringSubarray {α : Type u_1} [inst : ToString α] :
Equations