  Inductive binaryExp : Set :=
    (** A 32-bit unsigned integer. *)
    | BiU32     : nat -> binaryExp
    (** A 64-bit unsigned integer. *)
    | BiU64     : nat -> binaryExp
    (** A 64-bit IEEE754 binary64 value. *)
    | BiF64     : R -> binaryExp
    (** A sequence of bytes. *)
    | BiBytes   : list byte -> binaryExp
    (** A sequence of bytes describing UTF-8 encoded text. *)
    | BiUTF8    : list byte -> binaryExp
    (** An array of binary expressions. *)
    | BiArray   : list binaryExp -> binaryExp
    (** A section of reserved space. *)
    | BiReserve : nat -> binaryExp
    (** A record with named binary expression members. *)
    | BiRecord  : list (string * binaryExp) -> binaryExp.
