Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Equations.
Synopsis
- data Equation 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.
Instances
(Labelled f, Show f) => Show (Equation f) Source # | |
Eq (Equation f) Source # | |
Ord (Equation f) Source # | |
(Labelled f, PrettyTerm f) => Pretty (Equation f) Source # | |
Defined in Twee.Equation pPrintPrec :: PrettyLevel -> Rational -> Equation f -> Doc # pPrintList :: PrettyLevel -> [Equation f] -> Doc # | |
Symbolic (Equation f) Source # | |
(Labelled f, Sized f, Weighted f) => Sized (Equation f) Source # | |
type ConstantOf (Equation f) Source # | |
Defined in Twee.Equation |
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.
bothSides :: (Term f -> Term f') -> Equation f -> Equation f' Source #
Apply a function to both sides of an equation.