structure Subarray (α : Type u) : Type u

• array : Array α
• start : Nat
• stop : Nat
• start_le_stop : self.start ≤ self.stop
• stop_le_array_size : self.stop ≤ self.array.size

theorem Subarray.start_le_stop {α : Type u} (self : Subarray α) : self.start ≤ self.stop

theorem Subarray.stop_le_array_size {α : Type u} (self : Subarray α) : self.stop ≤ self.array.size

@[reducible, inline, deprecated Subarray.array]

abbrev Subarray.as {α : Type u_1} (s : Subarray α) : Array α

Equations

• s.as = s.array

@[deprecated Subarray.start_le_stop]

theorem Subarray.h₁ {α : Type u_1} (s : Subarray α) : s.start ≤ s.stop

@[deprecated Subarray.stop_le_array_size]

theorem Subarray.h₂ {α : Type u_1} (s : Subarray α) : s.stop ≤ s.array.size

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

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

• Subarray.instGetElemNatLtSize = { getElem := fun (xs : Subarray α) (i : Nat) (h : i < xs.size) => xs.get ⟨i, h⟩ }

@[inline]

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

Equations

• s.getD i v₀ = if h : i < s.size then s.get ⟨i, h⟩ else v₀

@[reducible, inline]

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

Equations

• s.get! i = s.getD i default

def Subarray.popFront {α : Type u_1} (s : Subarray α) : 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

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

Equations

• Subarray.instForIn = { forIn := fun {β : Type ?u.20} [Monad m] => Subarray.forIn }

@[inline]

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

Equations

• Subarray.foldlM f init as = Array.foldlM f init as.array as.start as.stop

@[inline]

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

Equations

• Subarray.foldrM f init as = Array.foldrM f init as.array as.stop as.start

@[inline]

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

Equations

• Subarray.anyM p as = Array.anyM p as.array as.start as.stop

@[inline]

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

Equations

• Subarray.allM p as = Array.allM p as.array as.start as.stop

@[inline]

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

Equations

• Subarray.forM f as = Array.forM f as.array as.start as.stop

@[inline]

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

Equations

• Subarray.forRevM f as = Array.forRevM f as.array as.stop as.start

@[inline]

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

Equations

• Subarray.foldl f init as = (Subarray.foldlM f init as).run

@[inline]

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

Equations

• Subarray.foldr f init as = (Subarray.foldrM f init as).run

@[inline]

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

Equations

• Subarray.any p as = (Subarray.anyM p as).run

@[inline]

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

Equations

• Subarray.all p as = (Subarray.allM p as).run

@[inline]

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

Equations

• as.findSomeRevM? f = Subarray.findSomeRevM?.find as f as.size ⋯

@[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.size → m (Option β)

Equations

• Subarray.findSomeRevM?.find as f 0 x_2 = pure none
• Subarray.findSomeRevM?.find as f i.succ h = do let r ← f as[i] match r with | some val => pure r | none => let_fun this := ⋯; Subarray.findSomeRevM?.find as f i this

@[inline]

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

Equations

• as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)

@[inline]

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

Equations

• as.findRev? p = (as.findRevM? p).run

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Array.instCoeSubarray = { coe := Array.ofSubarray }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• s.toArray = ↑s

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

Equations

• instAppendSubarray = { append := fun (x y : Subarray α) => let a := x.toArray ++ y.toArray; a.toSubarray }

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

Equations

• instReprSubarray = { reprPrec := fun (s : Subarray α) (x : Nat) => repr s.toArray ++ Std.Format.text ".toSubarray" }

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

Equations

• instToStringSubarray = { toString := fun (s : Subarray α) => toString s.toArray }