quickspec-0.9.2: Equational laws for free

Test.QuickSpec.Reasoning.PartialEquationalReasoning

Description

Equational reasoning that deals with partial functions. Only used in HipSpec at the moment.

data PEquation Source

Constructors

Instances

type Precondition = [Symbol]Source

data Totality Source

showPEquation :: Sig -> PEquation -> StringSource

data Context Source

Fields

type PEQ = State ContextSource

initial :: Int -> [(Symbol, Totality)] -> [Tagged Term] -> ContextSource

runPEQ :: Context -> PEQ a -> (a, Context)Source

evalPEQ :: Context -> PEQ a -> aSource

execPEQ :: Context -> PEQ a -> ContextSource

liftEQ :: [Int] -> (Maybe Int -> EQ a) -> PEQ [a]Source

equal :: PEquation -> PEQ BoolSource

irrelevant :: Equation -> PEQ PreconditionSource

unify :: PEquation -> PEQ BoolSource

precondition :: Equation -> PEQ PreconditionSource

get :: PEQ ContextSource

put :: Context -> PEQ ()Source

rep :: Precondition -> Term -> PEQ [Int]Source