Index of types

A
any [Session]
assertion_kind [Mlw_expr]
aty [Mlw_ty]
B
binop [Term]
C
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

D
data_decl [Mlw_decl]
data_decl [Decl]
decl [Decl]
decl_node [Decl]
detached [Session]
driver [Driver]
E
effect [Mlw_ty]
elt [Extset.S]

The type of set elements.

enumeration [Extmap.S]

enumeration: zipper style

env [Env]
env_session [Session]
expr [Mlw_expr]
expr_node [Mlw_expr]
extension [Env]
F
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]
G
goal [Session]
goal_parent [Session]
H
hide [Session]

For internal use

I
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]
K
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]
L
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]
M
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]
N
namespace [Mlw_module]
namespace [Theory]
notify [Session]

type of functions which notify modification of the verified field

P
pathname [Env]
pattern [Term]
pattern_node [Term]
pdecl [Mlw_decl]
pdecl_node [Mlw_decl]
plsymbol [Mlw_expr]
post [Mlw_ty]

postcondition: eps result .

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]
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]

Type that represents a single prover run

prover_result [Call_provers]
prover_result_parser [Call_provers]
prover_update [Call_provers]
prover_upgrade_policy [Whyconf]
prsymbol [Decl]
psymbol [Mlw_expr]
pvsymbol [Mlw_ty]
Q
quant [Term]
R
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]
S
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
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_def [Ty]
type_symbol [Mlw_module]
tysymbol [Ty]
U
update_context [Session]
V
variant [Mlw_ty]

tau * (tau -> tau -> prop)

varset [Mlw_ty.T]
vsymbol [Term]
vty [Mlw_ty]
X
xpost [Mlw_ty]

exceptional postconditions

xsymbol [Mlw_ty]