Idris2Doc : Data.Bytes.Interfaces

Data.Bytes.Interfaces

(source)
Definitions
data Endian : Type
  Totality: total
  Visibility: public export
  Constructors:
  
BigEndian : Endian
  
LittleEndian : Endian
  
NetworkEndian : Endian
interface Bytes : Type -> Type
  Parameters: num
Constructor: 
MkBytes

Methods:
  
byteSize : Nat
  
toBytes : Endian -> num -> Vect byteSize Bits8
  
fromBytes : Endian -> Vect byteSize Bits8 -> num

Implementations:
  
Bytes Double
  
Bytes Bits8
  
Bytes Bits16
  
Bytes Bits32
  
Bytes Bits64
  
Bytes Int8
  
Bytes Int16
  
Bytes Int32
  
Bytes Int64
  
Bytes Int
byteSize : Bytes num => Nat
  Totality: total
  Visibility: public export
toBytes : {auto __con : Bytes num} -> Endian -> num -> Vect byteSize Bits8
  Totality: total
  Visibility: public export
fromBytes : {auto __con : Bytes num} -> Endian -> Vect byteSize Bits8 -> num
  Totality: total
  Visibility: public export