Defines `Shape`, which quantifies the structure of array-like data types.
import public Data.Nat
import public Data.Vect0 Shape : TypeDescribes the shape of a `Tensor`. For example, a `Tensor` of `Double`s with contents
`[[0, 1, 2], [3, 4, 5]]` has two elements in its outer-most axis, and each of those elements
has three `Double`s in it, so this has shape [2, 3]. A `Tensor` can have axes of zero length,
though the shape cannot be unambiguously inferred by visualising it. For example, `[[], []]`
can have shape [2, 0], [2, 0, 5] or etc. A scalar `Tensor` has shape `[]`.
0 Array : (0 _ : Shape) -> (0 _ : Type) -> TypeAn `Array shape dtype` is either:
* a single value of type `dtype` (for `shape` `[]`), or
* an arbitrarily nested array of `Vect`s of such values (for any other `shape`)
@shape The shape of the array.
@dtype The type of elements of the array.