max expr size = 5 |- on ineqs = 4 |- on conds = 4 max #-tests = 500 min #-tests = 25 (to consider p ==> q true) max #-vars = 2 (for inequational and conditional laws) _ :: Int _ :: [Int] _ :: Int -> [Int] return :: Int -> [Int] (>>=) :: [Int] -> (Int -> [Int]) -> [Int] (>=>) :: (Int -> [Int]) -> (Int -> [Int]) -> Int -> [Int] (xs >>= return) == xs f x == (return x >>= f) (f x >>= g) == (f >=> g) x ((xs >>= f) >>= g) == (xs >>= (f >=> g)) (f >=> return) == f (return >=> f) == f ((f >=> g) >=> h) == (f >=> (g >=> h))