Idris2Doc : Primitive

Primitive

Supported backend primitive types, and their relation to Idris primitives.

The module contains a number of interfaces (`Primitive.Num`, `Primitive.Eq` etc.). These
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.
For example, primitive types satsifying `Primitive.Ord` have a notion of ordering.

Reexports

importpublic Compiler.Xla.XlaData

Definitions

interfaceNum : Type->Type
Parameters: dtype
Constraints: Primitive dtype
Implementations:
NumU32
NumU64
NumS32
NumS64
NumF32
NumF64
interfaceNeg : Type->Type
Parameters: dtype
Constraints: Num dtype
Implementations:
NegS32
NegS64
NegF32
NegF64
interfaceAbs : Type->Type
Parameters: dtype
Constraints: Num dtype
Implementations:
AbsS32
AbsS64
AbsF32
AbsF64
interfaceIntegral : Type->Type
Parameters: dtype
Constraints: Num dtype
Implementations:
IntegralU32
IntegralU64
IntegralS32
IntegralS64
interfaceFractional : Type->Type
Parameters: dtype
Constraints: Num dtype
Implementations:
FractionalF32
FractionalF64
interfaceEq : Type->Type
Parameters: dtype
Constraints: Primitive dtype
Implementations:
EqPRED
EqU32
EqU64
EqS32
EqS64
EqF32
EqF64
interfaceOrd : Type->Type
Parameters: dtype
Constraints: Eq dtype
Implementations:
OrdU32
OrdU64
OrdS32
OrdS64
OrdF32
OrdF64
interfacePrimitiveRW : Type->Type->Type
  A `PrimitiveRW dtype idr` means that values of type `idr` can be used to construct backend
data with data type `dtype`.

Parameters: dtype, idr
Constraints: LiteralRW dtype idr
Implementations:
PrimitiveRWPREDBool
PrimitiveRWS32Int32
PrimitiveRWU32Nat
PrimitiveRWU64Nat
PrimitiveRWF64Double