-- Copyright (c) 2018 Rudy Matela.
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
--
-- Minimal example of using LeanCheck with Tasty.
import Test.Tasty
import Test.Tasty.LeanCheck as LC
import Data.List
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Test properties checked by LeanCheck"
[ LC.testProperty "sort == sort . reverse" $
\list -> sort (list :: [Int]) == sort (reverse list)
, LC.testProperty "Fermat's little theorem" $
\x -> ((x :: Integer)^7 - x) `mod` 7 == 0
-- the following two properties do not hold
, LC.testProperty "Fermat's last theorem" $
\x y z n ->
(n :: Integer) >= 3 LC.==> x^n + y^n /= (z^n :: Integer)
, LC.testProperty "divMod" $
\x y -> y * (x `div` y) + x `mod` y == (x :: Int)
]