- Removed "lux/math/constructive".

1 files changed, 0 insertions, 58 deletions

diff --git a/stdlib/test/test/lux/math/constructive.lux b/stdlib/test/test/lux/math/constructive.lux
deleted file mode 100644
index 86f8b7360..000000000
--- a/stdlib/test/test/lux/math/constructive.lux
+++ /dev/null
@@ -1,58 +0,0 @@
-(.module:
-  [lux #+ ->]
-  (lux (data text/format)
-       (math ["_" constructive #*])))
-
-(theorem: #export (n/+ [param .Nat] [subject .Nat])
-  .Nat
-  (.n/+ param subject))
-
-(proposition: #export (apply2 f input0 input1 output))
-
-(proposition: #export (commutativity f left right output)
-  (-> (apply2 f left right output)
-      (apply2 f right left output)))
-
-(proof: #export n/+|commutativity
-  (commutativity (~ (@ n/+)))
-  (theorem [@left @right @output]
-           (_ [normal (apply2 (~ (@ n/+)) @left @right @output)])
-           (apply2 (~ (@ n/+)) @right @left @output)
-
-           (axiom "n/+|commutativity")))
-
-(proposition: #export (equality reference sample))
-
-(theorem: #export [t] (is {reference t} {sample t})
-  (Test (equality reference sample))
-  (.if (.is? reference sample)
-    (#_.True (.let [the-axiom (axiom "is")]
-               the-axiom))
-    (#_.False absurdity)))
-
-(proposition: #export (relation2 rel reference sample))
-
-(proposition: #export (reflexivity rel value)
-  (relation2 rel value value))
-
-(proposition: #export (symmetry rel left right)
-  (-> (relation2 rel left right)
-      (relation2 rel right left)))
-
-(proposition: #export (transitivity rel left mid right)
-  (-> [(relation2 rel left mid)
-       (relation2 rel mid right)]
-      (relation2 rel left right)))
-
-(theorem: #export [t0 t1 t2] ($2 {f (-> t0 t1 t2)}
-                                 {input0 t0}
-                                 {input1 t1})
-  [t2 (apply2 f input0 input1 t2)]
-  (.let [output ((? f) (? input0) (? input1))]
-    [output (axiom)]))
-
-(theorem: (can-commute-n/+ {param .Nat} {subject .Nat})
-  .Nat
-  (.let [[output apply2] ((? $2) n/+ param subject)
-         output|commutes! ((? n/+|commutativity) apply2)]
-    output))