Module Qcert.Data.Model.Constants
Require
Import
String
.
Require
Import
List
.
Require
Import
Data
.
Require
Import
ForeignData
.
Section
Constants
.
Context
{
fdata
:
foreign_data
}.
Definition
WORLD
:
string
:= "
WORLD
"%
string
.
Definition
mkWorld
(
world
:
list
data
) :
list
(
string
*
data
)
:= (
WORLD
,(
dcoll
world
))::
nil
.
Definition
pd_bindings
:=
list
(
string
*
option
data
).
End
Constants
.