Data.Buffer

peekBuffer : Buffer (n + offset) -> (offset3 : Nat) -> Buffer n

Create a view over a buffer

peekBits8 : Buffer (fromInteger 1 + n) -> (offset : Fin (S n)) -> Bits8

Read a Bits8 from a Buffer starting at offset

peekBits64Native : Buffer (fromInteger 8 + n) -> (offset : Fin (S n)) -> Bits64

Read a Bits64 in native byte order from a Buffer starting at offset

peekBits64LE : Buffer (fromInteger 8 + n) -> (offset : Fin (S n)) -> Bits64

Read a little-endian Bits64 from a Buffer starting at offset

peekBits64BE : Buffer (fromInteger 8 + n) -> (offset : Fin (S n)) -> Bits64

Read a big-endian Bits64 from a Buffer starting at offset

peekBits32Native : Buffer (fromInteger 4 + n) -> (offset : Fin (S n)) -> Bits32

Read a Bits32 in native byte order from a Buffer starting at offset

peekBits32LE : Buffer (fromInteger 4 + n) -> (offset : Fin (S n)) -> Bits32

Read a little-endian Bits32 from a Buffer starting at offset

peekBits32BE : Buffer (fromInteger 4 + n) -> (offset : Fin (S n)) -> Bits32

Read a big-endian Bits32 from a Buffer starting at offset

peekBits16Native : Buffer (fromInteger 2 + n) -> (offset : Fin (S n)) -> Bits16

Read a Bits16 in native byte order from a Buffer starting at offset

peekBits16LE : Buffer (fromInteger 2 + n) -> (offset : Fin (S n)) -> Bits16

Read a little-endian Bits16 from a Buffer starting at offset

peekBits16BE : Buffer (fromInteger 2 + n) -> (offset : Fin (S n)) -> Bits16

Read a big-endian Bits16 from a Buffer starting at offset

copy : Buffer n -> Buffer n

Copy a buffer, potentially allowing the (potentially large) space it
pointed to to be freed

appendBuffer : Buffer n -> (count : Nat) -> Buffer m -> Buffer (n + count * m)

Append count repetitions of a Buffer to another Buffer

appendBits8 : Buffer n -> (count : Nat) -> Bits8 -> Buffer (n + count * fromInteger 1)

Append count repetitions of a Bits8 to a Buffer

appendBits64Native : Buffer n -> (count : Nat) -> Bits64 -> Buffer (n + count * fromInteger 8)

Append count repetitions of a Bits64 in native byte order to a Buffer

appendBits64LE : Buffer n -> (count : Nat) -> Bits64 -> Buffer (n + count * fromInteger 8)

Append count repetitions of a little-endian Bits64 to a Buffer

appendBits64BE : Buffer n -> (count : Nat) -> Bits64 -> Buffer (n + count * fromInteger 8)

Append count repetitions of a big-endian Bits64 to a Buffer

appendBits32Native : Buffer n -> (count : Nat) -> Bits32 -> Buffer (n + count * fromInteger 4)

Append count repetitions of a Bits32 in native byte order to a Buffer

appendBits32LE : Buffer n -> (count : Nat) -> Bits32 -> Buffer (n + count * fromInteger 4)

Append count repetitions of a little-endian Bits32 to a Buffer

appendBits32BE : Buffer n -> (count : Nat) -> Bits32 -> Buffer (n + count * fromInteger 4)

Append count repetitions of a big-endian Bits32 to a Buffer

appendBits16Native : Buffer n -> (count : Nat) -> Bits16 -> Buffer (n + count * fromInteger 2)

Append count repetitions of a Bits16 in native byte order to a Buffer

appendBits16LE : Buffer n -> (count : Nat) -> Bits16 -> Buffer (n + count * fromInteger 2)

Append count repetitions of a little-endian Bits16 to a Buffer

appendBits16BE : Buffer n -> (count : Nat) -> Bits16 -> Buffer (n + count * fromInteger 2)

Append count repetitions of a big-endian Bits16 to a Buffer

allocate : (hint : Nat) -> Buffer 0

Allocate an empty Buffer. The size hint can be used to avoid
unnecessary reallocations and copies under the hood if the
approximate ultimate size of the Buffer is known. Users can assume
the new Buffer is word-aligned.

data Buffer : Nat -> Type

A contiguous chunk of n bytes

MkBuffer : (offset : Nat) -> (realBuffer : prim__UnsafeBuffer) -> Buffer n