# Documentation

## Init.Data.Array.Subarray

structure Subarray (α : Type u) :
• array :
• start : Nat
• stop : Nat
• start_le_stop : self.start self.stop
• stop_le_array_size : self.stop self.array.size
Instances For
theorem Subarray.start_le_stop {α : Type u} (self : ) :
self.start self.stop
theorem Subarray.stop_le_array_size {α : Type u} (self : ) :
self.stop self.array.size
@[reducible, inline, deprecated Subarray.array]
abbrev Subarray.as {α : Type u_1} (s : ) :
Equations
• s.as = s.array
Instances For
@[deprecated Subarray.start_le_stop]
theorem Subarray.h₁ {α : Type u_1} (s : ) :
s.start s.stop
@[deprecated Subarray.stop_le_array_size]
theorem Subarray.h₂ {α : Type u_1} (s : ) :
s.stop s.array.size
def Subarray.size {α : Type u_1} (s : ) :
Equations
• s.size = s.stop - s.start
Instances For
theorem Subarray.size_le_array_size {α : Type u_1} {s : } :
s.size s.array.size
def Subarray.get {α : Type u_1} (s : ) (i : Fin s.size) :
α
Equations
• s.get i = s.array[s.start + i]
Instances For
instance Subarray.instGetElemNatLtSize {α : Type u_1} :
GetElem (Subarray α) Nat α fun (xs : ) (i : Nat) => i < xs.size
Equations
• Subarray.instGetElemNatLtSize = { getElem := fun (xs : ) (i : Nat) (h : i < xs.size) => xs.get i, h }
@[inline]
def Subarray.getD {α : Type u_1} (s : ) (i : Nat) (v₀ : α) :
α
Equations
• s.getD i v₀ = if h : i < s.size then s.get i, h else v₀
Instances For
@[reducible, inline]
abbrev Subarray.get! {α : Type u_1} [] (s : ) (i : Nat) :
α
Equations
• s.get! i = s.getD i default
Instances For
def Subarray.popFront {α : Type u_1} (s : ) :
Equations
• s.popFront = if h : s.start < s.stop then { array := s.array, start := s.start + 1, stop := s.stop, start_le_stop := , stop_le_array_size := } else s
Instances For
@[inline]
unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [] (s : ) (b : β) (f : αβm (ForInStep β)) :
m β
Instances For
@[specialize #[]]
unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [] (s : ) (f : αβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
m β
Instances For
@[implemented_by Subarray.forInUnsafe]
opaque Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [] (s : ) (b : β) (f : αβm (ForInStep β)) :
m β
instance Subarray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} :
ForIn m (Subarray α) α
Equations
• Subarray.instForIn = { forIn := fun {β : Type ?u.20} [] => Subarray.forIn }
@[inline]
def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [] (f : βαm β) (init : β) (as : ) :
m β
Equations
Instances For
@[inline]
def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [] (f : αβm β) (init : β) (as : ) :
m β
Equations
Instances For
@[inline]
def Subarray.anyM {α : Type u} {m : TypeType w} [] (p : αm Bool) (as : ) :
Equations
Instances For
@[inline]
def Subarray.allM {α : Type u} {m : TypeType w} [] (p : αm Bool) (as : ) :
Equations
Instances For
@[inline]
def Subarray.forM {α : Type u} {m : Type v → Type w} [] (f : α) (as : ) :
Equations
Instances For
@[inline]
def Subarray.forRevM {α : Type u} {m : Type v → Type w} [] (f : α) (as : ) :
Equations
Instances For
@[inline]
def Subarray.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : ) :
β
Equations
Instances For
@[inline]
def Subarray.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : ) :
β
Equations
Instances For
@[inline]
def Subarray.any {α : Type u} (p : αBool) (as : ) :
Equations
Instances For
@[inline]
def Subarray.all {α : Type u} (p : αBool) (as : ) :
Equations
Instances For
@[inline]
def Subarray.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [] (as : ) (f : αm (Option β)) :
m (Option β)
Equations
Instances For
@[specialize #[]]
def Subarray.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [] (as : ) (f : αm (Option β)) (i : Nat) :
i as.sizem (Option β)
Equations
Instances For
@[inline]
def Subarray.findRevM? {α : Type} {m : TypeType w} [] (as : ) (p : αm Bool) :
m (Option α)
Equations
• as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_liftp a pure (if __do_lift = true then some a else none)
Instances For
@[inline]
def Subarray.findRev? {α : Type} (as : ) (p : αBool) :
Equations
• as.findRev? p = (as.findRevM? p).run
Instances For
def Array.toSubarray {α : Type u} (as : ) (start : ) (stop : optParam Nat as.size) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Array.ofSubarray {α : Type u} (s : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Array.instCoeSubarray {α : Type u} :
Coe (Subarray α) (Array α)
Equations
• Array.instCoeSubarray = { coe := Array.ofSubarray }
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Subarray.toArray {α : Type u_1} (s : ) :
Equations
• s.toArray = s
Instances For
instance instAppendSubarray {α : Type u_1} :
Equations
• instAppendSubarray = { append := fun (x y : ) => let a := x.toArray ++ y.toArray; a.toSubarray }
instance instReprSubarray {α : Type u_1} [Repr α] :
Equations
instance instToStringSubarray {α : Type u_1} [] :
Equations
• instToStringSubarray = { toString := fun (s : ) => toString s.toArray }