Spidr.DType

Tensor data types, and their interaction with Idris.

This module contains a number of data types (`Num`, `Eq` etc.) which indicate what operations
can be performed on primitive data in the backend. They are entirely
distinct from the Idris interfaces `Prelude.Num` etc. but carry largely the same meaning.

Definitions

data DType : Type

Totality: total
Visibility: public export
Constructors:

PRED : DType

S8 : DType

S16 : DType

S32 : DType

S64 : DType

U8 : DType

U16 : DType

U32 : DType

U64 : DType

F64 : DType

Hints:

Eq DType

Neg dtype -> Num dtype

Abs dtype -> Num dtype

Integral dtype -> Num dtype

Fractional dtype -> Num dtype

Show DType

Show (Tag (Tensor shape dtype))

Show (Tensor shape dtype)

Taggable (Tensor shape dtype)

idrisType : DType -> Type

Totality: total
Visibility: public export

data Num : DType -> Type

Totality: total
Visibility: public export
Constructors:

NumS8 : Num S8

NumS16 : Num S16

NumS32 : Num S32

NumS64 : Num S64

NumU8 : Num U8

NumU16 : Num U16

NumU32 : Num U32

NumU64 : Num U64

NumF64 : Num F64

Hints:

Neg dtype -> Num dtype

Abs dtype -> Num dtype

Integral dtype -> Num dtype

Fractional dtype -> Num dtype

data Neg : DType -> Type

Totality: total
Visibility: public export
Constructors:

NegS8 : Neg S8

NegS16 : Neg S16

NegS32 : Neg S32

NegS64 : Neg S64

NegF64 : Neg F64

Hint: 

Neg dtype -> Num dtype

negNum : Neg dtype -> Num dtype

Totality: total
Visibility: export

data Abs : DType -> Type

Totality: total
Visibility: public export
Constructors:

AbsS8 : Abs S8

AbsS16 : Abs S16

AbsS32 : Abs S32

AbsS64 : Abs S64

AbsU8 : Abs U8

AbsU16 : Abs U16

AbsU32 : Abs U32

AbsU64 : Abs U64

AbsF64 : Abs F64

Hint: 

Abs dtype -> Num dtype

absNum : Abs dtype -> Num dtype

Totality: total
Visibility: export

data Integral : DType -> Type

Totality: total
Visibility: public export
Constructors:

IntegralS8 : Integral S8

IntegralS16 : Integral S16

IntegralS32 : Integral S32

IntegralS64 : Integral S64

IntegralU8 : Integral U8

IntegralU16 : Integral U16

IntegralU32 : Integral U32

IntegralU64 : Integral U64

Hint: 

Integral dtype -> Num dtype

integralNum : Integral dtype -> Num dtype

Totality: total
Visibility: export

data Fractional : DType -> Type

Totality: total
Visibility: public export
Constructor: 

FractionalF64 : Fractional F64

Hint: 

Fractional dtype -> Num dtype

fractionalNum : Fractional dtype -> Num dtype

Totality: total
Visibility: export

data Ord : DType -> Type

Totality: total
Visibility: public export
Constructors:

OrdS8 : Ord S8

OrdS16 : Ord S16

OrdS32 : Ord S32

OrdS64 : Ord S64

OrdU8 : Ord U8

OrdU16 : Ord U16

OrdU32 : Ord U32

OrdU64 : Ord U64

OrdF64 : Ord F64