diff options
| author | Eduardo Julian | 2022-11-06 20:52:21 -0400 |
|---|---|---|
| committer | Eduardo Julian | 2022-11-06 20:52:21 -0400 |
| commit | ae4c0a4746d59b552ebeba166a43ce756dd265af (patch) | |
| tree | 8548fb3e4a77bd986d459a639ee31cf2455fe20e /stdlib/source/specification | |
| parent | fd8ea1e1b9cae781abe42aeadda2e0ef149994d6 (diff) | |
More efficient code-generation for text composition.
Diffstat (limited to 'stdlib/source/specification')
| -rw-r--r-- | stdlib/source/specification/lux/abstract/enum.lux | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/stdlib/source/specification/lux/abstract/enum.lux b/stdlib/source/specification/lux/abstract/enum.lux index f510a345e..569e67181 100644 --- a/stdlib/source/specification/lux/abstract/enum.lux +++ b/stdlib/source/specification/lux/abstract/enum.lux @@ -8,21 +8,25 @@ [test ["_" property (.only Test)]]]] [\\library - ["[0]" /]]) + ["[0]" /]] + [// + ["[0]S" order]]) -(def .public (spec (open "_#[0]") gen_sample) +(def .public (spec (open "/#[0]") random) (All (_ a) (-> (/.Enum a) (Random a) Test)) (do random.monad - [sample gen_sample] + [sample random] (<| (_.for [/.Enum]) (all _.and - (_.test "Successor and predecessor are inverse functions." - (and (_#= (|> sample _#succ _#pred) + (_.for [/.order] + (orderS.spec /#order random)) + (_.coverage [/.succ /.pred] + (and (/#= (|> sample /#succ /#pred) sample) - (_#= (|> sample _#pred _#succ) + (/#= (|> sample /#pred /#succ) sample) - (not (_#= (_#succ sample) + (not (/#= (/#succ sample) sample)) - (not (_#= (_#pred sample) + (not (/#= (/#pred sample) sample)))) )))) |