Define abs_{real,int} as ites *for external users only*

This is for running benchmarks, do not merge.
OCamlPro · Jul 25, 2023 · f07dfc6 · f07dfc6
1 parent 46077ed
commit f07dfc6
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
@@ -203,3 +203,6 @@ theory ABS extends RIA =
      - i <= x <= i
 
 end
+
+function abs_real(x : real) : real = if 0.0 <= x then x else -x
+function abs_int(x : int) : int = if 0 <= x then x else -x