Slice notation #
This module provides the means to obtain a slice from a collection and a range of indices via slice notation.
class
Std.Slice.Sliceable
(shape : PRange.RangeShape)
(α : Type u)
(β : outParam (Type v))
(γ : outParam (Type w))
:
Type (max (max u v) w)
This typeclass indicates how to obtain slices of α of type γ, given ranges of shape shape in
the index type β.