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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

• instIteratorLoopSubarrayIteratorIdOfMonad = Std.IteratorLoop.defaultImplementation

@[implicit_reducible, inline]

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

Equations

• Subarray.instToIterator = Std.ToIterator.of (SubarrayIterator α) fun (x : Std.Slice (Std.Slice.Internal.SubarrayData α)) => { internalState := { xs := x } }

@[implicit_reducible]

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

Equations

• instForInSubarrayOfMonad = inferInstance

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.

Equations

• s.forIn b f = forIn s b f

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

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

Equations

• ↑s = Std.Slice.toArray s

@[implicit_reducible]

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

Equations

• instCoeSubarrayArray = { coe := Subarray.copy }

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

Equations

• Array.ofSubarray s = Std.Slice.toArray s

@[implicit_reducible]

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

Equations

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

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

Subarray representation.

Equations

• Array.Subarray.repr s = repr (Std.Slice.toArray s) ++ Std.Format.text ".toSubarray"

@[implicit_reducible]

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

Equations

• Array.instReprSubarray = { reprPrec := fun (s : Subarray α) (x : Nat) => Array.Subarray.repr s }

@[implicit_reducible]

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

Equations

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