1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
$ifndef _SMT
$define _SMT
// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
val div = {
ocaml: "quotient",
lem: "integerDiv",
c: "tdiv_int",
coq: "ediv_with_eq"
} : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
overload operator / = {div}
val mod = {
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
coq: "emod_with_eq"
} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
overload operator % = {mod}
val abs_int = {
ocaml: "abs_int",
lem: "abs_int",
c: "abs_int",
coq: "abs_with_eq"
} : forall 'n. int('n) -> int(abs('n))
$ifdef TEST
let __smt_x : int(div(4, 2)) = div(8, 4)
$endif
$endif
|
