> module NumLaws where
> import NumPrelude
> import NumPrelude as Prelude
> import PreludeBase
> import Prelude as P
> import Debug.QuickCheck
> import NumExtras

Additive laws.

> prop_AddCommutative a b   =       a + b == b + a
> prop_AddAssociative a b c = (a + b) + c == a + (b + c)
> prop_AddIdentity a        =       0 + a == a
> prop_AddInverse a         =    a + (-a) == a

Num laws.

> prop_NumAssociative a b c  = a * (b * c) == (a * b) * c
> prop_NumIdentity a         =       a * 1 == a
> prop_NumDistributive a b c = a * (b + c) == a * b + a * c

This one need not be satisfied by all instances of Num.

> prop_NumCommutative a b    =       a * b == b * a

Integral laws.

> -- prop_NumCommutative and ...
> prop_IntegralDivMod a b      = (a `div` b)*b + (a `mod` b) == a
> prop_IntegralCanonical a b k =           (a + k*b) `mod` b == a `mod` b
> prop_IntegralZero b          =                   0 `mod` b == 0

To do: laws for lattices