Primitive backend data types, and their interaction with Idris. This 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 satisfying `Primitive.Ord` have a notion of ordering.
import public Compiler.Xla.XlaDatainterface Num : Type -> Typeinterface Neg : Type -> Typeinterface Abs : Type -> Typeinterface Integral : Type -> Typeinterface Fractional : Type -> Typeinterface Eq : Type -> Typeinterface Ord : Type -> Typeinterface PrimitiveRW : Type -> Type -> TypeA `PrimitiveRW dtype idr` means that values of type `idr` can be used to construct backend
data with data type `dtype`.
PrimitiveRW PRED BoolPrimitiveRW S32 Int32PrimitiveRW U32 NatPrimitiveRW U64 NatPrimitiveRW F64 Double