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 }

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

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

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

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

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

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

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