structure Std.Slice (γ : Type u) : Type u

Wrapper structure for slice types that makes generic slice functions available via dot notation. The implementation of the functions depends on the type γ of the internal representation.

Usually, if γ is the internal representation of a slice of some type α, then Slice γ can be used directly, but one usually creates an abbreviation AlphaSlice := Slice γ and provides Self (Slice γ) AlphaSlice and Sliceable shape α AlphaSlice instances. Then AlphaSlice can be worked with without ever thinking of Slice and it is possible to extend the API with α/γ-specific functions.

• internalRepresentation : γ

class Std.Slice.Self (α : Type u) (β : outParam (Type u)) : Prop

This typeclass determines that some type α is equal to β and that β should be used in APIs instead of α.

Self is used in the polymorphic slice library.

• eq : α = β