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

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

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

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

- instIteratorStateSubarrayId = inferInstance

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

- instIteratorCollectStateSubarrayId = inferInstance

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

- instIteratorCollectPartialStateSubarrayId = inferInstance

source
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

source
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

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

- instIteratorSizeStateSubarrayId = inferInstance

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

- instIteratorSizePartialStateSubarrayId = inferInstance

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

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

source
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 }

source
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"

Instances For

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

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

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

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

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

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

Equations

- s.toArray = ↑s

Instances For