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 {g : Type u_1} {β : Type u_2} (s : Slice g) [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 {g : Type u_1} {β : Type u_2} (s : Slice g) [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 {g : Type u_1} {β : Type u_2} (s : Slice g) [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 {g : Type u_1} {β : Type u_2} (s : Slice g) [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