Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Utils.TestHelpers

Contents Algebraic properties Generators Test driver.

Description

Some functions and generators suitable for writing QuickCheck properties.

Synopsis

associative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> a -> Bool commutative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> Bool isZero :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool identity :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool leftDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool rightDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool natural :: Integral i => Gen i positive :: Integral i => Gen i maybeGen :: Gen a -> Gen (Maybe a) maybeCoGen :: (a -> Gen b -> Gen b) -> Maybe a -> Gen b -> Gen b listOfElements :: [a] -> Gen [a] runTests :: String -> [IO Bool] -> IO Bool

Algebraic properties

associative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> a -> Bool Source

Is the operator associative?

commutative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> Bool Source

Is the operator commutative?

isZero :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool Source

Is the element a zero for the operator?

identity :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool Source

Is the element a unit for the operator?

leftDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool Source

Does the first operator distribute (from the left) over the second one?

rightDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool Source

Does the first operator distribute (from the right) over the second one?

Generators

natural :: Integral i => Gen i Source

Generates natural numbers.

positive :: Integral i => Gen i Source

Generates positive numbers.

maybeGen :: Gen a -> Gen (Maybe a) Source

Generates values of Maybe type, using the given generator to generate the contents of the Just constructor.

maybeCoGen :: (a -> Gen b -> Gen b) -> Maybe a -> Gen b -> Gen b Source

Coarbitrary "generator" for Maybe.

listOfElements :: [a] -> Gen [a] Source

Generates a list of elements picked from a given list.

Test driver.

runTests Source

:: String A label for the tests. Used for informational purposes. -> [IO Bool] -> IO Bool Runs the tests, and returns True if all tests were successful.

Produced by Haddock version 2.6.0