structure Subarray (α : Type u) : Type u

• as : Array α
• start : Nat
• stop : Nat
• h₁ : s.start ≤ s.stop
• h₂ : s.stop ≤ Array.size s.as

def Subarray.size {α : Type u_1} (s : Subarray α) : Nat

def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin (Subarray.size s)) : α

instance Subarray.instGetElemSubarrayNatLtInstLTNatSize {α : Type u_1} : GetElem (Subarray α) Nat α fun xs i => i < Subarray.size xs

@[inline]

def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) : α

@[inline, reducible]

abbrev Subarray.get! {α : Type u_1} [Inhabited α] (s : Subarray α) (i : Nat) : α

def Subarray.popFront {α : Type u_1} (s : Subarray α) : Subarray α

@[inline]

unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β

@[specialize #[]]

unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (f : α → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) : m β

@[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.instForInSubarray {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn m (Subarray α) α

@[inline]

def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β

@[inline]

def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β

@[inline]

def Subarray.anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool

@[inline]

def Subarray.allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool

@[inline]

def Subarray.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit

@[inline]

def Subarray.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit

@[inline]

def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β

@[inline]

def Subarray.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β

@[inline]

def Subarray.any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool

@[inline]

def Subarray.all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool

@[inline]

def Subarray.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β)

@[specialize #[]]

def Subarray.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) (i : Nat) : i ≤ Subarray.size as → m (Option β)

Equations

• One or more equations did not get rendered due to their size.
• Subarray.findSomeRevM?.find as f 0 x_2 = pure none

@[inline]

def Subarray.findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α)

@[inline]

def Subarray.findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α

def Array.toSubarray {α : Type u} (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) : Subarray α

def Array.ofSubarray {α : Type u} (s : Subarray α) : Array α

instance Array.instCoeSubarrayArray {α : Type u} : Coe (Subarray α) (Array α)

def Array.«term__[_:_]» : Lean.TrailingParserDescr

def Array.«term__[_:]» : Lean.TrailingParserDescr

def Array.«term__[:_]» : Lean.TrailingParserDescr

def Subarray.toArray {α : Type u_1} (s : Subarray α) : Array α

instance instAppendSubarray {α : Type u_1} : Append (Subarray α)

instance instReprSubarray {α : Type u_1} [Repr α] : Repr (Subarray α)

instance instToStringSubarray {α : Type u_1} [ToString α] : ToString (Subarray α)