Module Qcert.Cloudant.Lang.Cloudant

Cloudant is a representation for the emitted cloudant code. It is composed of a list of Cloudant design documents, a final expression, and a list of effective parameters.

Section Cloudant.
  Require Import String.
  Require Import Utils.

  Record cloudant_design :=
      { cloudant_design_inputdb : string;
        cloudant_design_name : string;
        cloudant_design_doc : string; }.
  Record cloudant :=
      { cloudant_designs : list cloudant_design;
        cloudant_final_expr : string;
        cloudant_effective_parameters : list string; }.
End Cloudant.