Index of modules


A
AC [FOTerm]
AllocCache
Simple Cache for Allocations
Arith [Builtin]
Arith [FOTerm]
ArithOp [Builtin]
Arr [AllocCache]

B
BasicEquation [Index]
Binder
Binders
Build [Position]
Builtin
Builtin Objects

C
C [Index_intf.SUBSUMPTION_IDX]
Classic [FOTerm]
Classic view
Cnf
Reduction to CNF and simplifications
Comparison
Partial Ordering values
Congruence
Simple and Lightweight Congruence and order
Constr [Precedence]
Constraints
Conv [Type]
Conv [FOTerm]
Ctx [TypeInference]

D
DB [InnerTerm]
DBEnv
De Bruijn environments
Default [Dtree]
Dtree
Perfect Discrimination Tree

E
E [Index_intf.UNIT_IDX]
Module that describes indexed equations
Exn [Util]

F
FO [Congruence]
FO [Unif]
FO [Substs]
FOTerm
First-order terms
Feature [FeatureVector.Make]
FeatureVector
Feature Vector indexing
Fingerprint
Fingerprint term indexing
Flag [Util]
Form [TypedSTerm]

H
HVar
Hashconsed Variable
Hashcons
Hashconsing

I
IArray
Immutable Arrays
ID
Unique Identifiers
IDOrBuiltin
ID or Builtin
Ind_ty
Inductive Types
Index
Generic term indexing
Index_intf
Match the indexed terms against the given query term
Inner [Unif]
To be used only on terms without InnerTerm.Multiset constructor
InnerTerm
Scoped Terms
Interfaces
Interfaces

L
LazyList
Lazy List
Leaf [Index_intf.TERM_IDX]
Loc [UntypedAST]

M
Make [Multiset]
Make [Hashcons]
Make [FeatureVector]
Make [Congruence]
Make [NPDtree]
Make [Fingerprint]
Make [Dtree]
MakeLeaf [Index]
MakeNonWeak [Hashcons]
Version that uses a regular Hashtbl, rather than a weak table.
MakeTerm [NPDtree]
Map [TypedSTerm]
Map [ID]
Map [Builtin]
Map [STerm]
Map [Type]
Map [FOTerm]
Map [InnerTerm]
Multiset
Generic multisets
Multiset_intf
Elements of the multiset

N
NPDtree
Non-Perfect Discrimination Tree

O
Options
Global CLI options
Ordering
Term Orderings

P
ParseLocation
Location in a file
Pos [FOTerm]
Pos [InnerTerm]
Position
Positions in terms, clauses...
Precedence
Precedence (total ordering) on symbols

R
Renaming [Substs]

S
SLiteral
Simple Literal
STerm
S-like Terms.
Scoped
Scoped Value
Section [Util]
Debug section
Seq [IArray]
Seq [Multiset_intf.S]
Seq [TypedSTerm]
Seq [Precedence]
Seq [Signature]
Seq [STerm]
Seq [Type]
Seq [FOTerm]
Seq [InnerTerm]
Set [TypedSTerm]
Set [ID]
Set [Builtin]
Set [Var]
Set [STerm]
Set [Type]
Set [FOTerm]
Set [InnerTerm]
Signature
Signature
Skolem
Skolem symbols
Statement
Statement
StatementSrc
Statement Source
StringSet [STerm]
Subst [TypedSTerm]
Subst [Var]
Substs
Substitutions

T
T [UntypedAST]
TPTP [TypedSTerm]
TPTP [Binder]
TPTP [SLiteral]
TPTP [Builtin]
TPTP [STerm]
TPTP [Type]
TPTP [FOTerm]
Tbl [TypedSTerm]
Tbl [ID]
Tbl [Builtin]
Tbl [STerm]
Tbl [Type]
Tbl [FOTerm]
Tbl [InnerTerm]
Ty [TypedSTerm]
Ty [Unif]
Ty [Substs]
TyBuiltin [TypeInference]
Type
Types
TypeInference
Type Inference
TypedSTerm
Simple Typed Terms.

U
UStack [TypedSTerm]
Unif
Unification and Matching
Unif_intf
bind subst v t binds v to t, but fails if v occurs in t (performs an occur-check first)
UntypedAST
Main AST before Typing
Util
Some helpers

V
Var
Variable
VarMap [Type]
VarMap [FOTerm]
VarMap [InnerTerm]
VarSet [Type]
VarSet [FOTerm]
VarSet [InnerTerm]
VarTbl [Type]
VarTbl [FOTerm]
VarTbl [InnerTerm]

Z
ZF [TypedSTerm]
ZF [Binder]
ZF [SLiteral]
ZF [Builtin]
ZF [STerm]