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
38
39
40
|
$ifndef _SMT
$define _SMT
// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
val div = {
smt: "div",
ocaml: "quotient",
lem: "integerDiv",
c: "tdiv_int",
coq: "ediv_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
overload operator / = {div}
val mod = {
smt: "mod",
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
coq: "emod_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
overload operator % = {mod}
val abs_atom = {
smt : "abs",
ocaml: "abs_int",
lem: "abs_int",
c: "abs_int",
coq: "abs_with_eq"
} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
$ifdef TEST
let __smt_x : atom(div(4, 2)) = div(8, 4)
$endif
$endif
|
