summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorThomas Bauereiss2017-12-06 17:18:36 +0000
committerThomas Bauereiss2017-12-06 17:18:36 +0000
commit2bc281428a3a1d608d56f69e71b50056a25e3da0 (patch)
treedfd8e8a13702696fd9daef64315952b9652f95e8 /lib
parentc3c3c40a1d4f81448d8356317e88be2b04363df7 (diff)
parent44e9396fa90ab68ee4c8d9674c6bbad6fc851c6d (diff)
Merge remote branch 'experiments' into experiments
Diffstat (limited to 'lib')
-rw-r--r--lib/ocaml_rts/sail_lib.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 3cf4505d..dfdd1db9 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -413,6 +413,8 @@ let real_power (x, y) = Num.power_num x (Num.num_of_big_int y)
let add_real (x, y) = Num.add_num x y
let sub_real (x, y) = Num.sub_num x y
+let abs_real x = Num.abs_num x
+
let lt (x, y) = lt_big_int x y
let gt (x, y) = gt_big_int x y
let lteq (x, y) = le_big_int x y
@@ -422,6 +424,7 @@ let pow2 x = power_big_int_positive_int x 2
let max_int (x, y) = max_big_int x y
let min_int (x, y) = min_big_int x y
+let abs_int x = abs_big_int x
let undefined_real () = Num.num_of_int 0