Module ErgoSpec.Backend.Qcert.QcertTypeToJSON
Require
Import
List
.
Require
Import
ZArith
.
Require
Import
EquivDec
.
Require
Import
RelationClasses
.
Require
Import
Equivalence
.
Require
Import
String
.
Require
Import
Qcert.Utils.Utils
.
Require
Import
Qcert.JSON.JSONSystem
.
Require
Import
Qcert.Data.DataSystem
.
Require
Import
Qcert.Translation.Model.ForeignTypeToJSON
.
Require
Import
QcertData
.
Require
Import
QcertType
.
Program
Instance
enhanced_foreign_type_to_JSON
:
foreign_type_to_JSON
:=
mk_foreign_type_to_JSON
enhanced_foreign_type
_
_
.
Next Obligation.
exact
(
string_to_enhanced_type
s
).
Defined.
Next Obligation.
exact
(
enhanced_type_to_string
fd
).
Defined.