summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/arith.sail4
-rw-r--r--lib/smt.sail4
2 files changed, 6 insertions, 2 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index 7c002e1c..6b064433 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -96,7 +96,7 @@ val tmod_int = {
coq: "Z.rem"
} : (int, int) -> nat
-val abs_int = {
+val abs_int_plain = {
smt : "abs",
ocaml: "abs_int",
interpreter: "abs_int",
@@ -105,4 +105,6 @@ val abs_int = {
coq: "Z.abs"
} : int -> int
+overload abs_int = {abs_int_plain}
+
$endif
diff --git a/lib/smt.sail b/lib/smt.sail
index f58c008f..93fe0827 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -20,7 +20,7 @@ val emod_int = {
coq: "emod_with_eq"
} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
-val abs_int = {
+val abs_int_atom = {
ocaml: "abs_int",
interpreter: "abs_int",
lem: "abs_int",
@@ -28,6 +28,8 @@ val abs_int = {
coq: "abs_with_eq"
} : forall 'n. int('n) -> int(abs('n))
+overload abs_int = {abs_int_atom}
+
$ifdef TEST
let __smt_x : int(div(4, 2)) = div(8, 4)