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

class Std.Slice.SliceSize (α : Type u) : Type u

This type class provides support for the Slice.size function.

• size (slice : Slice α) : Nat

  Computes the slice of a Slice. Use Slice.size instead.

class Std.Slice.LawfulSliceSize {β : Type u_1} (α : Type u) [SliceSize α] [(s : Slice α) → Iterators.ToIterator s Id β] [(s : Slice α) → Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] : Prop

This type class states that the slice's iterator emits exactly Slice.size elements before terminating.

• finite (s : Slice α) : Iterators.Finite (Iterators.ToIterator.State s Id) Id

  The iterator for every Slice α is finite.

• lawful (s : Slice α) : SliceSize.size s = (Iterators.ToIterator.iter s).count

  The iterator of a slice s of type Slice α emits exactly SliceSize.size s elements.

@[inline]

def Std.Slice.size {γ : Type u_1} (s : Slice γ) [SliceSize γ] : 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.SliceSize.size s

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