- Removed "lux/math/constructive".

2 files changed, 0 insertions, 257 deletions

diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux
deleted file mode 100644
index 2a904f7cb..000000000
--- a/stdlib/source/lux/math/constructive.lux
+++ /dev/null
@@ -1,199 +0,0 @@
-(.module:
-  [lux #+ ->]
-  (lux (control [monad #+ do]
-                ["p" parser "parser/" Monad<Parser>]
-                ["ex" exception #+ exception:])
-       (data [product]
-             ["e" error]
-             text/format
-             (coll [list "list/" Functor<List>]))
-       (lang [type])
-       (type abstract)
-       [macro]
-       (macro [code]
-              ["s" syntax #+ syntax:]
-              (syntax (common ["scr" reader]
-                              ["scw" writer]))
-              [poly])))
-
-(abstract: #export (Witness t w)
-  {}
-
-  t
-
-  (.def: #export !
-    (.All [t]
-      (.Ex [w]
-        (-> t (Witness t w))))
-    (.|>> :abstraction))
-
-  (.def: #export ?
-    (.All [t w]
-      (-> (Witness t w) t))
-    (.|>> :representation))
-  )
-
-(syntax: #export (@ {name s.symbol})
-  (do @
-    [witnessT (macro.find-type name)]
-    (.case (.<| (poly.run witnessT)
-                poly.apply
-                (p.after (poly.this Witness))
-                (p.after poly.any)
-                poly.any)
-      (#e.Success identityT)
-      (wrap (.list (type.to-code identityT)))
-      
-      (#e.Error error)
-      (macro.fail error))))
-
-(syntax: #export (proof:
-                   {export? scr.export}
-                   {name s.local-symbol}
-                   type
-                   proof)
-  (do @
-    [g!w (macro.gensym "w")]
-    (wrap (.list (.` (.def: (~+ (scw.export export?))
-                       (~ (code.local-symbol name))
-                       (..! (.: (~ type)
-                                (~ proof)))))))))
-
-(.def: type-vars
-  (s.Syntax (.List .Text))
-  (p.default (.list)
-             (s.tuple (p.some s.local-symbol))))
-
-(.type: Input'
-  {#input-name .Text
-   #input-type .Code})
-
-(.type: Input
-  (#Identified Input')
-  (#Anonymous Input'))
-
-(.do-template [<name> <tag> <type>]
-  [(.def: (<name> input)
-     (-> Input <type>)
-     (.case input
-       (#Identified input')
-       (.get@ <tag> input')
-       
-       (#Anonymous input')
-       (.get@ <tag> input')))]
-
-  [input-name #input-name .Text]
-  [input-type #input-type .Code]
-  )
-
-(.def: (identified? input)
-  (-> Input .Bool)
-  (.case input
-    (#Identified input')
-    true
-    
-    (#Anonymous input')
-    false))
-
-(.def: input
-  (s.Syntax Input)
-  (p.alt (s.record (p.seq s.local-symbol s.any))
-         (s.tuple (p.seq s.local-symbol s.any))))
-
-(.def: theorem-declaration
-  (s.Syntax [.Text (.List Input)])
-  (s.form (p.seq s.local-symbol (p.some input))))
-
-(.def: proposition-declaration
-  (s.Syntax [.Text (.List .Text)])
-  (s.form (p.seq s.local-symbol (p.many s.local-symbol))))
-
-(syntax: #export (proposition:
-                   {export? scr.export}
-                   {[name elements] proposition-declaration}
-                   {meaning (p.maybe s.any)})
-  (.case meaning
-    #.None
-    (wrap (.list (.` ((~! abstract:) (~+ (scw.export export?))
-                      ((~ (code.local-symbol name))
-                       (~+ (list/map code.local-symbol elements)))
-
-                      {}
-
-                      .Any))))
-
-    (#.Some meaning)
-    (wrap (.list (.` (.type: (~+ (scw.export export?))
-                       ((~ (code.local-symbol name))
-                        (~+ (list/map code.local-symbol elements)))
-                       (~ meaning)))))))
-
-(.def: (theorem-type type-vars inputs meaning)
-  (-> (.List .Text) (.List Input) .Code .Code)
-  (.let [g!universals (list/map code.local-symbol
-                                type-vars)
-         g!identities (.|> inputs
-                           (list.filter identified?)
-                           (list/map (.|>> input-name code.local-symbol)))
-         g!requisites (list/map (.function (_ input)
-                                  (.case input
-                                    (#Identified input')
-                                    (.` (..Witness (~ (.get@ #input-type input'))
-                                                   (~ (code.local-symbol (input-name input)))))
-                                    
-                                    (#Anonymous input')
-                                    (.get@ #input-type input')))
-                                inputs)]
-    (.` (.All [(~+ g!universals)]
-          (.Ex [(~+ g!identities)]
-            (-> (~+ g!requisites) (~ meaning)))))))
-
-(syntax: #export (axiom {description (p.default "" s.text)})
-  (wrap (.list (.` (.:assume [])))))
-
-(syntax: #export (theorem {type-vars type-vars}
-                          {[name inputs] theorem-declaration}
-                          outputT
-                          meaning)
-  (.let [inputs-names (list/map (.|>> input-name code.local-symbol)
-                                inputs)]
-    (wrap (.list (.` (.: (~ (theorem-type type-vars inputs outputT))
-                         (.function ((~ (code.local-symbol name)) (~+ inputs-names))
-                           (~ meaning))))))))
-
-(.def: (input-code input)
-  (-> Input .Code)
-  (.case input
-    (#Identified [name type])
-    (.` {(~ (code.local-symbol name)) (~ type)})
-    
-    (#Anonymous [name type])
-    (.` [(~ (code.local-symbol name)) (~ type)])))
-
-(syntax: #export (theorem:
-                   {export? scr.export}
-                   {type-vars type-vars}
-                   {[name inputs] theorem-declaration}
-                   outputT
-                   meaning)
-  (wrap (.list (.` (..proof: (~+ (scw.export export?))
-                     (~ (code.local-symbol name))
-                     (~ (theorem-type type-vars inputs outputT))
-                     (..theorem [(~+ (list/map code.local-symbol type-vars))]
-                                ((~ (code.local-symbol name)) (~+ (list/map input-code inputs)))
-                                (~ outputT)
-                                (~ meaning)))))))
-
-(.type: #export (not p)
-  (-> p .Nothing))
-
-(.type: #export (Test p)
-  (#True p)
-  (#False (not p)))
-
-(exception: #export absurd)
-
-(.def: #export absurdity
-  (.All [p] (-> p .Nothing))
-  (.function (_ proof)
-    (.error! (ex.construct absurd []))))
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))