(.require
 [library
  [lux (.except)
   [abstract
    [monad (.only do)]]
   [math
    ["[0]" random (.only Random)]
    [number
     ["n" nat]]]
   [meta
    ["[0]" static]
    ["[0]" code]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" /]])

(with_expansions [<before> (static.random_nat)
                  <after> (static.random code.nat
                                         (random.only (|>> (n.= <before>) not) random.nat))]
  (def my_global
    Nat
    <before>)

  (/.with [..my_global <after>]
    (def my_local
      Nat
      (n.+ my_global my_global)))

  (def .public test
    Test
    (<| (_.covering /._)
        (do [! random.monad]
          [])
        (all _.and
             (_.coverage [/.with]
               (and (n.= (n.+ <after> <after>) my_local)
                    (not (n.= (n.+ <before> <before>) my_local))))
             )))
  )