(.using
 [library
  [lux (.except)
   ["_" test (.only Test)]
   ["[0]" static]
   [math
    [number
     ["n" nat]]]]]
 [\\library
  ["[0]" / (.only)
   ["/[1]" //]]])

(with_expansions [<nat> (static.random_nat)]
  (/.export:
    (def: nullary
      Nat
      <nat>)
    (def: unary
      (-> Nat Nat)
      (|>> (n.+ <nat>)))
    (def: CONSTANT
      Nat
      <nat>)
    (def: $global
      (-> Nat Nat)
      (|>> (n.+ <nat>))))

  (//.import: (nullary [] Nat))
  (//.import: (unary [Nat] Nat))
  (//.import: (CONSTANT Nat))
  (//.import: ($global (-> Nat Nat)))

  (def: .public test
    Test
    (<| (_.covering /._)
        (all _.and
             (_.coverage [/.export:]
               (and (n.= <nat> (..nullary []))
                    (n.= (n.+ <nat> <nat>) (..unary <nat>))
                    (n.= <nat> (..CONSTANT))
                    (n.= (n.+ <nat> <nat>) ((..$global) <nat>))))
             )))
  )