Index of types

A
apply_error [TermInner.UTIL]
apply_error [TermInner.Util]
atom [FO_rel]
atom_name [FO_rel]
attempt_stack [TypeInference]	a trace of inference attempts with a message and optional location for each attempt.
attr [FO]
attribute [UntypedAST]	one attribute = list of strings separated by spaces
axiom [Statement]	Flavour of axiom
B
binop [FO_rel]
build [TermInner]	A builder for a concrete representation with type `'t`.
C
cache [AnalyzeType.Make]	Cache for memoizing cardinality computations
callback_id [Utils.Callback]	The unique identifier of a given callback (for removal)
case [TermInner]	A pattern match case for a given constructor `vars, right-hand side` The pattern must be linear (variable list does not contain duplicates)
case [Model.DT]
cases [TermInner]	A list of cases (indexed by constructor)
cases [Model.DT]
cell [Lazy_list]
check_res [Transform.Features]
constructor [FO]
copy [Statement]
copy [UntypedAST]
copy_wrt [Statement]
copy_wrt [UntypedAST]
cstor [Tip_ast]
D
decl [FO_rel]
decl_attr [Statement]	Attribute on declarations
decode_state [Elim_infinite]
decode_state [ElimData.S]
decode_state [Unroll]
decode_state [Polarize]
decode_state [ElimCopy]
decode_state [ElimIndPreds]
decode_state [ElimRecursion]
decode_state [Elim_HOF]
decode_state [Specialize]	Used to decode
def [Env]
defined [Statement]
dispatch [Traversal.Make]
dt [Model.DT_util]
E
entry [Tip_ast.Smbc_res]
env [TypeInference.Convert]
env [AnalyzeType.Make]	We only consider monomorphic types
equations [Statement]
expr [FO_rel]
F
final_state [Scheduling.Fut]
flat_dt [Model.DT]	A flat model
flat_test [Model.DT]	A test for the flat model
form [TPTP_lexer]
form [TPTP_print]
form [FO_rel]
form [FO_tptp]
fun_decl [Tip_ast]
fun_def [Tip_ast]
funs_rec_def [Tip_ast]
G
gen [Sexp_lib]
gen [Lazy_list]
general_data [UntypedAST.TPTP]
guard [TermInner.Builtin]
I
id [TypeInference]
id [TPTP_model_ast]
id [TypeMono]
id [TypePoly]
id [Pattern]
id [TermMono]
id [TermTyped]
id [TermInner]
id [Statement]
id [Signature]
id [Env]
id [FO]
id [Problem]
id [MetaVar]
id [Var]
include_mode [Parsing_utils]
info [Statement]	Additional informations on the statement
info [Env]	All information on a given symbol
info [Problem.Res]
inner [Transform]	Transformation with explicit hidden state
int_expr [FO_rel]
int_op [FO_rel]
inv [Problem.Convert]
K
key [Transform.Features]
L
loc [TypeInference]
loc [TermTyped]
loc [Statement]
loc [Env]
loc [Problem]
M
match_branch [Tip_ast]
meta_vars_set [TypeUnify.Make]
metadata [FO]
metadata [Problem]
mode [ElimData]
mode [ElimPatternMatch]	Mode of operations: which matches should be removed?
mode [Skolem]
model [Elim_prop_args]
model [Model_clean]
model [Tip_ast.Smbc_res]
model [Ast_kodkod]
model [TPTP_print]
model [Model]
model1 [FoToRelational]
model2 [FoToRelational]
mult [FO_rel]	multiplicity
mutual_preds [UntypedAST]
mutual_types [Statement]	Mutual definitions of several types
mutual_types [FO]
mutual_types [UntypedAST]
N
name [TPTP_model_ast]
O
on_res_callback [Scheduling.Fut]	callback executed once a future is done
or_error [TypeInference]
or_error [Parse_tip]
or_error [TPTP_preprocess]
or_error [Parsing_utils]
or_error [TermInner]
or_error [Sexp_lib]
or_error [Scheduling]
or_error [FO]
or_error [Problem]
or_error [Utils]
P
parse_result [Sexp_lib]	A parser of `'a` can return `Ok x when it parsed a value, or `Error e when a parse error was encountered, or `End if the input was empty
parser_ [Parsing_utils.PARSER]
prec [TermInner]
prec_printer [Model]
pred_clause [Statement]
pred_def [Statement]
print [TermInner]
printer [TPTP_print]
printer [TypeMono]
printer [TypePoly]
printer [TermInner]
printer [Statement]
printer [Env]
printer [FO]
printer [Problem]
printer [Model]
printer [Transform]
problem [Elim_ite]
problem [Elim_prop_args]
problem [TypeInference.Convert]
problem [FO_rel]
problem [FO_tptp]
problem1 [FoToRelational]
problem2 [FoToRelational]
process_status [Scheduling]
R
rec_def [Statement]
rec_defs [Statement]
rec_defs [UntypedAST]
relation [Ast_kodkod]
renaming [TermInner.UTIL]
renaming [TermInner.Util]
repr [TermInner]	A concrete representation of terms by the type `'t`
res [Elim_prop_args]
res [FO]
result [Ast_kodkod]
role [FO_tptp]
run_result [Scheduling]
S
section [Ast_kodkod]
sequence [Sexp_lib]
sequence [TypeUnify]
sequence [Utils]
sexp [Sexp_lib]
shortcut [Scheduling]
signature [TermInner.UTIL]	A signature is a way to obtain the type of a variable
signature [TermInner.Util]
spec_defs [Statement]
spec_defs [UntypedAST]
state [FoToRelational]
state [Elim_prop_args]
state [ElimTypes]
state [LambdaLift]
state [Skolem]
state [ID.Erase]
statement [TypeInference.Convert]
statement [Tip_ast]
statement [TPTP_model_ast]
statement [Parsing_utils]
statement [FO_tptp]
statement [Statement]
statement [FO]	Statement
statement [UntypedAST]
statement_node [UntypedAST]
stmt [Tip_ast]
sub_universe [FO_rel]
subst [TermInner.UTIL]
subst [TermInner.Util]
subst [Reduce.Make]
subst [Model.DT_util]
symbol_kind [Model]
T
t [Tip_ast.Smbc_res]
t [Pattern.S]
t [Pattern.Make]
t [Pattern.Builtin]
t [TermMono.S]
t [TermMono.OfFO]
t [TermMono.Make]
t [TermMono.Binder]
t [TermTyped.S]
t [TermTyped.BUILD]
t [TermTyped.REPR]
t [TermTyped.Default]
t [TermTyped.Util]
t [TermTyped.LiftRepr]
t [TermInner.PRINT]
t [TermInner.S]
t [TermInner.BUILD]
t [TermInner.REPR]
t [TermInner.Default]
t [TermInner.Print]
t [TermInner.Builtin]
t [TermInner.TyBuiltin]
t [TermInner.Binder]
t [Sexp_lib.Decoder]	Decoder
t [Sexp_lib]
t [Lazy_list]
t [TypeCheck.Make]
t [ProblemMetadata]
t [Traversal.ARG]
t [Traversal.Make]	A stateful object used for traversing a problem, eventually building a new list of statements
t [Polarity]
t [Scheduling.Task]	Task returning a value of type `'res` when executed
t [Scheduling.Fut]
t [Scheduling.MVar]
t [Cardinality.Z]
t [Cardinality]
t [Statement]
t [Signature]
t [Env]	Maps ID to their type and definitions
t [FO.Problem]
t [FO.T]
t [FO.Ty]
t [FO.Builtin]
t [FO.TyBuiltin]
t [Problem.Res]
t [Problem]
t [Model.Default]
t [Model.DT]
t [Model]	A model
t [UntypedAST.Builtin]
t [Transform.Pipe]	Composite transformation from `'a` to `'b`, with a reverse transformation from `'c` to `'d`
t [Transform.Features]
t [Transform]	Transformation of `'a` to `'b`, with reverse transformation from `'c` to `'d`.
t [Utils.Callback]	Set of callbacks where callbacks have type `'a`
t [Utils.Section]
t [Intf.PRINT]
t [Intf.HASH]
t [Intf.ORD]
t [Intf.EQ]
t [Location]
t [MetaVar]	Pointer to another type
t [Var.Subst]	A substitution for variables of type `'ty`, to terms `'a`
t [Var]
t [ID]
t_ [TermInner.UTIL_REPR]
t_ [TermInner.UtilRepr]
tasks_bag [Scheduling.Fut]	internal type for a list of tasks to run
term [Elim_infinite]
term [Elim_ite]
term [Elim_prop_args]
term [ElimTypes]
term [ElimData]
term [Model_clean]
term [IntroGuards]
term [Unroll]
term [Polarize]
term [ElimCopy]
term [ElimIndPreds]
term [ElimMultipleEqns]
term [ElimRecursion]
term [Elim_HOF]
term [LambdaLift]
term [Specialize]
term [Monomorphization]
term [ElimPatternMatch]
term [TypeInference.Convert]
term [Skolem]
term [Tip_ast]	AST: S-expressions with locations
term [TPTP_model_ast]
term [TPTP_print]
term [Parsing_utils]
term [Traversal.Make]
term [FO_tptp]
term [Env.Util]
term [Model.Default]
term [Model.DT_util]
term [UntypedAST]
term1 [TypeInference.Make]
term2 [TypeInference.Make]
term_node [UntypedAST]
timer [Utils.Time]	A single-use timer, measures elapsed time between `start_timer()` and first call to `Utils.Time.stop_timer`
to_sexp [Problem]
to_sexp [Model]
token [Tip_parser]
token [Parse_kodkod]
token [TPTP_model_parser]
token [TPTP_parser]
token [Parser]
token [Parsing_utils.PARSER]
token [Sexp_lex]
toplevel_ty [FO.Ty]
toplevel_ty [FO]	Toplevel type: an arrow of atomic types
transformation [Transform]	Alias to `Transform.t`
tuple [FO_rel]
tuple_set [FO_rel]
ty [Elim_ite]
ty [Elim_prop_args]
ty [ElimCopy]
ty [Specialize]
ty [Tip_ast]	Polymorphic types
ty [TPTP_print]
ty [Parsing_utils]
ty [AnalyzeType.Make]
ty [Traversal.Make]
ty [FO_tptp]
ty [Env.Util]
ty [UntypedAST]
ty_constructor [Statement]	A type constructor: name + type of arguments
ty_var [Tip_ast]
ty_view [FO]	Type
tydef [Statement]	A (co)inductive type.
tydef [FO]
typed_var [Tip_ast]
typed_var [UntypedAST]	A variable with, possibly, its type
U
universe [FO_rel]	A universe is a list of sub-universes, each with a different name
unknown_info [Problem.Res]
unmangle_state [Monomorphization]	State used to un-mangle specialized symbols
unop [FO_rel]
V
value [Transform.Features]
value_def [Model]
var [TypeInference]
var [Tip_ast]
var [TPTP_model_ast]
var [TypeMono]
var [TypePoly]
var [Pattern]
var [TermMono]
var [TermTyped]
var [TermInner]
var [FO_rel]
var [FO_tptp]
var [Statement]
var [FO]
var [UntypedAST]
var [Var.Subst]
var_or_wildcard [UntypedAST]
var_ty [FO_rel]
view [TypeMono]
view [TypePoly]
view [Pattern]
view [TermMono]
view [TermTyped]	Same view as `TermInner`
view [TermInner]	The main view of terms.
view [Statement]
view [FO]	Term
W
warning [Utils]
with_loc [Location]