This module implements an iterator for list slices.

@[instance_reducible, inline]

instance ListSlice.instToIterator {α : Type u} : Std.ToIterator (Std.Slice (Std.Slice.Internal.ListSliceData α)) Id (Std.Iterators.Types.Take (Std.Iterators.Types.ListIterator α) Id) α

Equations

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

@[instance_reducible]

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).length }

@[instance_reducible]

instance instForInListSliceOfMonad {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (ListSlice α) α

Equations

• instForInListSliceOfMonad = { forIn := fun {β : Type ?u.24} (xs : ListSlice α) (init : β) (f : α → β → m (ForInStep β)) => forIn (Std.Slice.Internal.iter xs) init f }

@[instance_reducible]

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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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