Twee.Equation

Equations.

Equations.

data Equation f

Constructors

(:=:)

Fields

• eqn_lhs :: !(Term f)
• eqn_rhs :: !(Term f)

Instances

Eq (Equation f)

Defined in Twee.Equation

Methods

(==) :: Equation f -> Equation f -> Bool

(/=) :: Equation f -> Equation f -> Bool

Ord (Equation f)

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

Show (Equation f)

Defined in Twee.Equation

Methods

showsPrec :: Int -> Equation f -> ShowS

show :: Equation f -> String

showList :: [Equation f] -> ShowS

PrettyTerm f => Pretty (Equation f)

Defined in Twee.Equation

Methods

pPrintPrec :: PrettyLevel -> Rational -> Equation f -> Doc

pPrint :: Equation f -> Doc

pPrintList :: PrettyLevel -> [Equation f] -> Doc

Sized f => Sized (Equation f)

Defined in Twee.Equation

Methods

size :: Equation f -> Int

Symbolic (Equation f)

Defined in Twee.Equation

Associated Types

type ConstantOf (Equation f) :: Type

Methods

termsDL :: Equation f -> DList (TermListOf (Equation f))

subst_ :: (Var -> BuilderOf (Equation f)) -> Equation f -> Equation f

type ConstantOf (Equation f)

Defined in Twee.Equation

type ConstantOf (Equation f) = f

type EquationOf a = Equation (ConstantOf a)

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

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'

Apply a function to both sides of an equation.

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

Is an equation of the form t = t?

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