Idris2Doc : Data.Bytes.Impls

Data.Bytes.Impls

(source)
Reexports
import public Data.Bits
Definitions
implBytesForFiniteBits : {auto {conArg:824} : FiniteBits num} -> Cast num Bits8 => Cast Bits8 num => IsJust (isMultN 8 bitSize) => Bytes num
  Totality: total
  Visibility: public export
bytesForBits8 : Bytes Bits8
  Totality: total
  Visibility: public export
bytesForBits16 : Bytes Bits16
  Totality: total
  Visibility: public export
bytesForBits32 : Bytes Bits32
  Totality: total
  Visibility: public export
bytesForBits64 : Bytes Bits64
  Totality: total
  Visibility: public export
bytesForInt8 : Bytes Int8
  Totality: total
  Visibility: public export
bytesForInt16 : Bytes Int16
  Totality: total
  Visibility: public export
bytesForInt32 : Bytes Int32
  Totality: total
  Visibility: public export
bytesForInt64 : Bytes Int64
  Totality: total
  Visibility: public export
bytesForInt : Bytes Int
  Totality: total
  Visibility: public export