For a value `V`, we write `«V»` for the binary encoding of `V`.

```text
                      «#f» = [0x80]
                      «#t» = [0x81]

                    «@W V» = [0x85] ++ «W» ++ «V»
                     «#!V» = [0x86] ++ «V»

  «V» if V ∈ Double        = [0x87, 0x08] ++ binary64(V)

  «V» if V ∈ SignedInteger = [0xB0] ++ varint(|intbytes(V)|) ++ intbytes(V)
  «V» if V ∈ String        = [0xB1] ++ varint(|utf8(V)|) ++ utf8(V)
  «V» if V ∈ ByteString    = [0xB2] ++ varint(|V|) ++ V
  «V» if V ∈ Symbol        = [0xB3] ++ varint(|utf8(V)|) ++ utf8(V)

           «<L F_1...F_m>» = [0xB4] ++ «L» ++ «F_1» ++...++ «F_m» ++ [0x84]
             «[X_1...X_m]» = [0xB5] ++ «X_1» ++...++ «X_m» ++ [0x84]
            «#{E_1...E_m}» = [0xB6] ++ «E_1» ++...++ «E_m» ++ [0x84]
     «{K_1:V_1...K_m:V_m}» = [0xB7] ++ «K_1» ++ «V_1» ++...++ «K_m» ++ «V_m» ++ [0x84]

                 varint(n) = [n]                                  if n < 128
                             [(n & 127) | 128] ++ varint(n >> 7)  if n ≥ 128

               intbytes(n) = the empty sequence if n = 0, otherwise signedBigEndian(n)

        signedBigEndian(n) = [n & 255]                            if -128 ≤ n ≤ 127
                             signedBigEndian(n >> 8) ++ [n & 255] otherwise
```

The function `binary64(D)` yields the big-endian 8-byte IEEE 754 binary representation of `D`.