diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 4 | ||||
| -rw-r--r-- | lib/smt.sail | 4 |
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) |
