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.

Summary:
  
Section Cloudant.
  Require Import String.
  Require Import Utils.

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