diff options
author | Eduardo Julian | 2023-01-04 18:37:14 -0400 |
---|---|---|
committer | Eduardo Julian | 2023-01-04 18:37:14 -0400 |
commit | 3ca054b6b992e2233d763aabc5c938ee10d116a4 (patch) | |
tree | 90b93c5a922fa312331f33cc4c93962c76db4636 /stdlib/source/specification | |
parent | ad1391ea1cdd33167339d25dbff2567f5a8d5c68 (diff) |
Added simple machinery for aliasing of definitions.
Diffstat (limited to 'stdlib/source/specification')
-rw-r--r-- | stdlib/source/specification/lux/abstract/hash.lux | 29 | ||||
-rw-r--r-- | stdlib/source/specification/lux/math/arithmetic.lux | 57 |
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)))) - )))) |