diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/test/lux/abstract/equivalence.lux | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/stdlib/source/test/lux/abstract/equivalence.lux b/stdlib/source/test/lux/abstract/equivalence.lux index 7cc5c95f9..d79803e31 100644 --- a/stdlib/source/test/lux/abstract/equivalence.lux +++ b/stdlib/source/test/lux/abstract/equivalence.lux @@ -1,7 +1,12 @@ (.module: [lux #* ["_" test (#+ Test)] - [abstract/monad (#+ do)] + [abstract + [monad (#+ do)] + {[0 #spec] + [/ + [functor + ["." contravariant]]]}] [data ["." bit ("#@." equivalence)] [number @@ -20,9 +25,20 @@ leftI random.int rightI random.int sample random.nat - different (|> random.nat (random.filter (|>> (n.= sample) not)))] + different (|> random.nat (random.filter (|>> (n.= sample) not))) + #let [equivalence (: (Equivalence (Equivalence Nat)) + (structure + (def: (= left right) + (and (bit@= (:: left = leftN leftN) + (:: right = leftN leftN)) + (bit@= (:: left = rightN rightN) + (:: right = rightN rightN)) + (bit@= (:: left = leftN rightN) + (:: right = leftN rightN))))))]] (<| (_.covering /._) ($_ _.and + (_.with-cover [/.functor] + (contravariant.spec equivalence n.equivalence /.functor)) (_.cover [/.sum] (let [equivalence (/.sum n.equivalence i.equivalence)] (and (bit@= (:: n.equivalence = leftN leftN) |