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.Iterators.IterStep (Std.IterM m α) α

Equations

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

instance instIteratorSubarrayIteratorId {α : Type u} : Std.Iterators.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

instance instIteratorCollectSubarrayIteratorIdOfMonad {α : Type u} {m : Type u → Type u_1} [Monad m] : Std.Iterators.IteratorCollect (SubarrayIterator α) Id m

Equations

• instIteratorCollectSubarrayIteratorIdOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

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

Equations

• instIteratorLoopSubarrayIteratorIdOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

@[inline]

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

Equations

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

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

Equations

• instSliceSizeSubarrayData = { size := fun (s : Std.Slice (Std.Slice.Internal.SubarrayData α)) => s.internalRepresentation.stop - s.internalRepresentation.start }

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

Equations

• Subarray.foldlM f init as = Std.Slice.foldlM f init as

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

Equations

• Subarray.foldl f init as = Std.Slice.foldl f init as

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

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

Equations

• ↑s = Std.Slice.toArray s

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

Equations

• instCoeSubarrayArray = { coe := Subarray.toArray }

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

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

Equations

• s.copy = Std.Slice.toArray s

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

Equations

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

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

Equations

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

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

Subarray representation.

Equations

• Array.Subarray.repr s = repr ↑s ++ Std.Format.text ".toSubarray"

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

Equations

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

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

Equations

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