Module ForeignToJSON
Require
Import
List
String
.
Require
Import
Utils
ForeignRuntime
.
Require
Import
JSON
.
Local
Open
Scope
string_scope
.
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
.