Index of types

A
arith_view [Builtin.ArithOp]
arity_result [Type]
attr [Statement]
attr [UntypedAST]	Attributes
attrs [Statement]
attrs [UntypedAST]
B
builtin [TypedSTerm.Ty]
builtin [Type]
C
c_statement [Cnf]	A statement after CNF
clause [Statement]
clause [Cnf]	Basic clause representation, as list of literals
clause_t [Statement]
combination [Comparison]	Lexicographic combination of comparators.
comparator [Comparison]
comparison [Comparison]
constructor [Ind_ty]	Constructor for an inductive type
ctx [Skolem]	Context needed to create new symbols
ctx [Type.Conv]
ctx [FOTerm.Conv]
D
data [Statement]	A datatype declaration
data [UntypedAST]	Basic definition of inductive types
definition [Skolem]
E
elt [Multiset_intf.S]	Elements of the multiset
elt [Hashcons.S]	Hashconsed objects
elt [Index_intf.TERM_IDX]
elt [Index_intf.LEAF]
env [InnerTerm.DB]
F
f_statement [Cnf]	A statement before CNF
feature_vector [FeatureVector.Make]	a vector of feature
fingerprint_fun [Fingerprint]
fixity [Builtin]
form [UntypedAST]
form [SLiteral]
form [Cnf]
form [Skolem]
from_file [StatementSrc]
G
gen [Util.Flag]	Generator of flags
H
hvar [HVar]
I
input_format [Options]
L
lit [SLiteral]
lit [Cnf]
lits [FeatureVector]
lits [Index_intf]	Sequence of literals, as a cheap abstraction on query clauses
loc [TypeInference]
location [TypedSTerm]
location [STerm]
M
meta_var [TypedSTerm]
N
nat [InnerTerm]
node [LazyList]
O
options [Cnf]	Options are used to tune the behavior of the CNF conversion.
or_error [TypeInference]
or_error [Util]
ordering [Ordering]
P
polarity [Skolem]
position [Position]
precedence [Precedence]
print_format [Options]
print_hook [Interfaces.PRINT_DE_BRUIJN]	User-provided hook that can be used to print terms (for composite cases) before the default printing occurs.
profiler [Util]
R
rhs [Index_intf.UNIT_IDX]	Right hand side of equation
rhs [Index_intf.EQUATION]	An equation can have something other than a term as a right-hand side, for instance a formula.
S
sequence [Unif]
snapshot [TypedSTerm.UStack]	A snapshot of bindings at a given moment
sourced_t [Statement]
stat [Util]
statement [UntypedAST]
statement_view [UntypedAST]	Statement
subst [Index_intf]
subst [Index]
subst [Unif_intf]
subst [Unif]
subst [Substs]
symbol_status [Precedence]
T
t [AllocCache.Arr]	Cache for 'a arrays
t [IArray]	Array of values of type 'a
t [LazyList]
t [Multiset_intf.S]	A multiset of elements of type 'a
t [Hashcons.HashedType]
t [StatementSrc]
t [Statement]
t [TypedSTerm.UStack]	Unification stack, for backtracking purposes
t [TypedSTerm.Subst]
t [TypedSTerm.Form]
t [TypedSTerm.Ty]
t [TypedSTerm]
t [Ind_ty]	An inductive type, along with its set of constructors
t [ParseLocation]
t [FeatureVector.Make.Feature]	a function that computes a given feature on clauses
t [Congruence.TERM]
t [Congruence.S]	Represents a congruence
t [Binder]
t [Index_intf.UNIT_IDX]
t [Index_intf.SUBSUMPTION_IDX]
t [Index_intf.CLAUSE]
t [Index_intf.TERM_IDX]
t [Index_intf.EQUATION]
t [Index_intf.LEAF]
t [SLiteral]
t [IDOrBuiltin]
t [ID]
t [Ordering]	Partial ordering on terms
t [Builtin]
t [Precedence.Constr]	A partial order on symbols, used to make the precedence more precise.
t [Precedence]	Total Ordering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)
t [Comparison.PARTIAL_ORD]
t [Comparison]
t [TypeInference.Ctx]
t [Scoped]
t [Signature]	A signature maps symbols to types
t [Substs.SPECIALIZED]
t [Substs.Renaming]
t [Substs]	A substitution that binds term variables to other terms
t [HVar]
t [Var.Subst]
t [Var.Set]
t [Var]
t [Position.Build]
t [Position]	A position is a path in a tree
t [DBEnv]	An environment that maps De Bruijn indices to values of type 'a.
t [Interfaces.MONOID]
t [Interfaces.ITER]
t [Interfaces.PRINT_DE_BRUIJN]
t [Interfaces.PRINT_OVERLOAD]
t [Interfaces.PRINT3]
t [Interfaces.PRINT2]
t [Interfaces.PRINT1]
t [Interfaces.PRINT]
t [Interfaces.ORD]
t [Interfaces.EQ]
t [STerm]
t [Util.Section]
t [Type]	Type is a subtype of the term structure (itself a subtype of InnerTerm.t), with explicit conversion
t [FOTerm]
t [InnerTerm]	Abstract type of term
term [TypedSTerm]
term [UntypedAST]
term [Congruence.S]
term [Index_intf]
term [Index]
term [SLiteral]
term [Cnf]
term [Skolem]
term [Ordering]
term [Unif_intf.S]
term [Substs.SPECIALIZED]
term [Substs]
term [Interfaces.PRINT_DE_BRUIJN]
term [STerm]
term [FOTerm]
term [InnerTerm]
ty [UntypedAST]
ty [Unif_intf.S]
ty [Type]
type_ [Cnf]
type_ [Skolem]
type_ [TypeInference]
type_result [InnerTerm]
typed [TypeInference]	typed term
typed_statement [TypeInference]
typed_var [STerm]
U
untyped [TypeInference]	untyped term
V
var [Substs]
var [Var]
var [STerm]
var [FOTerm]	Variables are typed with `Type.t`
view [Statement]
view [TypedSTerm.Form]
view [TypedSTerm.Ty]
view [TypedSTerm]
view [STerm]
view [Type]
view [FOTerm.Classic]
view [FOTerm]
view [InnerTerm]
W
weight_fun [Precedence]