Documentation

Init.Data.Slice.Basic

structure Std.Slice (γ : 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 : γ
Instances For
    class Std.Slice.Self (α : Type u) (β : outParam (Type u)) :

    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 : α = β
    Instances