Inductive json : Set :=
  (** A boolean constant. *)
  | JsonBoolean : bool -> json
  (** An integer constant. *)
  | JsonInteger : nat -> json
  (** A floating point constant. *)
  | JsonFloat   : json
  (** A string constant. *)
  | JsonString  : string -> json
  (** An object. *)
  | JsonObject  : list (string * json) -> json
  (** An array. *)
  | JsonArray   : list json -> json
  .
