Index of types

any [Session]
assertion_kind [Mlw_expr]
aty [Mlw_ty]

binop [Term]

clone_map [Task]
config [Whyconf]
A configuration linked to an rc file.
config_editor [Whyconf]
config_prover [Whyconf]
config_strategy [Whyconf]
constructor [Mlw_decl]
constructor [Decl]
constructor symbol with the list of projections

data_decl [Mlw_decl]
data_decl [Decl]
decl [Decl]
decl_node [Decl]
detached [Session]
driver [Driver]

effect [Mlw_ty]
elt [Extset.S]
The type of set elements.
enumeration [Extmap.S]
enumeration: zipper style
env [Env]
env_session [Session]
expl [Session]
An explanation gives hint about how the goal has been produced.
expr [Mlw_expr]
expr_node [Mlw_expr]
extension [Env]

family [Rc]
A family in rc files
fformat [Env]
field [Mlw_expr]
file [Session]
filename [Env]
filter_prover [Whyconf]
filter prover
flag [Debug]
fold [Util]
fold2 [Util]
foldd [Util]
for_bounds [Mlw_expr]
for_direction [Mlw_expr]
format_parser [Env]
(fn : 'a format_parser) env path file ch parses the in_channel ch and returns the language-specific contents of type 'a.
fun_defn [Mlw_expr]

goal [Session]
goal_parent [Session]

hide [Session]
For internal use

ident [Ident]
ident_path [Session]
ident_printer [Ident]
idpos [Session]
ind_decl [Decl]
ind_list [Decl]
ind_sign [Decl]
invariant [Mlw_expr]
ity [Mlw_ty.T]
ity = individual type in programs, first-order, i.e.
ity_node [Mlw_ty.T]
ity_subst [Mlw_ty]
itysymbol [Mlw_ty.T]

key [Session_scheduler.OBSERVER]
type key allowing to uniquely identify an element of of session: a goal, a transformation, a proof attempt, a theory or a file.
key [Weakhtbl.S]
key [Exthtbl.Private]
key [Extmap.S]
The type of the map keys.
keygen [Session]
type of functions which can generate keys
known_map [Mlw_decl]
known_map [Decl]

label [Ident]
lambda [Mlw_expr]
language [Env]
let_defn [Mlw_expr]
let_sym [Mlw_expr]
loaded_prover [Session]
loaded_provers [Session]
logic_decl [Decl]
ls_defn [Decl]
lsymbol [Term]

main [Whyconf]
Main section
meta [Theory]
meta_arg [Theory]
meta_arg_type [Theory]
meta_args [Session]
meta_map [Task]
metas [Session]
metas_args [Session]
mlw_file [Mlw_module]
mod_inst [Mlw_module]
modul [Mlw_module]
module_or_theory [Mlw_module]
module_uc [Mlw_module]

namespace [Mlw_module]
namespace [Theory]
notify [Session]
type of functions which notify modification of the verified field

pathname [Env]
pattern [Term]
pattern_node [Term]
pdecl [Mlw_decl]
pdecl_node [Mlw_decl]
plsymbol [Mlw_expr]
post [Mlw_ty]
postcondition: eps result .
post_prover_call [Call_provers]
Thread-unsafe closure that interprets the prover's results
ppattern [Mlw_expr]
pre [Mlw_ty]
precondition: pre_fmla
pre_constructor [Mlw_decl]
pre_data_decl [Mlw_decl]
pre_field [Mlw_decl]
pre_ppattern [Mlw_expr]
pre_prover_call [Call_provers]
Thread-safe closure that launches the prover
preid [Ident]
a user-created type of unregistered identifiers
prog_symbol [Mlw_module]
proof_attempt [Session]
proof_attempt_status [Session]
State of a proof
prop_decl [Decl]
prop_kind [Decl]
prover [Whyconf]
record of necessary data for a given external prover
prover_answer [Call_provers]
prover_call [Call_provers]
Functions for calling external provers
prover_result [Call_provers]
prover_result_parser [Call_provers]
prover_upgrade_policy [Whyconf]
prsymbol [Decl]
psymbol [Mlw_expr]
pvsymbol [Mlw_ty]

quant [Term]

rc_value [Rc]
reason_unknown [Call_provers]
The reason why unknown was reported
region [Mlw_ty.T]
report [Session_scheduler.Make]
resource_limit [Call_provers]
run_external_status [Session_scheduler.Make]

section [Rc]
Section in rc file
session [Session]
simple_family [Rc]
A family w/o arguments in rc files
spec [Mlw_ty]
spec [Debug.Args]
stat [Debug]
stepregexp [Call_provers]
The type of precompiled regular expressions for parsing of steps
symbol_map [Mlw_expr]
symbol_map [Theory]
symset [Mlw_expr]

t [Session_scheduler.Make]
the scheduler environment
t [Rc]
Rc parsed file
t [Stdlib.TaggedType]
t [Stdlib.OrderedHashedType]
t [Weakhtbl.Weakey]
t [Weakhtbl.S]
t [Exthtbl.Private]
Private Hashtbl
t [Extset.S]
The type of sets of type elt.
t [Extmap.S]
The type of maps from type key to type 'a.
tag [Weakhtbl]
task [Task]
task_hd [Task]
task_option [Session]
The task can be removed and later reconstructible
tdecl [Theory]
tdecl_node [Theory]
tdecl_set [Task]
term [Term]
term_bound [Term]
term_branch [Term]
term_node [Term]
term_quant [Term]
th_inst [Theory]
theory [Session]
theory [Theory]
theory_uc [Theory]
a theory under construction
timeregexp [Call_provers]
The type of precompiled regular expressions for time parsing
todo [Session_scheduler.Todo]
transf [Session]
trigger [Term]
tvsymbol [Ty]
ty [Ty]
ty_node [Ty]
type_symbol [Mlw_module]
tysymbol [Ty]

update_context [Session]

variant [Mlw_ty]
tau * (tau -> tau -> prop)
varset [Mlw_ty.T]
vsymbol [Term]
vty [Mlw_ty]

xpost [Mlw_ty]
exceptional postconditions
xsymbol [Mlw_ty]