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 β

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

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

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

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

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