diff options
Diffstat (limited to '')
| -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)))) )))) |