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

S32 : DType

S64 : DType

U32 : DType

U64 : DType

F64 : DType

Hints:

Ord dtype -> Eq dtype

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:

NumS32 : Num S32

NumS64 : Num S64

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:

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:

AbsS32 : Abs S32

AbsS64 : Abs S64

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:

IntegralS32 : Integral S32

IntegralS64 : Integral S64

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 Eq : DType -> Type

Totality: total
Visibility: public export
Constructors:

EqPRED : Eq PRED

EqS32 : Eq S32

EqS64 : Eq S64

EqU32 : Eq U32

EqU64 : Eq U64

EqF64 : Eq F64

Hint: 

Ord dtype -> Eq dtype

data Ord : DType -> Type

Totality: total
Visibility: public export
Constructors:

OrdS32 : Ord S32

OrdS64 : Ord S64

OrdU32 : Ord U32

OrdU64 : Ord U64

OrdF64 : Ord F64

Hint: 

Ord dtype -> Eq dtype

ordEq : Ord dtype -> Eq dtype

Totality: total
Visibility: export