Documentation

reserved for rules and equations that were later found to be invalid through testing

should be compatible with compareE

Prints a Thy (theory) on the console. (cf. showThy)

Double-checks a resulting theory moving untrue rules and equations to the invalid list.

As a side-effect of using testing to conjecturing equations, we may get smaller equations that are obviously incorrect when we consider a bigger (harder-to-test) equation that is incorrect.

For example, given an incorrect large equation, it may follow that False=True.

This function can be used to double-check the generated theory. If any equation or rule is discarded, that means the number of tests should probably be increased.

Computes a theory from atomic expressions. Example:

> theoryFromAtoms 5 (const True) (equal preludeInstances 100)
>   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
Thy { rules = [ (x + y) + z == x + (y + z) ]
    , equations = [ y + x == x + y
                  , y + (x + z) == x + (y + z)
                  , z + (x + y) == x + (y + z)
                  , z + (y + x) == x + (y + z) ]
    , canReduceTo = (|>)
    , closureLimit = 2
    , keepE = keepUpToLength 5
    }