Twee.Rule

data Rule f

data Orientation f

oriented

pPrintRule

data Equation f

type EquationOf a

order

unorient

orient

rule

bothSides

trivial

type Strategy f

data Reduction f

result

pPrintReduction

steps

anywhere1

normaliseWith

normalForms

anywhere

nested

rewrite

tryRule

simplifies

reducesWith

reduces

reducesInModel

reducesSkolem

reducesSub