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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible, inline]

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

@[implicit_reducible]

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.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.copy {α : Type u} (s : Subarray α) : Array α

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

@[implicit_reducible]

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

@[simp]

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

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

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

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

@[implicit_reducible]

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

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

Subarray representation.

@[implicit_reducible]

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

@[implicit_reducible]

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