Types

Common library types.

Reexports

Definitions

0 Shape : Type

  Describes 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 `[]`.

Totality: total
Visibility: public export

0 Array : (0 _ : Shape) -> (0 _ : Type) -> Type

  An `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.

Totality: total
Visibility: public export

interface Bounded : Type -> Type

  A type `a` satisfying `Bounded a` has a minimum and a maximum value.

Parameters: a
Methods:

min : a

max : a

Implementation: 

Bounded Int32

min : Bounded a => a

Totality: total
Visibility: public export

max : Bounded a => a

Totality: total
Visibility: public export