diff options
author | Eduardo Julian | 2018-07-03 19:53:11 -0400 |
---|---|---|
committer | Eduardo Julian | 2018-07-03 19:53:11 -0400 |
commit | 56b20b2c3e96f983490c0dbde95634e06fbdf73c (patch) | |
tree | 3000d494d73f0db0d23a728a6e7e609086ebe5e9 /stdlib/test | |
parent | aac5a7796939cd705d955acb616cbff38474606d (diff) |
- Removed "lux/math/constructive".
Diffstat (limited to 'stdlib/test')
-rw-r--r-- | stdlib/test/test/lux/math/constructive.lux | 58 |
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)) |