twee-lib-2.3.1: An equational theorem prover
Safe HaskellNone
LanguageHaskell2010

Twee.Equation

Contents

Description

Equations.

Synopsis

Equations.

data Equation f Source #

Constructors

(:=:) 

Fields

Instances

Instances details
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, 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 #

(Labelled f, PrettyTerm f) => Pretty (Equation f) Source # 
Instance details

Defined in Twee.Equation

Symbolic (Equation f) Source # 
Instance details

Defined in Twee.Equation

Associated Types

type ConstantOf (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

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

Order an equation roughly left-to-right. However, 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.

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.