quickspec-0.9.6: Equational laws for free!

Safe HaskellNone

Test.QuickSpec.Reasoning.NaiveEquationalReasoning

Description

Equational reasoning built on top of congruence closure.

Documentation

data Context Source

Constructors

Context 

Fields

rel :: S
 
maxDepth :: Int
 
universe :: IntMap Universe
 

type Universe = IntMap [Int]Source

type EQ = ReaderT (Int, IntMap Universe) CCSource

initial :: Int -> [Symbol] -> [Tagged Term] -> ContextSource

createUniverse :: [Term] -> CC UniverseSource

runEQ :: Context -> EQ a -> (a, Context)Source

evalEQ :: Context -> EQ a -> aSource

execEQ :: Context -> EQ a -> ContextSource

liftCC :: CC a -> EQ aSource

(=?=) :: Term -> Term -> EQ BoolSource

equal :: Equation -> EQ BoolSource

(=:=) :: Term -> Term -> EQ BoolSource

unify :: Equation -> EQ BoolSource

type Subst = Symbol -> IntSource

substs :: Term -> IntMap Universe -> Int -> [Subst]Source

subst :: Subst -> Term -> CC IntSource

flatten :: Term -> CC IntSource

get :: EQ SSource

put :: S -> EQ ()Source

rep :: Term -> EQ IntSource