This module provides slice notation for array slices (a.k.a. Subarray) and implements an iterator for those slices.

instance instToIteratorSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.ToIterator s Id α

Equations

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

instance instIteratorStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.Iterator (Std.Iterators.ToIterator.State s Id) Id α

Equations

• instIteratorStateSubarrayId = inferInstance

instance instFiniteStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.Finite (Std.Iterators.ToIterator.State s Id) Id

instance instIteratorCollectStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.IteratorCollect (Std.Iterators.ToIterator.State s Id) Id Id

Equations

• instIteratorCollectStateSubarrayId = inferInstance

instance instIteratorCollectPartialStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.IteratorCollectPartial (Std.Iterators.ToIterator.State s Id) Id Id

Equations

• instIteratorCollectPartialStateSubarrayId = inferInstance

instance instIteratorLoopStateSubarrayIdOfMonad {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] : Std.Iterators.IteratorLoop (Std.Iterators.ToIterator.State s Id) Id m

Equations

• instIteratorLoopStateSubarrayIdOfMonad = inferInstance

instance instIteratorLoopPartialStateSubarrayIdOfMonad {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] : Std.Iterators.IteratorLoopPartial (Std.Iterators.ToIterator.State s Id) Id m

Equations

• instIteratorLoopPartialStateSubarrayIdOfMonad = inferInstance

instance instIteratorSizeStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.IteratorSize (Std.Iterators.ToIterator.State s Id) Id

Equations

• instIteratorSizeStateSubarrayId = inferInstance

instance instIteratorSizePartialStateSubarrayId {α : Type u} {s : Subarray α} : Std.Iterators.IteratorSizePartial (Std.Iterators.ToIterator.State s Id) Id

Equations

• instIteratorSizePartialStateSubarrayId = inferInstance

instance instForInSubarray {α : Type u} {m : Type v → Type w} : ForIn m (Subarray α) α

Equations

• instForInSubarray = { forIn := fun {β : Type ?u.20} [Monad m] (xs : Subarray α) (init : β) (f : α → β → m (ForInStep β)) => forIn (Std.Slice.Internal.iter xs) init f }

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

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

Equations

• ↑s = Std.Slice.toArray s

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

Equations

• Array.instCoeSubarray = { coe := Array.ofSubarray }

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"

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 (Std.Slice.toArray s) }

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

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

Equations

• s.toArray = ↑s