speculate-0.4.1: discovery of properties about Haskell functions

Copyright(c) 2016-2019 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellNone
LanguageHaskell2010

Test.Speculate.Reason

Description

This module is part of Speculate.

Equational reasoning for Exprs based on term rewriting.

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 |==|.

Instance details

Defined in Test.Speculate.Reason

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 #

finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation] 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 #

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 #