| InnerTerm |
Scoped Terms
|
| FOTerm |
First-order terms
|
| Type |
Types
|
| Util |
Some helpers
|
| STerm |
S-like Terms.
|
| Interfaces |
Interfaces
|
| DBEnv |
De Bruijn environments
|
| Position |
Positions in terms, clauses...
|
| Var |
Variable
|
| HVar |
Hashconsed Variable
|
| Substs |
Substitutions
|
| Unif |
Unification and Matching
|
| Signature |
Signature
|
| Scoped |
Scoped Value
|
| Unif_intf | bind subst v t binds v to t, but fails if v occurs in t
(performs an occur-check first)
|
| TypeInference |
Type Inference
|
| Options |
Global CLI options
|
| Comparison |
Partial Ordering values
|
| Precedence |
Precedence (total ordering) on symbols
|
| Builtin |
Builtin Objects
|
| Ordering |
Term Orderings
|
| Skolem |
Skolem symbols
|
| Cnf |
Reduction to CNF and simplifications
|
| ID |
Unique Identifiers
|
| IDOrBuiltin |
ID or Builtin
|
| SLiteral |
Simple Literal
|
| Index |
Generic term indexing
|
| Index_intf |
Match the indexed terms against the given query term
|
| Dtree |
Perfect Discrimination Tree
|
| Fingerprint |
Fingerprint term indexing
|
| NPDtree |
Non-Perfect Discrimination Tree
|
| Binder |
Binders
|
| Congruence |
Simple and Lightweight Congruence and order
|
| FeatureVector |
Feature Vector indexing
|
| UntypedAST |
Main AST before Typing
|
| Ind_ty |
Inductive Types
|
| TypedSTerm |
Simple Typed Terms.
|
| Statement |
Statement
|
| StatementSrc |
Statement Source
|
| Hashcons |
Hashconsing
|
| ParseLocation |
Location in a file
|
| Multiset |
Generic multisets
|
| LazyList |
Lazy List
|
| IArray |
Immutable Arrays
|
| AllocCache |
Simple Cache for Allocations
|
| Multiset_intf |
Elements of the multiset
|