lean: add support for int_mult (#752)

rems-project · Oct 30, 2024 · 9e228eb · 9e228eb
1 parent 262cab4
commit 9e228eb
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 3 deletions.
diff --git a/lib/arith.sail b/lib/arith.sail
@@ -87,7 +87,7 @@ overload negate = {negate_atom, negate_int}
 val mult_atom = pure {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul", _: "mult_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n * 'm)
 
-val mult_int = pure {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul", _: "mult_int"} : (int, int) -> int
+val mult_int = pure {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul", lean: "Int.mul", _: "mult_int"} : (int, int) -> int
 
 overload operator * = {mult_atom, mult_int}
 

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -1,6 +1,9 @@
-def foo : Int :=
+def extern_negate : Int :=
   (Int.neg 5)
 
+def extern_mult : Int :=
+  (Int.mul 5 4)
+
 def initialize_registers : Unit :=
   ()
 
diff --git a/test/lean/extern.sail b/test/lean/extern.sail
@@ -2,7 +2,11 @@ default Order dec
 
 $include <prelude.sail>
 
-function foo() -> int = {
+function extern_negate() -> int = {
   return negate_int(5)
 }
 
+function extern_mult() -> int = {
+  return mult_int(5, 4)
+}
+