Documentation

Init.Data.Array.Subarray

def Subarray.size {α : Type u_1} (s : Subarray α) :
Equations
  • s.size = s.stop - s.start
theorem Subarray.size_le_array_size {α : Type u_1} {s : Subarray α} :
s.size s.array.size
def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin s.size) :
α
Equations
  • s.get i = s.array[s.start + i]
instance Subarray.instGetElemNatLtSize {α : Type u_1} :
GetElem (Subarray α) Nat α fun (xs : Subarray α) (i : Nat) => i < xs.size
Equations
@[inline]
def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) :
α
Equations
  • s.getD i v₀ = if h : i < s.size then s[i] else v₀
@[reducible, inline]
abbrev Subarray.get! {α : Type u_1} [Inhabited α] (s : Subarray α) (i : Nat) :
α
Equations
def Subarray.popFront {α : Type u_1} (s : Subarray α) :
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
def Subarray.empty {α : Type u_1} :

The empty subarray.

Equations
instance Subarray.instInhabited {α : Type u_1} :
Equations
@[inline]
unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
m β
Equations
@[specialize #[]]
unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (f : αβm (ForInStep β)) (sz i : USize) (b : β) :
m β
Equations
  • One or more equations did not get rendered due to their size.
@[implemented_by Subarray.forInUnsafe]
opaque Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
m β
instance Subarray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} :
ForIn m (Subarray α) α
Equations
@[inline]
def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (init : β) (as : Subarray α) :
m β
Equations
@[inline]
def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (init : β) (as : Subarray α) :
m β
Equations
@[inline]
def Subarray.anyM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Subarray α) :
Equations
@[inline]
def Subarray.allM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Subarray α) :
Equations
@[inline]
def Subarray.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Subarray α) :
Equations
@[inline]
def Subarray.forRevM {α : Type u} {m : Type v → Type w} [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
@[inline]
def Subarray.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : αm (Option β)) :
m (Option β)
Equations
@[specialize #[]]
def Subarray.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : αm (Option β)) (i : Nat) :
i as.sizem (Option β)
Equations
@[inline]
def Subarray.findRevM? {α : Type} {m : TypeType w} [Monad m] (as : Subarray α) (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)
@[inline]
def Subarray.findRev? {α : Type} (as : Subarray α) (p : αBool) :
Equations
  • as.findRev? p = (as.findRevM? p).run
def Array.toSubarray {α : Type u} (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
Equations
  • One or more equations did not get rendered due to their size.
def Array.ofSubarray {α : Type u} (s : Subarray α) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
def Subarray.toArray {α : Type u_1} (s : Subarray α) :
Equations
  • s.toArray = s
instance instAppendSubarray {α : Type u_1} :
Equations
instance instReprSubarray {α : Type u_1} [Repr α] :
Equations
instance instToStringSubarray {α : Type u_1} [ToString α] :
Equations