This module implements an iterator for array slices (Subarray).

@[unbox]

structure SubarrayIterator (α : Type u) : Type u

• xs : Subarray α

@[inline]

def SubarrayIterator.step {α : Type u} {m : Type u → Type u_1} : Std.IterM Id α → Std.IterStep (Std.IterM m α) α

instance instIteratorSubarrayIteratorId {α : Type u} : Std.Iterator (SubarrayIterator α) Id α

instance SubarrayIterator.instFinite {α : Type u} : Std.Iterators.Finite (SubarrayIterator α) Id

instance instIteratorLoopSubarrayIteratorIdOfMonad {α : Type u} {m : Type u_1 → Type u_2} [Monad m] : Std.IteratorLoop (SubarrayIterator α) Id m

@[inline]

instance Subarray.instToIterator {α : Type u} : Std.ToIterator (Std.Slice (Std.Slice.Internal.SubarrayData α)) Id (SubarrayIterator α) α

instance instSliceSizeSubarrayData {α : Type u} : Std.Slice.SliceSize (Std.Slice.Internal.SubarrayData α)

instance instForInSubarrayOfMonad {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (Subarray α) α

Without defining the following function Subarray.foldlM, it is still possible to call subarray.foldlM, which would be elaborated to Slice.foldlM (s := subarray). However, in order to maximize backward compatibility and avoid confusion in the manual entry for Subarray, we explicitly provide the wrapper function Subarray.foldlM for Slice.foldlM, providing a more specific docstring.

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

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

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

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

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

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

@[simp]

theorem Subarray.copy_eq_toArray {α : Type u} {s : Subarray α} : s.copy = ↑s

theorem Subarray.sliceToArray_eq_toArray {α : Type u} {s : Subarray α} : Std.Slice.toArray s = ↑s

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

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

instance Array.instAppendSubarray {α : Type u} : Append (Subarray α)

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

Subarray representation.

instance Array.instReprSubarray {α : Type u} [Repr α] : Repr (Subarray α)

instance Array.instToStringSubarray {α : Type u} [ToString α] : ToString (Subarray α)