From aaf8c4941c975899c1aca562ebe4fcb30b224f81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Mon, 24 Jul 2023 18:47:11 +0200
Subject: [PATCH] Add explicit definitions for abs_{real,int}

---
 src/preludes/ria.ae | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
index 0dafe50e5..7b75aedef 100644
--- a/src/preludes/ria.ae
+++ b/src/preludes/ria.ae
@@ -88,6 +88,13 @@ theory Real_of_Int extends RIA =
 
 end
 
+(* Outside of the theories because it is ignored otherwise. *)
+axiom abs_real_def :
+  forall x : real [ abs_real(x) ]. abs_real(x) = if 0.0 <= x then x else -x
+
+axiom abs_int_def :
+  forall x : int [ abs_int(x) ]. abs_int(x) = if 0 <= x then x else -x
+
 theory ABS extends RIA =
 
    axiom abs_real_pos :