class Std.Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being closed.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Rcc β) : γ

  Slices carrier from range.lower to range.upper, both inclusive.

class Std.Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-open.

The type of resulting the slices is γ.

• mkSlice (carrier : α) (range : Rco β) : γ

  Slices carrier from range.lower (inclusive) to range.upper (exclusive).

class Std.Rci.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-unbounded.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Rci β) : γ

  Slices carrier from range.lower (inclusive).

class Std.Roc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-closed.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Roc β) : γ

  Slices carrier from range.lower (exclusive) to range.upper (inclusive).

class Std.Roo.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being open.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Roo β) : γ

  Slices carrier from range.lower to range.upper, both exclusive.

class Std.Roi.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-unbounded.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Roi β) : γ

  Slices carrier from range.lower (exclusive).

class Std.Ric.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-closed.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Ric β) : γ

  Slices carrier up to range.upper (inclusive).

class Std.Rio.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-open.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Rio β) : γ

  Slices carrier up to range.upper (exclusive).

class Std.Rii.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) : Type (max u w)

This typeclass indicates how to obtain slices of elements of α over the full range in the index type β.

The type of the resulting slices is γ.

• mkSlice (carrier : α) (range : Rii β) : γ

  Slices carrier with no bounds.