1 files changed, 46 insertions, 0 deletions
diff --git a/stdlib/source/specification/lux/math/arithmetic.lux b/stdlib/source/specification/lux/math/arithmetic.lux
new file mode 100644
index 000000000..7ae9f3f06
--- /dev/null
+++ b/stdlib/source/specification/lux/math/arithmetic.lux
@@ -0,0 +1,46 @@
+(.require
+ [library
+  [lux (.except)
+   [abstract
+    [equivalence (.only Equivalence)]
+    [monad (.only do)]]
+   [math
+    ["[0]" random (.only Random)]]
+   [test
+    ["_" property (.only Test)]]]]
+ [\\library
+  ["[0]" /]])
+
+(def .public (spec (open "[0]") (open "[0]") random)
+  (All (_ of)
+    (-> (Equivalence of) (/.Arithmetic of) (Random of)
+        Test))
+  (do random.monad
+    [any random
+     .let [zero (- any any)
+           non_zero (random.only (|>> (= zero) not)
+                                 random)]
+     left non_zero
+     right non_zero
+     .let [one (/ right right)]]
+    (<| (_.covering /._)
+        (_.for [/.Arithmetic])
+        (all _.and
+             (_.coverage [/.+ /.-]
+               (and (|> left (+ right) (- right) (= left))
+                    (|> left (- right) (+ right) (= left))
+                    (|> left (+ zero) (= left))
+                    (|> left (- zero) (= left))
+                    (|> left (- left) (= zero))))
+             (_.coverage [/.* /./]
+               (and (|> left (* right) (/ right) (= left))
+                    (|> left (* one) (= left))
+                    (|> left (/ one) (= left))
+                    (|> left (/ left) (= one))
+                    (|> left (* zero) (= zero))))
+             (_.coverage [/.%]
+               (let [rem (% left right)
+                     div (|> right (- rem) (/ left))]
+                 (= right
+                    (|> div (* left) (+ rem)))))
+             ))))