structure Subarray (α : Type u) : Type u

A region of some underlying array.

A subarray contains an array together with the start and end indices of a region of interest. Subarrays can be used to avoid copying or allocating space, while being more convenient than tracking the bounds by hand. The region of interest consists of every index that is both greater than or equal to start and strictly less than stop.

• array : Array α

  The underlying array.

• start : Nat

  The starting index of the region of interest (inclusive).

• stop : Nat

  The ending index of the region of interest (exclusive).

• start_le_stop : self.start ≤ self.stop

  The starting index is no later than the ending index.

  The ending index is exclusive. If the starting and ending indices are equal, then the subarray is empty.

• stop_le_array_size : self.stop ≤ self.array.size

  The stopping index is no later than the end of the array.

  The ending index is exclusive. If it is equal to the size of the array, then the last element of the array is in the subarray.

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

Computes the size of the subarray.

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) : α

Extracts an element from the subarray.

The index is relative to the start of the subarray, rather than the underlying array.

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

@[inline]

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

Extracts an element from the subarray, or returns a default value v₀ when the index is out of bounds.

The index is relative to the start and end of the subarray, rather than the underlying array.

@[reducible, inline]

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

Extracts an element from the subarray, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the subarray, rather than the underlying array. The default value is that provided by the Inhabited α instance.

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

Shrinks the subarray by incrementing its starting index if possible, returning it unchanged if not.

Examples:

• #[1,2,3].toSubarray.popFront.toArray = #[2, 3]
• #[1,2,3].toSubarray.popFront.popFront.toArray = #[3]
• #[1,2,3].toSubarray.popFront.popFront.popFront.toArray = #[]
• #[1,2,3].toSubarray.popFront.popFront.popFront.popFront.toArray = #[]

def Subarray.empty {α : Type u_1} : Subarray α

The empty subarray.

This empty subarray is backed by an empty array.

instance Subarray.instEmptyCollection {α : Type u_1} : EmptyCollection (Subarray α)

instance Subarray.instInhabited {α : Type u_1} : Inhabited (Subarray α)

@[inline]

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

The run-time implementation of ForIn.forIn for Subarray, which allows it to be used with for loops in do-notation.

This definition replaces Subarray.forIn.

@[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 β

@[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 β

The implementation of ForIn.forIn for Subarray, which allows it to be used with for loops in do-notation.

instance Subarray.instForIn {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 β

Folds a monadic operation from left to right over the elements in a subarray.

An accumulator of type β is constructed by starting with init and monadically combining each element of the subarray with the current accumulator value in turn. The monad in question may permit early termination or repetition.

Examples:

#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
  let l ← Option.guard (· ≠ 0) x.length
  return s!"{acc}({l}){x} "

some "(3)red (5)green (4)blue "

#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
  let l ← Option.guard (· ≠ 5) x.length
  return s!"{acc}({l}){x} "

none

@[inline]

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

Folds a monadic operation from right to left over the elements in a subarray.

An accumulator of type β is constructed by starting with init and monadically combining each element of the subarray with the current accumulator value in turn, moving from the end to the start. The monad in question may permit early termination or repetition.

Examples:

#eval #["red", "green", "blue"].toSubarray.foldrM (init := "") fun x acc => do
  let l ← Option.guard (· ≠ 0) x.length
  return s!"{acc}({l}){x} "

some "(4)blue (5)green (3)red "

#eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
  let l ← Option.guard (· ≠ 5) x.length
  return s!"{acc}({l}){x} "

none

@[inline]

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

Checks whether any of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that satisfies the predicate is found.

Example:

#eval #["red", "green", "blue", "orange"].toSubarray.popFront.anyM fun x => do
  IO.println x
  pure (x == "blue")

green
blue

true

@[inline]

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

Checks whether all of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that does not satisfy the predicate is found.

Example:

#eval #["red", "green", "blue", "orange"].toSubarray.popFront.allM fun x => do
  IO.println x
  pure (x.length == 5)

green
blue

false

@[inline]

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

Runs a monadic action on each element of a subarray.

The elements are processed starting at the lowest index and moving up.

@[inline]

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

Runs a monadic action on each element of a subarray, in reverse order.

The elements are processed starting at the highest index and moving down.

@[inline]

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

Folds an operation from left to right over the elements in a subarray.

An accumulator of type β is constructed by starting with init and combining each element of the subarray with the current accumulator value in turn.

Examples:

• #["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12
• #["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9

@[inline]

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

Folds an operation from right to left over the elements in a subarray.

An accumulator of type β is constructed by starting with init and combining each element of the subarray with the current accumulator value in turn, moving from the end to the start.

Examples:

• #eval #["red", "green", "blue"].toSubarray.foldr (·.length + ·) 0 = 12
• #["red", "green", "blue"].toSubarray.popFront.foldlr (·.length + ·) 0 = 9

@[inline]

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

Checks whether any of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that satisfies the predicate is found.

@[inline]

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

Checks whether all of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that does not satisfy the predicate is found.

@[inline]

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

Applies a monadic function to each element in a subarray in reverse order, stopping at the first element for which the function succeeds by returning a value other than none. The succeeding value is returned, or none if there is no success.

Example:

#eval #["red", "green", "blue"].toSubarray.findSomeRevM? fun x => do
  IO.println x
  return Option.guard (· = 5) x.length

blue
green

some 5

@[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 β)

@[inline]

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

Applies a monadic Boolean predicate to each element in a subarray in reverse order, stopping at the first element that satisfies the predicate. The element that satisfies the predicate is returned, or none if no element satisfies it.

Example:

#eval #["red", "green", "blue"].toSubarray.findRevM? fun x => do
  IO.println x
  return (x.length = 5)

blue
green

some 5

@[inline]

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

Tests each element in a subarray with a Boolean predicate in reverse order, stopping at the first element that satisfies the predicate. The element that satisfies the predicate is returned, or none if no element satisfies the predicate.

Examples:

• #["red", "green", "blue"].toSubarray.findRev? (·.length ≠ 4) = some "green"
• #["red", "green", "blue"].toSubarray.findRev? (fun _ => true) = some "blue"
• #["red", "green", "blue"].toSubarray 0 0 |>.findRev? (fun _ => true) = none

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

Returns a subarray of an array, with the given bounds.

If start or stop are not valid bounds for a subarray, then they are clamped to array's size. Additionally, the starting index is clamped to the ending index.

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

Allocates a new array that contains the contents of the subarray.

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

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

A subarray with the provided bounds.

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

A subarray with the provided lower bound that extends to the rest of the array.

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

A subarray with the provided upper bound, starting at the index 0.

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

Allocates a new array that contains the contents of the subarray.

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

def Subarray.repr {α : Type u_1} [Repr α] (s : Subarray α) : Std.Format

Subarray representation.

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

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