source
instance Std.Slice.instToIteratorMk {γ : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} {x : γ} [Iterators.ToIterator x m β] :
Iterators.ToIterator { internalRepresentation := x } m β
Equations

- Std.Slice.instToIteratorMk = { State := Std.Iterators.ToIterator.State x m, iterMInternal := Std.Iterators.ToIterator.iterMInternal }

source
@[inline]
def Std.Slice.Internal.iter {γ : Type u_1} {β : Type u_2} (s : Slice γ) [Iterators.ToIterator s Id β] :
Iter β

Internal function to obtain an iterator from a slice. Users should import `Std.Data.Iterators` and use `Std.Slice.iter` instead.

Equations

- Std.Slice.Internal.iter s = Std.Iterators.ToIterator.iter s

Instances For

source
@[inline]
def Std.Slice.size {γ : Type u_1} {β : Type u_2} (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id] :
Nat

Returns the number of elements with distinct indices in the given slice.

Example: `#[1, 1, 1][0...2].size = 2`.

Equations

- s.size = (Std.Slice.Internal.iter s).size

Instances For

source
@[inline]
def Std.Slice.toArray {γ : Type u_1} {β : Type u_2} (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] :
Array β

Allocates a new array that contains the elements of the slice.

Equations

- s.toArray = (Std.Slice.Internal.iter s).toArray

Instances For

source
@[inline]
def Std.Slice.toList {γ : Type u_1} {β : Type u_2} (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] :
List β

Allocates a new list that contains the elements of the slice.

Equations

- s.toList = (Std.Slice.Internal.iter s).toList

Instances For

source
@[inline]
def Std.Slice.toListRev {γ : Type u_1} {β : Type u_2} (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] :
List β

Allocates a new list that contains the elements of the slice in reverse order.

Equations

- s.toListRev = (Std.Slice.Internal.iter s).toListRev

Instances For

source
@[inline]
def Std.Slice.foldlM {γ : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → β → m δ) (init : δ) (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorLoop (Iterators.ToIterator.State s Id) Id m] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] :
m δ

Folds a monadic operation from left to right over the elements in a slice. An accumulator of type `β` is constructed by starting with `init` and monadically combining each element of the slice with the current accumulator value in turn. The monad in question may permit early termination or repetition.

Examples for the special case of subarrays:

    #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

- Std.Slice.foldlM f init s = Std.Iterators.Iter.foldM f init (Std.Slice.Internal.iter s)

Instances For

source
@[inline]
def Std.Slice.foldl {γ : Type u} {β : Type v} {δ : Type w} (f : δ → β → δ) (init : δ) (s : Slice γ) [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorLoop (Iterators.ToIterator.State s Id) Id Id] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] :
δ

Folds an operation from left to right over the elements in a slice. An accumulator of type `β` is constructed by starting with `init` and combining each element of the slice with the current accumulator value in turn. Examples for the special case of subarrays:

- `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
- `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`

Equations

- Std.Slice.foldl f init s = Std.Iterators.Iter.fold f init (Std.Slice.Internal.iter s)

Instances For