[Now tests that negative "natural numbers" are never encountered.
Nils Anders Danielsson <nad@cs.chalmers.se>**20050530193039] {
hunk ./Test/ChasingBottoms/Nat/Tests.hs 8
+import Test.ChasingBottoms.SemanticOrd
hunk ./Test/ChasingBottoms/Nat/Tests.hs 17
+import Data.Maybe
hunk ./Test/ChasingBottoms/Nat/Tests.hs 150
+-- Since the implementation is based on Integers I'd like to test that
+-- we can't construct values of the form "Nat i" where i is a negative
+-- Integer. (This can be seen as a test of the observation function
+-- toInteger.)
+
+prop_Nat_closed = [ unary (fromJust . fromSucc)
+                    -- Ord
+                  , binary max
+                  , binary min
+                    -- Enum
+                    -- enumFrom and friends have default definitions.
+                  , unary succ
+                  , unary pred
+                  , unary' toEnum
+                    -- Num
+                  , binary (+)
+                  , binary (-)
+                  , binary (*)
+                  , unary negate
+                  , unary abs
+                  , unary signum
+                  , unary' fromInteger
+                    -- Integral
+                  , binary quot
+                  , binary rem
+                  , binary div
+                  , binary mod
+                  , binary (fst .^^ quotRem)
+                  , binary (snd .^^ quotRem)
+                  , binary (fst .^^ divMod)
+                  , binary (snd .^^ divMod)
+                  ]
+  where
+  ok (n :: Nat) = (toInteger n >= 0) <=! True
+
+  unary (f :: Nat -> Nat) = unary' f
+
+  unary' f =
+    forAll arbitrary $ \x ->
+      ok (f x)
+
+  binary f =
+    forAll arbitrary $ \(m :: Nat) ->
+    forAll arbitrary $ \(n :: Nat) ->
+      ok (f m n)
+
+  f .^^ g = \x y -> f (g x y)
+
hunk ./Test/ChasingBottoms/Nat/Tests.hs 239
+    , prop_Nat_closed
}