Safe Haskell | None |
---|
Documentation
eqF :: [EqLiteral] -> EqFormula
Build a conjunction of literals out of a list of literals
eq :: EqTerm -> EqTerm -> EqLiteral
'eq a b' builds the literal a = b
neq :: EqTerm -> EqTerm -> EqLiteral
'neq a b' builds the literal 'not (a = b)'
var :: Name -> EqTerm
Returns a new variable
fun :: Name -> Arity -> [EqTerm] -> EqTerm
Returns a new function
satisfiableInEq :: EqFormula -> Bool
Returns true if the conjunction of literals given as an argument is satisfiable in the first order theory of uninterpreted functions with equality