twee-0.1: An equational theorem prover

Index

!Twee.Array
$$Twee.Pretty, Twee.Base
$+$Twee.Pretty, Twee.Base
&&&Twee.Constraints
:=:Twee.Rule
<+>Twee.Pretty, Twee.Base
<>Twee.Pretty, Twee.Base
addCancellationRuleTwee
addEqualsTwee.Constraints
addExtraRuleTwee
addGoalsTwee
addLessTwee.Constraints
addRuleTwee
addTermTwee.Constraints
allRulesTwee
allSubstTwee.Term, Twee.Base
AndTwee.Constraints
anywhereTwee.Rule
anywhere1Twee.Rule
AppTwee.Term, Twee.Base
appTwee.Term, Twee.Base
ArityTwee.Base
arityTwee.Base
Array 
1 (Type/Class)Twee.Array
2 (Data Constructor)Twee.Array
arrayTwee.Term.Core
arrayContentsTwee.Array
arraySizeTwee.Array
atTwee.Term.Core, Twee.Term, Twee.Base
AtomTwee.Constraints
atomicCancellationTwee
atomsTwee.Constraints
bestTwee
bestCancellationTwee
bothSidesTwee.Rule
boundTwee.Term, Twee.Base
boundListTwee.Term, Twee.Base
bracesTwee.Pretty, Twee.Base
bracketsTwee.Pretty, Twee.Base
Branch 
1 (Type/Class)Twee.Constraints
2 (Data Constructor)Twee.Constraints
branchesTwee.Constraints
BuildTwee.Term, Twee.Base
buildTwee.Term, Twee.Base
Builder 
1 (Type/Class)Twee.Term.Core, Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term.Core
builderTwee.Term, Twee.Base
Builder1Twee.Term.Core
BuilderOfTwee.Base
buildListTwee.Term, Twee.Base
buildTermListTwee.Term.Core
builtTwee.Term.Core
CacheTwee.Label
cacheTwee.Label
CacheState 
1 (Type/Class)Twee.Label
2 (Data Constructor)Twee.Label
CancelTwee
CancellationRule 
1 (Type/Class)Twee
2 (Data Constructor)Twee
cancellationRulesTwee
cancellationsTwee
cancelledWeightTwee
canonicalise 
1 (Function)Twee.Term
2 (Function)Twee.Base
catTwee.Pretty, Twee.Base
charTwee.Pretty, Twee.Base
checkedTwee.Term.Core
childrenTwee.Term, Twee.Base
ChrTwee.Pretty, Twee.Base
closeTwee.Term, Twee.Base
collateTwee.Utils
colonTwee.Pretty, Twee.Base
commaTwee.Pretty, Twee.Base
compareContentsTwee.Term.Core
completeTwee
complete1Twee
conTwee.Term, Twee.Base
conjTwee.Constraints
ConsTwee.Term.Core, Twee.Term, Twee.Base
ConsiderTwee
considerTwee
ConsSymTwee.Term.Core, Twee.Term, Twee.Base
ConstantTwee.Constraints
ConstantOfTwee.Base
contradictoryTwee.Constraints
countTwee
CP 
1 (Type/Class)Twee
2 (Data Constructor)Twee
cpTwee
cpAge1Twee
cpAge2Twee
cpCPTwee
cpIdTwee
CPInfo 
1 (Type/Class)Twee
2 (Data Constructor)Twee
cpOKTwee
CPs 
1 (Type/Class)Twee
2 (Data Constructor)Twee
cpSplitsTwee
cpWeightTwee
cpWeight2Twee
Critical 
1 (Type/Class)Twee
2 (Data Constructor)Twee
criticalTwee
criticalPairsTwee
criticalPairs1Twee
CritInfo 
1 (Type/Class)Twee
2 (Data Constructor)Twee
critInfoTwee
cr_ruleTwee
cr_unifiedTwee
curriedTwee.Pretty, Twee.Base
defTwee.Array
DefaultTwee.Array
DelayTwee
delete 
1 (Function)Twee.Index
2 (Function)Twee.Indexes
deleteCancellationRuleTwee
deleteLabelTwee.Queue
deleteRuleTwee
dequeueTwee.Queue
dequeueMTwee
DischargeTwee
disjTwee.Constraints
DocTwee.Pretty, Twee.Base
doubleTwee.Pretty, Twee.Base
doubleQuotesTwee.Pretty, Twee.Base
easyRulesTwee
Either1Twee.Queue
elemTwee.Index
elems 
1 (Function)Twee.Index
2 (Function)Twee.Indexes
emitFunTwee.Term.Core
emitReplacementTwee
emitSymbolBuilderTwee.Term.Core
emitTermTwee.Term, Twee.Base
emitTermListTwee.Term.Core
emitVarTwee.Term.Core
EmptyTwee.Term.Core, Twee.Term, Twee.Base
empty 
1 (Function)Twee.Pretty, Twee.Base
2 (Function)Twee.Queue
3 (Function)Twee.Indexes
emptyFIFOTwee.Queue
emptyFromTwee.Queue
emptyHeapTwee.Queue
emptyMixTwee.Queue
emptyQueueTwee.Queue
emptySubstTwee.Term, Twee.Base
emptyTermListTwee.Term, Twee.Base
enqueueTwee.Queue
enqueueMTwee
Entry 
1 (Type/Class)Twee.Index
2 (Data Constructor)Twee.Index
eqSameLengthTwee.Term.Core
equals 
1 (Function)Twee.Pretty, Twee.Base
2 (Function)Twee.Constraints
EquationTwee.Rule
EquationOfTwee.Rule
evalSubstTwee.Term, Twee.Base
EventTwee
expandTwee.Index
extendTwee.Term, Twee.Base
ExtendedTwee.Base
extendedTwee.Base
extendListTwee.Term, Twee.Base
ExtraRuleTwee
extraRulesTwee
extraRuleSafeTwee
e_keyTwee.Index
e_valueTwee.Index
falseTwee.Constraints
fcatTwee.Pretty, Twee.Base
FIFO 
1 (Type/Class)Twee.Queue
2 (Data Constructor)Twee.Queue
filterTwee.Index
find 
1 (Function)Twee.Label
2 (Function)Twee.Index
firstTwee.Pretty, Twee.Base
fixedArityTwee.Pretty, Twee.Base
flattenSubstTwee.Term, Twee.Base
floatTwee.Pretty, Twee.Base
foldSubstTwee.Term, Twee.Base
formAndTwee.Constraints
forMSubst_Twee.Term, Twee.Base
FormulaTwee.Constraints
freeze 
1 (Function)Twee.Index
2 (Function)Twee.Indexes
from 
1 (Function)Twee.Label
2 (Function)Twee
fromFunTwee.Term, Twee.Base
fromIntTwee.Term, Twee.Base
fromSymbolTwee.Term.Core
fromTermTwee.Constraints
fromTermListTwee.Term, Twee.Base
Frozen 
1 (Type/Class)Twee.Index
2 (Data Constructor)Twee.Index
fsepTwee.Pretty, Twee.Base
fullRenderTwee.Pretty, Twee.Base
Fun 
1 (Type/Class)Twee.Term.Core, Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term.Core, Twee.Term, Twee.Base
fun 
1 (Function)Twee.Term, Twee.Base
2 (Function)Twee.Index
Function 
1 (Data Constructor)Twee.Base
2 (Type/Class)Twee.Base
FunOfTwee.Base
funs 
1 (Function)Twee.Constraints
2 (Function)Twee.Base
getArrayTwee.Term.Core
getIndexTwee.Term.Core
getMaxTwee.Utils
getMaxWithTwee.Utils
getMinTwee.Utils
getMinWithTwee.Utils
getSizeTwee.Term.Core
goalsTwee
groundJoinTwee
groundJoinableTwee
groundJoinableEqTwee
GroundJoinedTwee
hangTwee.Pretty, Twee.Base
hcatTwee.Pretty, Twee.Base
HeapTwee.Queue
hereTwee.Index
HeuristicTwee.Queue
highTwee.Term.Core
hsepTwee.Pretty, Twee.Base
idempotentTwee.Term, Twee.Base
idempotentOnTwee.Term, Twee.Base
implicitArgumentsTwee.Pretty, Twee.Base
Index 
1 (Type/Class)Twee.Index
2 (Data Constructor)Twee.Index
indexTwee.Term.Core
Indexes 
1 (Type/Class)Twee.Indexes
2 (Data Constructor)Twee.Indexes
infixStyleTwee.Pretty, Twee.Base
infoTwee
InitialTwee
InitialCP 
1 (Type/Class)Twee
2 (Data Constructor)Twee
initialIdTwee.Label
initialStateTwee
insert 
1 (Function)Twee.Queue
2 (Function)Twee.Index
3 (Function)Twee.Indexes
intTwee.Pretty, Twee.Base
integerTwee.Pretty, Twee.Base
interreduceTwee
invisibleTwee.Pretty, Twee.Base
isEmptyTwee.Pretty, Twee.Base
isFun 
1 (Function)Twee.Term.Core
2 (Function)Twee.Term, Twee.Base
isGroundTwee.Base
isInstanceOfTwee.Term, Twee.Base
isMinimalTwee.Base
isSortedTwee.Utils
isSortedByTwee.Utils
isVarTwee.Term, Twee.Base
isVariantOfTwee.Term, Twee.Base
JoinedTwee
JoinReasonTwee
JoinStageTwee
joinStatisticsTwee
keyTwee.Index
l1Twee
l2Twee
Label 
1 (Type/Class)Twee.Queue
2 (Data Constructor)Twee.Queue
label 
1 (Function)Twee.Label
2 (Function)Twee
Labelled 
1 (Type/Class)Twee.Label
2 (Type/Class)Twee.Queue
3 (Data Constructor)Twee.Queue
labelledRulesTwee
labelMTwee.Utils
labelOfTwee.Queue
LabelsTwee.Queue
labelsTwee.Queue
lbraceTwee.Pretty, Twee.Base
lbrackTwee.Pretty, Twee.Base
leftTwee.Queue
Left1Twee.Queue
LeftModeTwee.Pretty, Twee.Base
lenTwee.Term, Twee.Base
lenListTwee.Term.Core, Twee.Term, Twee.Base
LessTwee.Constraints
lessTwee.Constraints
LessEqTwee.Constraints
lessEq 
1 (Function)Twee.Constraints, Twee.Base
2 (Function)Twee.KBO
3 (Function)Twee.LPO
lessEqInModelTwee.Constraints
lessIn 
1 (Function)Twee.Constraints, Twee.Base
2 (Function)Twee.KBO
3 (Function)Twee.LPO
lexLessInTwee.KBO
lhsTwee.Rule
lhsWeightTwee
liftSTTwee.Term.Core
lineLengthTwee.Pretty, Twee.Base
listSubstTwee.Term, Twee.Base
listSubstListTwee.Term, Twee.Base
lookup 
1 (Function)Twee.Term, Twee.Base
2 (Function)Twee.Index
lookupListTwee.Term, Twee.Base
lowTwee.Term.Core
lowerTwee
lparenTwee.Pretty, Twee.Base
ManyCPsTwee
mapTwee.Index
mapFunTwee.Term, Twee.Base
mapFunListTwee.Term, Twee.Base
Match 
1 (Type/Class)Twee.Index
2 (Data Constructor)Twee.Index
matchTwee.Term, Twee.Base
matchesTwee.Index
matchesListTwee.Index
matchesList_Twee.Index
matchListTwee.Term, Twee.Base
matchResultTwee.Index
matchSubstTwee.Index
Max 
1 (Type/Class)Twee.Utils
2 (Data Constructor)Twee.Utils
maxCancellationSizeTwee
maxRatingTwee.Indexes
maxSizeTwee
maybeBracesTwee.Pretty, Twee.Base
maybeBracketsTwee.Pretty, Twee.Base
maybeDoubleQuotesTwee.Pretty, Twee.Base
maybeParensTwee.Pretty, Twee.Base
maybeQuotesTwee.Pretty, Twee.Base
membersTwee.Queue
Min 
1 (Type/Class)Twee.Utils
2 (Data Constructor)Twee.Utils
Minimal 
1 (Type/Class)Twee.Constraints, Twee.Base
2 (Data Constructor)Twee.Base
minimalTwee.Constraints, Twee.Base
minimalTermTwee.Base
minimumCPSetSizeTwee
minimumInTwee.KBO
Mix 
1 (Type/Class)Twee.Queue
2 (Data Constructor)Twee.Queue
mkCacheTwee.Label
MkFunTwee.Term.Core, Twee.Term, Twee.Base
MkVarTwee.Term.Core, Twee.Term, Twee.Base
ModeTwee.Pretty, Twee.Base
modeTwee.Pretty, Twee.Base
Model 
1 (Type/Class)Twee.Constraints
2 (Data Constructor)Twee.Constraints
modelTwee
modelFromOrderTwee.Constraints
Modelled 
1 (Type/Class)Twee
2 (Data Constructor)Twee
modelledTwee
modelToLiteralsTwee.Constraints
moreTracingTwee
moveLabelTwee.Queue
negateFormulaTwee.Constraints
nestTwee.Pretty, Twee.Base
nestedTwee.Rule
newArrayTwee.Array
NewCPTwee
newEquationTwee
newLabelTwee.Queue
newLabelMTwee
NewRuleTwee
nextIdTwee.Label
nextLabelTwee.Queue
NilTwee.Index
noCritInfoTwee
noLabelTwee.Queue
NonstrictTwee.Constraints, Twee.Base
normTwee.Constraints
normalFormsTwee.Rule
normaliseTwee
normaliseCPTwee
normaliseCPQuicklyTwee
normaliseCPReducingTwee
NormaliseCPsTwee
normaliseCPsTwee
normaliseInTwee
normaliseQuicklyTwee
normaliseSkolemTwee
normaliseSubTwee
normaliseWithTwee.Rule
nullTwee.Index
NumberedTwee.Term, Twee.Base
occTwee.Base
occursTwee.Term, Twee.Base
occursListTwee.Term, Twee.Base
OneLineModeTwee.Pretty, Twee.Base
optimiseTwee
OrTwee.Constraints
orderTwee.Rule
OrderedTwee.Constraints, Twee.Base
orElseTwee.Utils
orientTwee.Rule
OrientationTwee.Rule
orientationTwee.Rule
OrientedTwee.Rule
orientedTwee.Rule
orientTermsTwee.Constraints, Twee.Base
overlapTwee
overlapsTwee
PageModeTwee.Pretty, Twee.Base
ParallelTwee.Rule
parensTwee.Pretty, Twee.Base
partitionByTwee.Utils
PassiveTwee
passiveCountTwee
patHeadTwee.Term.Core
patNextTwee.Term.Core
patRootTwee.Term.Core
peelTwee.Queue
PermutativeTwee.Rule
positionsTwee
postfixTwee.Pretty, Twee.Base
pPrintTwee.Pretty, Twee.Base
pPrintListTwee.Pretty, Twee.Base
pPrintParenTwee.Pretty, Twee.Base
pPrintPrecTwee.Pretty, Twee.Base
pPrintReductionTwee.Rule
pPrintRuleTwee.Rule
pPrintSetTwee.Pretty, Twee.Base
pPrintTermTwee.Pretty, Twee.Base
pPrintTupleTwee.Pretty, Twee.Base
prefixTwee.Pretty, Twee.Base
PrettyTwee.Pretty, Twee.Base
PrettyLevel 
1 (Data Constructor)Twee.Pretty, Twee.Base
2 (Type/Class)Twee.Pretty, Twee.Base
prettyNormalTwee.Pretty, Twee.Base
prettyParenTwee.Pretty, Twee.Base
prettyPrintTwee.Pretty, Twee.Base
prettyShowTwee.Pretty, Twee.Base
PrettyTermTwee.Pretty, Twee.Base
processedCPsTwee
properSubtermsTwee.Term, Twee.Base
properSubtermsListTwee.Term, Twee.Base
PStrTwee.Pretty, Twee.Base
ptextTwee.Pretty, Twee.Base
punctuateTwee.Pretty, Twee.Base
putIndexTwee.Term.Core
Queue 
1 (Type/Class)Twee.Queue
2 (Data Constructor)Twee.Queue
queue 
1 (Function)Twee.Queue
2 (Function)Twee
queueCPTwee
queueCPsTwee
queueCPsSplitTwee
queueLabelsTwee.Queue
queueSizeTwee.Queue
quotesTwee.Pretty, Twee.Base
RatedTwee.Indexes
ratingTwee.Indexes
rationalTwee.Pretty, Twee.Base
rbraceTwee.Pretty, Twee.Base
rbrackTwee.Pretty, Twee.Base
ReduceTwee
reduceCPTwee
reduceDocTwee.Pretty, Twee.Base
reducesTwee.Rule
reducesInModelTwee.Rule
reducesSkolemTwee.Rule
reducesSubTwee.Rule
reducesWithTwee.Rule
reduceWithTwee
ReducingTwee
ReductionTwee.Rule
reenqueueTwee.Queue
reenqueueMTwee
reinsertTwee.Queue
removeTwee.Queue
renderTwee.Pretty, Twee.Base
renderStyleTwee.Pretty, Twee.Base
renormaliseAtTwee
renormaliseGoalsTwee
ReorientTwee
repeatMTwee.Utils
replaceTwee.Base
reportTwee
resultTwee.Rule
retractTwee.Term, Twee.Base
rewriteTwee.Rule
rhsTwee.Rule
rhsWeightTwee
ribbonsPerLineTwee.Pretty, Twee.Base
rightTwee.Queue
Right1Twee.Queue
rootTwee.Term.Core
rparenTwee.Pretty, Twee.Base
Rule 
1 (Type/Class)Twee.Rule
2 (Data Constructor)Twee.Rule
ruleTwee.Rule
ruleOverlapsTwee
rulesTwee
rulesForTwee
semiTwee.Pretty, Twee.Base
sepTwee.Pretty, Twee.Base
SetJoiningTwee
Simplification 
1 (Type/Class)Twee
2 (Data Constructor)Twee
simplifiesTwee.Rule
SimplifyTwee
simplifyRuleTwee
SingleCPTwee
SingletonTwee.Index
singleton 
1 (Function)Twee.Term.Core, Twee.Term, Twee.Base
2 (Function)Twee.Index
3 (Function)Twee.Indexes
size 
1 (Function)Twee.Term.Core
2 (Function)Twee.Base
3 (Function)Twee.Index
SizedTwee.Base
sizedTextTwee.Pretty, Twee.Base
sizeLessInTwee.KBO
skipCompositeSuperpositionsTwee
Skolem 
1 (Data Constructor)Twee.Base
2 (Type/Class)Twee.Base
skolemTwee.Base
solveTwee.Constraints
sortBy'Twee.Utils
spaceTwee.Pretty, Twee.Base
StepTwee.Rule
stepsTwee.Rule
StrTwee.Pretty, Twee.Base
StrategyTwee.Rule
StrictTwee.Constraints, Twee.Base
StrictnessTwee.Constraints, Twee.Base
Style 
1 (Data Constructor)Twee.Pretty, Twee.Base
2 (Type/Class)Twee.Pretty, Twee.Base
styleTwee.Pretty, Twee.Base
SubjoiningTwee
Subst 
1 (Type/Class)Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term, Twee.Base
subst 
1 (Function)Twee.Term
2 (Function)Twee.Base
substCompatibleTwee.Term, Twee.Base
substComposeTwee.Term, Twee.Base
SubstitutionTwee.Term, Twee.Base
substListTwee.Term, Twee.Base
SubstOfTwee.Base
substSizeTwee.Term, Twee.Base
substTriTwee.Term, Twee.Base
substUnionTwee.Term, Twee.Base
SubsumedTwee
subtermsTwee.Term, Twee.Base
subtermsListTwee.Term, Twee.Base
supplyTwee.Pretty, Twee.Base
Symbol 
1 (Type/Class)Twee.Term.Core
2 (Data Constructor)Twee.Term.Core
SymbolicTwee.Base
takeLeftTwee.Queue
takeNextTwee.Queue
takeRightTwee.Queue
Term 
1 (Type/Class)Twee.Term.Core, Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term.Core
termTwee.Base
TermList 
1 (Type/Class)Twee.Term.Core, Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term.Core
termlistTwee.Term.Core
TermListOfTwee.Base
termListToListTwee.Term, Twee.Base
TermOfTwee.Base
termsTwee.Base
termsDLTwee.Base
TermStyle 
1 (Type/Class)Twee.Pretty, Twee.Base
2 (Data Constructor)Twee.Pretty, Twee.Base
termStyleTwee.Pretty, Twee.Base
textTwee.Pretty, Twee.Base
TextDetailsTwee.Pretty, Twee.Base
then_Twee.Term.Core
toTwee.Label
toCancellationRuleTwee
toCPTwee
toCPsTwee
toFunTwee.Term, Twee.Base
toIntTwee.Term, Twee.Base
toList 
1 (Function)Twee.Queue
2 (Function)Twee.Array
topTwee
toSymbolTwee.Term.Core
totalCPsTwee
toTermTwee.Constraints
traceTwee
traceIfTwee
traceMTwee
tracingTwee
TransTwee.Rule
TriangleTwee.Term, Twee.Base
TriangleSubstTwee.Term, Twee.Base
TrivialTwee
trivialTwee.Rule
trueTwee.Constraints
trueBranchTwee.Constraints
tryRuleTwee.Rule
tupleStyleTwee.Pretty, Twee.Base
Twee 
1 (Type/Class)Twee
2 (Data Constructor)Twee
unbufferedTwee.Utils
unBuilderTwee.Term.Core
uncurriedTwee.Pretty, Twee.Base
unextendedTwee.Base
unifyTwee.Term, Twee.Base
unifyConstantsInCancellationTwee
unifyListTwee.Term, Twee.Base
unifyListTriTwee.Term, Twee.Base
unifyTriTwee.Term, Twee.Base
unIndexesTwee.Indexes
unionTwee.Index
unlabelledTwee.Queue
unorientTwee.Rule
UnorientedTwee.Rule
UnsafeConsTwee.Term.Core, Twee.Term, Twee.Base
UnsafeConsSymTwee.Term.Core, Twee.Term, Twee.Base
unsafeExtendListTwee.Term, Twee.Base
unsafePatHeadTwee.Term.Core
unSubstTwee.Term, Twee.Base
unTriangleTwee.Term, Twee.Base
updateTwee.Array
upperTwee
useCancellationTwee
useConnectednessTwee
useGeneralSuperpositionsTwee
useGroundJoiningTwee
useInterreductionTwee
useSetJoiningTwee
useSetJoiningForGoalsTwee
useUnsafeInterreductionTwee
usortTwee.Utils
usortByTwee.Utils
usortBy'Twee.Utils
validTwee
valueTwee.Index
Var 
1 (Type/Class)Twee.Term.Core, Twee.Term, Twee.Base
2 (Data Constructor)Twee.Term.Core, Twee.Term, Twee.Base
var 
1 (Function)Twee.Term, Twee.Base
2 (Function)Twee.Index
varGroupsTwee.Constraints
VariableTwee.Constraints
varInModelTwee.Constraints
varsTwee.Base
vcatTwee.Pretty, Twee.Base
weakenModelTwee.Constraints
WeaklyOrientedTwee.Rule
weightTwee
weight'Twee
zeroWidthTextTwee.Pretty, Twee.Base
ZigZagModeTwee.Pretty, Twee.Base
|||Twee.Constraints