aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/specification/lux/abstract/monoid.lux
blob: f6daaa867ceeb197c8baa0248a1a42beb4b681d2 (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
25
26
27
28
29
30
31
32
(.using
 [library
  [lux "*"
   ["_" test {"+" Test}]
   [abstract
    [monad {"+" do}]]
   [math
    ["[0]" random {"+" Random}]]]]
 [\\library
  ["[0]" /
   [//
    [equivalence {"+" Equivalence}]]]])

(def: .public (spec (open "_#[0]") (open "_#[0]") gen_sample)
  (All (_ a) (-> (Equivalence a) (/.Monoid a) (Random a) Test))
  (do random.monad
    [sample gen_sample
     left gen_sample
     mid gen_sample
     right gen_sample]
    (<| (_.for [/.Monoid])
        (all _.and
             (_.test "Left identity."
                     (_#= sample
                          (_#composite _#identity sample)))
             (_.test "Right identity."
                     (_#= sample
                          (_#composite sample _#identity)))
             (_.test "Associativity."
                     (_#= (_#composite left (_#composite mid right))
                          (_#composite (_#composite left mid) right)))
             ))))