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.