Module Time
Require
Import
String
.
Require
Import
AST_source
.
Class
Size
(
A
:
Type
) :=
size
:
A
->
BinInt.Z
.
Definition
time
{
A
B
:
Type
} (
category
:
option
string
) (
name
:
string
) (
f
:
A
->
B
) :
A
->
B
:=
f
.
Definition
set_function_ident
{
A
B
:
Type
} (
i
:
ident
) (
f
:
A
->
B
) :=
f
.
Definition
set_function_type
{
A
B
C
} {
size
:
Size
A
} (
fd
:
fundef
A
) (
f
:
B
->
C
) :=
f
.
Axiom
assert_false
:
forall
{
A
},
A
.