aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/equivalence.lux
blob: d4c3357944aba0a72bc88fdc9bfeed773f86db52 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(.module:
  [library
   [lux "*"
    ["_" test {"+" [Test]}]
    [abstract
     [monad {"+" [do]}]]
    [math
     ["[0]" random {"+" [Random]}]]]]
  [\\library
   ["[0]" / {"+" [Equivalence]}]])

(def: .public (spec (^open "_//[0]") random)
  (All (_ a) (-> (Equivalence a) (Random a) Test))
  (do random.monad
    [left random
     right random]
    (<| (_.for [/.Equivalence])
        ($_ _.and
            (_.test "Reflexivity."
                    (_//= left left))
            (_.test "Symmetry."
                    (if (_//= left right)
                      (_//= right left)
                      (not (_//= right left))))))))