From 1567624ec09688b5d17be99fc1cc4f29eea78e45 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Mon, 1 Aug 2011 17:31:20 +0200
Subject: [PATCH] new library arith.mlw: arithmetic for programs

---
 modules/arith.mlw | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 modules/arith.mlw

diff --git a/modules/arith.mlw b/modules/arith.mlw
new file mode 100644
index 000000000..801f1f25b
--- /dev/null
+++ b/modules/arith.mlw
@@ -0,0 +1,29 @@
+
+(* Arithmetic for programs *)
+
+module Int
+
+  use export int.Int
+  use export int.ComputerDivision
+
+  let (/) (x: int) (y:int) = { y <> 0 } div x y { result = div x y }
+
+end
+
+(* machine arithmetic (32-bit integers, etc.) will go here *)
+
+module Real
+
+  use import real.Real
+  use export real.RealInfix
+  use export real.FromInt
+
+  let (/.) (x: real) (y: real) = { y <> 0. } x / y { result = x / y }
+
+end
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C .. modules/arith"
+End:
+*)
-- 
GitLab