Index of types

A
any [Session_itp]
any_pp [Pretty]
arg [Getopt]
arr_index [Model_parser]
assertion_kind [Expr]
assign [Expr]
attr [Ptree]
attribute [Ident]
B
bad_instance [Theory]
big_float [Pinterp]
binder [Ptree]
binop [Term]
blacklist [Printer]
C
call_set [Decl]
ce_summary [Counterexample]
cexp [Expr]
cexp_node [Expr]
check_model_result [Counterexample]
clone_map [Task]
clone_subst [Ptree]

The possible clone substitution elements

cmptr [Util]

A comparator for values of type 'a *

cntr_ctx [Pinterp]

Context of a contradiction during RAC

color [Itp_communication]

Used to give colors to the parts of the source code that corresponds to the following property in the current task.

compare [Util]
config [Whyconf]

A configuration linked to an rc file.

config_editor [Whyconf]
config_prover [Whyconf]
config_strategy [Whyconf]
constructor [Decl]

constructor symbol with the list of projections

controller [Controller_itp]
cty [Ity]
D
data_decl [Decl]
decl [Ptree]

top-level declarations

decl [Decl]
decl_node [Decl]
default_format [Number]
delayed_format [Number]
diff_decl [Trans]
doc [Getopt]
driver [Driver]
E
effect [Ity]
elt [Extset.S]

The type of set elements.

enumeration [Extmap.S]

enumeration: zipper style

env [Pinterp]

Context for the interpreter

env [Env]
exec_kind [Pinterp.Log]
exec_log [Pinterp.Log]
exn_branch [Ptree]

An exception match branch

exn_branch [Expr]
expr [Ptree]

Expressions, equipped with a source location

expr [Expr]
expr_desc [Ptree]

Expression kinds

expr_node [Expr]
extension [Env]
F
family [Rc]

A family in rc files

fformat [Env]
field [Ptree]

record fields

field [Pinterp.Value]
field_info [Printer]
field_name [Model_parser]
file [Session_itp]
fileID [Session_itp]
filename [Env]
filter_prover [Whyconf]

filter prover

flag [Debug]
flag_trans [Trans]
float_format [Number]
float_mode [Pinterp]
fold [Util]
fold2 [Util]
foldd [Util]
for_bounds [Expr]
for_direction [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.

formatted [Pp]

formatted: string which is formatted "@ " allow to cut the line if too long

formatter [Pp]
frac_real_format [Number]
full_verdict [Counterexample]
fundef [Ptree]

Local function definition

G
gentrans [Trans]
ghost [Ptree]
global_information [Itp_communication]

Global information known when server process has started and that can be shared with the IDE through communication

H
handler [Getopt]
I
ide_request [Itp_communication]
ident [Ptree]
ident [Ident]
ident_printer [Ident]
import_value [Pinterp]
ind_decl [Ptree]

A single declaration of an inductive predicate

ind_decl [Decl]
ind_list [Decl]
ind_sign [Decl]
int_constant [Number]
int_literal_kind [Number]
int_range [Number]
int_value [Number]
integer_format [Number]
interface [Printer]
interface_export_map [Printer]
interface_map [Printer]
invariant [Ptree]

Loop invariant or type invariant

invariant [Expr]
its_defn [Pdecl]
its_flag [Ity]
ity [Ity]
ity_node [Ity]
ity_subst [Ity]
itysymbol [Ity]
K
key [Weakhtbl.S]
key [Exthtbl.Private]
key [Extmap.S]

The type of the map keys.

key [Getopt]
known_map [Pdecl]
known_map [Decl]
L
language [Env]
let_defn [Expr]
log_entry [Pinterp.Log]
log_entry_desc [Pinterp.Log]
log_uc [Pinterp.Log]
logic_decl [Ptree]

A single declaration of a function or predicate

logic_decl [Decl]
ls_defn [Decl]
lsymbol [Term]
M
main [Whyconf]

Main section

mask [Ity]
message_notification [Itp_communication]
meta [Theory]
meta_arg [Theory]
meta_arg_type [Theory]
meta_decl [Pdecl]
meta_map [Task]
metarg [Ptree]

Arguments of meta declarations

mlw_file [Ptree]
mlw_file [Pmodule]
mod_inst [Pmodule]
mod_unit [Pmodule]
model [Model_parser]
model_array [Model_parser]
model_bv [Model_parser]
model_dec [Model_parser]
model_element [Model_parser]

Counter-example model elements.

model_element_kind [Model_parser]
model_element_name [Model_parser]

Information about the name of the model element

model_float [Model_parser]
model_float_binary [Model_parser]
model_frac [Model_parser]
model_int [Model_parser]
model_parser [Model_parser]

Parses the input string into model elements, estabilishes a mapping between these elements and mapping from printer and builds model data structure.

model_proj [Model_parser]
model_record [Model_parser]
model_value [Model_parser]
mpfr_float [Mlmpfr_wrapper]
mpfr_rnd_t [Mlmpfr_wrapper]
N
namespace [Pmodule]
namespace [Theory]
naming_table [Trans]

In order to interpret, that is type, string arguments as symbols or terms, a transformation may need a naming_table.

next_unproved_node_strat [Itp_communication]
node_ID [Itp_communication]
node_type [Itp_communication]
notation [Ident]
notification [Itp_communication]
notifier [Session_itp]
number_support [Number]
O
oneway [Ity]
opt [Getopt]
overload [Pmodule]
P
param [Ptree]
pat_desc [Ptree]
pat_ghost [Expr]
pathname [Env]
pattern [Ptree]
pattern [Term]
pattern_node [Term]
pdecl [Pdecl]
pdecl_node [Pdecl]
pmodule [Pmodule]
pmodule_uc [Pmodule]
position [Loc]
post [Ptree]

Normal postcondition

post [Ity]

postcondition: eps result .

pp [Pp]
pre [Ptree]

Precondition

pre [Ity]

precondition: pre_fmla

pre_pattern [Expr]
preid [Ident]

a user-created type of unregistered identifiers

prelude [Printer]
prelude_export_map [Printer]
prelude_map [Printer]
printer [Printer]
printer_args [Printer]
printer_mapping [Printer]
printers [Mlw_printer]

The marked printer potentially adds the marker, the closed printer adds parentheses to the potentially marked node

prog_pattern [Expr]
prog_symbol [Pmodule]
proj_name [Model_parser]
proofAttemptID [Session_itp]
proofNodeID [Session_itp]
proof_attempt_node [Session_itp]
proof_attempt_status [Controller_itp]
proof_parent [Session_itp]
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]
pty [Ptree]
pvsymbol [Ity]
Q
qualid [Ptree]
quant [Term]
R
rac_config [Pinterp]
rac_prover [Pinterp]

The configuration of the prover used for reducing terms in RAC

rac_reduce_config [Pinterp]

The configuration for RAC, including (optionally) a transformation for reducing terms (usually: compute_in_goal), and a prover to be used if the transformation does not yield a truth value.

raw_model_parser [Model_parser]
rc_value [Rc]
real_constant [Number]
real_format [Number]
real_literal_kind [Number]
real_value [Number]
rec_defn [Expr]
reg_branch [Ptree]

A regular match branch

reg_branch [Expr]
region [Ity]
report [Controller_itp.Make]
resource_limit [Call_provers]
result [Pinterp]

Result of the interpreter *

rs_kind [Expr]
rs_logic [Expr]
rsymbol [Expr]
S
section [Rc]

Section in rc file

session [Session_itp]
sign [Mlmpfr_wrapper]
simple_family [Rc]

A family w/o arguments in rc files

sort_models [Counterexample]

Sort prover models in select_model.

spec [Ptree]

Contract

spec [Debug.Args]
stat [Debug]
state [Ptree_helpers.F]
stepregexp [Call_provers]

The type of precompiled regular expressions for parsing of steps

strategy [Itp_communication]
strategy_status [Controller_itp]
symbol [Args_wrapper]
symbol_map [Theory]
syntax [Pretty]
syntax_map [Printer]
T
t [Coercion]

a set of coercions

t [BigInt]
t [Rc]

Rc parsed file

t [Wstdlib.TaggedType]
t [Wstdlib.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]
tdecl [Theory]
tdecl_node [Theory]
tdecl_set [Task]
term [Ptree]
term [Term]
term_bound [Term]
term_branch [Term]
term_desc [Ptree]
term_node [Term]
term_quant [Term]
th_inst [Theory]
theory [Session_itp]
theory [Theory]
theory_uc [Theory]
timeregexp [Call_provers]

The type of precompiled regular expressions for time parsing

tlist [Trans]
trans [Trans]
transID [Session_itp]
trans_typ [Args_wrapper]
trans_with_args [Trans]
trans_with_args_l [Trans]
transformation [Itp_communication]
transformation_status [Controller_itp]
trigger [Term]
tvsymbol [Ty]
two_strings_format [Number]
ty [Ty]
ty_node [Ty]
type_decl [Ptree]
type_def [Ptree]

Type definition body

type_def [Ty]
tysymbol [Ty]
U
update_info [Itp_communication]
V
value [Pinterp.Value]
value_desc [Pinterp.Value]
variant [Ptree]

Variant for both loops and recursive functions

variant [Expr]

tau * (tau -> tau -> prop)

verdict [Counterexample]
visibility [Ptree]
vs_graph [Decl]
vsymbol [Term]
X
xpost [Ptree]

Exceptional postcondition

xsymbol [Ity]