This module provides slice notation for list slices (a.k.a. Sublist) and implements an iterator for those slices.

class Std.Slice.Internal.ListSliceData (α : Type u) : Type u

Internal representation of ListSlice, which is an abbreviation for Slice ListSliceData.

• list : List α

  The relevant suffix of the underlying list.

• stop : Option Nat

  The maximum length of the slice, starting at the beginning of list.

@[reducible, inline]

abbrev ListSlice (α : Type u) : Type u

A region of some underlying list. List slices can be used to avoid copying or allocating space, while being more convenient than tracking the bounds by hand.

A list slice only stores the suffix of the underlying list, starting from the range's lower bound so that the cost of operations on the slice does not depend on the start position. However, the cost of creating a list slice is linear in the start position.

Equations

• ListSlice α = Std.Slice (Std.Slice.Internal.ListSliceData α)

def List.toSlice {α : Type u} (as : List α) (start stop : Nat) : ListSlice α

Returns a slice of a list with the given bounds.

If start or stop are not valid bounds for a sublist, then they are clamped to the list's length. Additionally, the starting index is clamped to the ending index.

This function is linear in start because it stores as.drop start in the slice.

Equations

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

def List.toUnboundedSlice {α : Type u} (as : List α) (start : Nat) : ListSlice α

Returns a slice of a list with the given lower bound.

If start is not a valid bound for a sublist, then they are clamped to the list's length.

This function is linear in start because it stores as.drop start in the slice.

Equations

• as.toUnboundedSlice start = { internalRepresentation := { list := List.drop start as, stop := none } }

instance instSliceableListNatListSlice {α : Type u} : Std.Rcc.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice = { mkSlice := fun (xs : List α) (range : Std.Rcc Nat) => xs.toSlice range.lower (range.upper + 1) }

instance instSliceableListNatListSlice_1 {α : Type u} : Std.Rco.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_1 = { mkSlice := fun (xs : List α) (range : Std.Rco Nat) => xs.toSlice range.lower range.upper }

instance instSliceableListNatListSlice_2 {α : Type u} : Std.Rci.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_2 = { mkSlice := fun (xs : List α) (range : Std.Rci Nat) => xs.toUnboundedSlice range.lower }

instance instSliceableListNatListSlice_3 {α : Type u} : Std.Roc.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_3 = { mkSlice := fun (xs : List α) (range : Std.Roc Nat) => xs.toSlice (range.lower + 1) (range.upper + 1) }

instance instSliceableListNatListSlice_4 {α : Type u} : Std.Roo.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_4 = { mkSlice := fun (xs : List α) (range : Std.Roo Nat) => xs.toSlice (range.lower + 1) range.upper }

instance instSliceableListNatListSlice_5 {α : Type u} : Std.Roi.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_5 = { mkSlice := fun (xs : List α) (range : Std.Roi Nat) => xs.toUnboundedSlice (range.lower + 1) }

instance instSliceableListNatListSlice_6 {α : Type u} : Std.Ric.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_6 = { mkSlice := fun (xs : List α) (range : Std.Ric Nat) => xs.toSlice 0 (range.upper + 1) }

instance instSliceableListNatListSlice_7 {α : Type u} : Std.Rio.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_7 = { mkSlice := fun (xs : List α) (range : Std.Rio Nat) => xs.toSlice 0 range.upper }

instance instSliceableListNatListSlice_8 {α : Type u} : Std.Rii.Sliceable (List α) Nat (ListSlice α)

Equations

• instSliceableListNatListSlice_8 = { mkSlice := fun (xs : List α) (x : Std.Rii Nat) => xs.toUnboundedSlice 0 }