Qcert.Translation.ForeignToCloudant

Section ForeigntoCloudant.

  Class foreign_to_cloudant
        {fruntime:foreign_runtime}
        {fredop:foreign_reduce_op} : Type
  := mk_foreign_to_cloudant {
         foreign_to_cloudant_reduce_op
           (rop:foreign_reduce_op_type)
         : cld_reduce_op
         ; foreign_to_cloudant_prepare_nnrcmr :
             nnrcmr → nnrcmr
         ; foreign_to_cloudant_nnrcmr_prepared :
             nnrcmr → Prop
         ; foreign_to_cloudant_prepare_nnrcmr_prepares (src:nnrcmr) :
             foreign_to_cloudant_nnrcmr_prepared
               (foreign_to_cloudant_prepare_nnrcmr src)
       }.

End ForeigntoCloudant.