Safe Haskell	Safe-Inferred
Language	Haskell2010

Twee.Equation

Contents

Equations.

Description

Equations.

Synopsis

data Equation f = (:=:) {
- eqn_lhs :: !(Term f)
- eqn_rhs :: !(Term f)
}
type EquationOf a = Equation (ConstantOf a)
order :: Function f => Equation f -> Equation f
orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool
bothSides :: (Term f -> Term f') -> Equation f -> Equation f'
trivial :: Eq f => Equation f -> Bool
simplerThan :: Function f => Equation f -> Equation f -> Bool
matchEquation :: Equation f -> Equation f -> Maybe (Subst f)

Equations.

data Equation f Source #

Constructors

(:=:)
Fields eqn_lhs :: !(Term f) eqn_rhs :: !(Term f)

Instances

Instances details

(Labelled f, Show f) => Show (Equation f) Source #
Instance details Defined in Twee.Equation Methods showsPrec :: Int -> Equation f -> ShowS # show :: Equation f -> String # showList :: [Equation f] -> ShowS #
Eq (Equation f) Source #
Instance details Defined in Twee.Equation Methods (==) :: Equation f -> Equation f -> Bool # (/=) :: Equation f -> Equation f -> Bool #
Ord (Equation f) Source #
Instance details Defined in Twee.Equation Methods compare :: Equation f -> Equation f -> Ordering # (<) :: Equation f -> Equation f -> Bool # (<=) :: Equation f -> Equation f -> Bool # (>) :: Equation f -> Equation f -> Bool # (>=) :: Equation f -> Equation f -> Bool # max :: Equation f -> Equation f -> Equation f # min :: Equation f -> Equation f -> Equation f #
(Labelled f, PrettyTerm f) => Pretty (Equation f) Source #
Instance details Defined in Twee.Equation Methods pPrintPrec :: PrettyLevel -> Rational -> Equation f -> Doc # pPrint :: Equation f -> Doc # pPrintList :: PrettyLevel -> [Equation f] -> Doc #
Symbolic (Equation f) Source #
Instance details Defined in Twee.Equation Associated Types type ConstantOf (Equation f) Source # Methods termsDL :: Equation f -> DList (TermListOf (Equation f)) Source # subst_ :: (Var -> BuilderOf (Equation f)) -> Equation f -> Equation f Source #
(Labelled f, Sized f, Weighted f) => Sized (Equation f) Source #
Instance details Defined in Twee.KBO Methods size :: Equation f -> Integer Source #
type ConstantOf (Equation f) Source #
Instance details Defined in Twee.Equation type ConstantOf (Equation f) = f

type EquationOf a = Equation (ConstantOf a) Source #

order :: Function f => Equation f -> Equation f Source #

Order an equation roughly left-to-right, and canonicalise its variables. There is no guarantee that the result is oriented.

orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool Source #

bothSides :: (Term f -> Term f') -> Equation f -> Equation f' Source #

Apply a function to both sides of an equation.

trivial :: Eq f => Equation f -> Bool Source #

Is an equation of the form t = t?

simplerThan :: Function f => Equation f -> Equation f -> Bool Source #

A total order on equations. Equations with lesser terms are smaller.

matchEquation :: Equation f -> Equation f -> Maybe (Subst f) Source #

Match one equation against another.