twee-lib-2.1.1: An equational theorem prover

Safe HaskellNone
LanguageHaskell2010

Twee.Equation

Contents

Description

Equations.

Synopsis

Equations.

data Equation f Source #

Constructors

(:=:) 

Fields

Instances

Eq (Equation f) Source # 

Methods

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

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

Ord (Equation f) Source # 

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) Source # 

Methods

showsPrec :: Int -> Equation f -> ShowS #

show :: Equation f -> String #

showList :: [Equation f] -> ShowS #

PrettyTerm f => Pretty (Equation f) Source # 
Sized f => Sized (Equation f) Source # 

Methods

size :: Equation f -> Int Source #

Symbolic (Equation f) Source # 

Associated Types

type ConstantOf (Equation f) :: * Source #

type ConstantOf (Equation f) Source # 
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?