speculate-0.2.0: discovery of properties about Haskell functions

Safe HaskellNone
LanguageHaskell2010

Test.Speculate.Reason

Synopsis

Documentation

data Thy Source #

Constructors

Thy 

Fields

Instances

Eq Thy Source #

This instance is as efficient as it gets, but, this function will not detect equality when rules and equations are in a different order (or repeated). See |==|.

Methods

(==) :: Thy -> Thy -> Bool #

(/=) :: Thy -> Thy -> Bool #

insert :: Equation -> Thy -> Thy Source #

keepMaxOf :: [Equation] -> Expr -> Bool Source #

(|==|) :: Thy -> Thy -> Bool infix 4 Source #

theorize :: [Equation] -> Thy Source #

theorizeBy :: (Expr -> Expr -> Bool) -> [Equation] -> Thy Source #

prettyThy :: (Equation -> Bool) -> Instances -> Thy -> String Source #

append :: Thy -> [Equation] -> Thy Source #

canonicalEqn :: Thy -> Equation -> Bool Source #

canonicalizeEqn :: Thy -> Equation -> Equation Source #

updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy Source #

updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy Source #

finalize :: Thy -> Thy Source #

Finalize a theory by discarding redundant equations. If after finalizing you complete, redundant equations might pop-up again.

initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy Source #

reductions1 :: Expr -> Rule -> [Expr] Source #

reductionsO :: Expr -> Rule -> [Expr] Source #

dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool Source #

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

(|>) :: Expr -> Expr -> Bool infix 4 Source #