module Number.Peano.Inf.Test
( test
) where
import Number.Peano.Inf
import Test.LazySmallCheck hiding (test)
default (Nat)
test :: IO ()
test = do
smallCheck 10 $
undefined >= (0::Nat)
smallCheck 10 $ \(n::Nat) -> and
[ n + undefined >= n
, n /= infinity ==> (1 + n + undefined) `compare` n == GT
, n `min` (n + undefined) == n
, (1 + n + undefined) `min` n == n
]
smallCheck 10 $ \(m::Nat) (n::Nat) -> and
[ (m + n) `min` (m + undefined) >= m
, (m + undefined) `min` (m + n) >= m
, n `max` (m + undefined) >= m
, (m + undefined) `max` n >= m
]
smallCheck 10 $ and
[ infinity == infinity
, 0 * infinity == 0
, infinity * 0 == 0
]
smallCheck 10 $ \(n::Nat) -> and
[ n /= infinity ==> n < infinity
, n + infinity == infinity
, infinity + n == infinity
, n /= 0 ==> n * infinity == infinity
, n /= 0 ==> infinity * n == infinity
, n /= infinity ==> infinity n == infinity
]