This module implements an iterator for list slices.

instance instToIteratorListSliceId {α : Type u} {s : ListSlice α} : Std.Iterators.ToIterator s Id α

Equations

• One or more equations did not get rendered due to their size.

instance instIteratorStateListSliceId {α : Type u} {s : ListSlice α} : Std.Iterators.Iterator (Std.Iterators.ToIterator.State s Id) Id α

Equations

• instIteratorStateListSliceId = inferInstance

instance instFiniteStateListSliceId {α : Type u} {s : ListSlice α} : Std.Iterators.Finite (Std.Iterators.ToIterator.State s Id) Id

instance instIteratorCollectStateListSliceId {α : Type u} {s : ListSlice α} : Std.Iterators.IteratorCollect (Std.Iterators.ToIterator.State s Id) Id Id

Equations

• instIteratorCollectStateListSliceId = inferInstance

instance instIteratorCollectPartialStateListSliceId {α : Type u} {s : ListSlice α} : Std.Iterators.IteratorCollectPartial (Std.Iterators.ToIterator.State s Id) Id Id

Equations

• instIteratorCollectPartialStateListSliceId = inferInstance

instance instIteratorLoopStateListSliceIdOfMonad {α : Type u} {s : ListSlice α} {m : Type v → Type w} [Monad m] : Std.Iterators.IteratorLoop (Std.Iterators.ToIterator.State s Id) Id m

Equations

• instIteratorLoopStateListSliceIdOfMonad = inferInstance

instance instIteratorLoopPartialStateListSliceIdOfMonad {α : Type u} {s : ListSlice α} {m : Type v → Type w} [Monad m] : Std.Iterators.IteratorLoopPartial (Std.Iterators.ToIterator.State s Id) Id m

Equations

• instIteratorLoopPartialStateListSliceIdOfMonad = inferInstance

instance instSliceSizeListSliceData {α : Type u} : Std.Slice.SliceSize (Std.Slice.Internal.ListSliceData α)

Equations

• instSliceSizeListSliceData = { size := fun (s : Std.Slice (Std.Slice.Internal.ListSliceData α)) => (Std.Slice.Internal.iter s).count }

instance instForInListSlice {α : Type u} {m : Type v → Type w} : ForIn m (ListSlice α) α

Equations

• instForInListSlice = { forIn := fun {β : Type ?u.20} [Monad m] (xs : ListSlice α) (init : β) (f : α → β → m (ForInStep β)) => forIn (Std.Slice.Internal.iter xs) init f }

def List.ofSlice {α : Type u} (s : ListSlice α) : List α

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

Equations

• List.ofSlice s = Std.Slice.toList s

instance List.instAppendListSlice {α : Type u} : Append (ListSlice α)

Equations

• List.instAppendListSlice = { append := fun (x y : ListSlice α) => have a := Std.Slice.toList x ++ Std.Slice.toList y; a.toSlice 0 a.length }

def List.ListSlice.repr {α : Type u} [Repr α] (s : ListSlice α) : Std.Format

ListSlice representation.

Equations

• List.ListSlice.repr s = repr (Std.Slice.toList s) ++ Std.Format.text ".toSlice 0 " ++ Std.Format.text (toString (Std.Slice.toList s).length)

instance List.instReprListSlice {α : Type u} [Repr α] : Repr (ListSlice α)

Equations

• List.instReprListSlice = { reprPrec := fun (s : ListSlice α) (x : Nat) => List.ListSlice.repr s }

instance List.instToStringListSlice {α : Type u} [ToString α] : ToString (ListSlice α)

Equations

• List.instToStringListSlice = { toString := fun (s : ListSlice α) => toString (Std.Slice.toArray s) }

def ListSlice.toList {α : Type u} (s : ListSlice α) : List α

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

Equations

• s.toList = List.ofSlice s