diff options
author | Eduardo Julian | 2022-03-01 02:29:52 -0400 |
---|---|---|
committer | Eduardo Julian | 2022-03-01 02:29:52 -0400 |
commit | 8023df0f5dae4638021fef7b8194a3d0a16b32e4 (patch) | |
tree | 8d64ad88decb0832d85b46a9ef7e734e6b816c35 /stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux | |
parent | 62436b809630ecd3e40bd6e2b45a8870a2866934 (diff) |
Still more fixes for JVM interop.
Diffstat (limited to '')
-rw-r--r-- | stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux b/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux new file mode 100644 index 000000000..3dccec159 --- /dev/null +++ b/stdlib/source/test/lux/tool/compiler/language/lux/synthesis/side.lux @@ -0,0 +1,43 @@ +(.using + [library + [lux "*" + ["_" test {"+" Test}] + [abstract + [monad {"+" do}] + [\\specification + ["$[0]" equivalence] + ["$[0]" hash]]] + [data + ["[0]" bit ("[1]#[0]" equivalence)] + ["[0]" text ("[1]#[0]" equivalence)]] + [math + ["[0]" random {"+" Random}] + [number + ["n" nat]]]]] + [\\library + ["[0]" /]]) + +(def: .public random + (Random /.Side) + ($_ random.and + random.nat + random.bit + )) + +(def: .public test + Test + (<| (_.covering /._) + (_.for [/.Side]) + (do [! random.monad] + [left ..random + right ..random] + ($_ _.and + (_.for [/.equivalence] + ($equivalence.spec /.equivalence ..random)) + (_.for [/.hash] + ($hash.spec /.hash ..random)) + + (_.cover [/.format] + (bit#= (# /.equivalence = left right) + (text#= (/.format left) (/.format right)))) + )))) |