Qcert.Backend.ForeignToJSON

Section ForeignToJSON.


Class foreign_to_JSON {fdata:foreign_data}: Type
  := mk_foreign_to_JSON {
         foreign_to_JSON_to_data
           (j:json) : option foreign_data_type
         ; foreign_to_JSON_from_data
             (fd:foreign_data_type) : json
       }.

End ForeignToJSON.