aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification
diff options
context:
space:
mode:
authorEduardo Julian2023-01-04 18:37:14 -0400
committerEduardo Julian2023-01-04 18:37:14 -0400
commit3ca054b6b992e2233d763aabc5c938ee10d116a4 (patch)
tree90b93c5a922fa312331f33cc4c93962c76db4636 /stdlib/source/specification
parentad1391ea1cdd33167339d25dbff2567f5a8d5c68 (diff)
Added simple machinery for aliasing of definitions.
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r--stdlib/source/specification/lux/abstract/hash.lux29
-rw-r--r--stdlib/source/specification/lux/math/arithmetic.lux57
2 files changed, 0 insertions, 86 deletions
diff --git a/stdlib/source/specification/lux/abstract/hash.lux b/stdlib/source/specification/lux/abstract/hash.lux
deleted file mode 100644
index 28b1c27a2..000000000
--- a/stdlib/source/specification/lux/abstract/hash.lux
+++ /dev/null
@@ -1,29 +0,0 @@
-(.require
- [library
- [lux (.except)
- [abstract
- [monad (.only do)]
- ["[0]" equivalence
- ["[1]T" \\test]]]
- [math
- ["[0]" random (.only Random)]
- [number
- ["n" nat]]]
- [test
- ["_" property (.only Test)]]]]
- [\\library
- ["[0]" /]])
-
-(def .public (spec (open "/#[0]") random)
- (All (_ a) (-> (/.Hash a) (Random a) Test))
- (do random.monad
- [parameter random
- subject random]
- (all _.and
- (_.for [/.equivalence]
- (equivalenceT.spec /#equivalence random))
- (_.coverage [/.Hash /.hash]
- (if (/#= parameter subject)
- (n.= (/#hash parameter) (/#hash subject))
- true))
- )))
diff --git a/stdlib/source/specification/lux/math/arithmetic.lux b/stdlib/source/specification/lux/math/arithmetic.lux
deleted file mode 100644
index 1c13f52f5..000000000
--- a/stdlib/source/specification/lux/math/arithmetic.lux
+++ /dev/null
@@ -1,57 +0,0 @@
-(.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 [@0 (- any any)
- non_zero (random.only (|>> (= @0) not)
- random)]
- any non_zero
- .let [@1 (/ any any)
- @2 (+ @1 @1)
- @4 (+ @2 @2)
- @8 (+ @4 @4)
-
- power_of_two (all random.either
- (in @1)
- (in @2)
- (in @4)
- (in @8)
- )]
- left power_of_two
- right power_of_two]
- (<| (_.covering /._)
- (_.for [/.Arithmetic])
- (all _.and
- (_.coverage [/.+ /.-]
- (and (|> left (+ right) (- right) (= left))
- (|> left (- right) (+ right) (= left))
-
- (|> left (+ @0) (= left))
- (|> left (- @0) (= left))
-
- (|> left (- left) (= @0))))
- (_.coverage [/.* /./]
- (and (|> left (* @0) (= @0))
-
- (|> left (* @1) (= left))
- (|> left (/ @1) (= left))
-
- (|> left (/ left) (= @1))
-
- (|> left (* @2) (/ @2) (= left))))
- ))))