From 7bf9b460d3b2c324b4fae8e14e0a54e354002f54 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 25 Mar 2020 20:40:59 +0000
Subject: Add Lem builtins for operations on reals

... that match the names in lib/real.sail.

Also fix the lem mapping for abs_int_atom and a Lem syntax error with
nested record updates.
---
 lib/smt.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index 93fe0827..2e72e791 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -23,7 +23,7 @@ val emod_int = {
 val abs_int_atom = {
   ocaml: "abs_int",
   interpreter: "abs_int",
-  lem: "abs_int",
+  lem: "integerAbs",
   c: "abs_int",
   coq: "abs_with_eq"
 } : forall 'n. int('n) -> int(abs('n))
-- 
cgit v1.2.3