From f07dfc63c8f7a727d5db774592b0f863a4ecd1d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Tue, 25 Jul 2023 11:48:02 +0200
Subject: [PATCH] Define abs_{real,int} as ites *for external users only*

This is for running benchmarks, do not merge.
---
 src/preludes/ria.ae | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
index 0dafe50e5..9c8b3d69e 100644
--- 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