Index of types

any [Session_itp]
assertion_kind [Expr]
assign [Expr]
attribute [Ident]
binop [Term]
blacklist [Printer]
call_set [Decl]
cexp [Expr]
cexp_node [Expr]
clone_map [Task]
color [Itp_communication]

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

config [Whyconf]

A configuration linked to an rc file.

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

constructor symbol with the list of projections

controller [Controller_itp]
cty [Ity]
data_decl [Decl]
dec_real_format [Number]
decl [Decl]
decl_node [Decl]
diff_decl [Trans]
driver [Driver]
effect [Ity]
elt [Extset.S]

The type of set elements.

enumeration [Extmap.S]

enumeration: zipper style

env [Env]
exn_branch [Expr]
expr [Expr]
expr_node [Expr]
extension [Env]
family [Rc]

A family in rc files

fformat [Env]
file [Session_itp]
fileID [Session_itp]
file_path [Session_itp]
filename [Env]
filter_prover [Whyconf]

filter prover

flag [Debug]
flag_trans [Trans]
float_format [Number]
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]
gentrans [Trans]
global_information [Itp_communication]

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

ide_request [Itp_communication]
ident [Ident]
ident_printer [Ident]
ind_decl [Decl]
ind_list [Decl]
ind_sign [Decl]
int_range [Number]
integer_constant [Number]
integer_format [Number]
integer_literal [Number]
integer_support_kind [Number]
interface [Printer]
interface_map [Printer]
invariant [Expr]
its_defn [Pdecl]
its_flag [Ity]
ity [Ity]
ity_node [Ity]
ity_subst [Ity]
itysymbol [Ity]
key [Weakhtbl.S]
key [Exthtbl.Private]
key [Extmap.S]

The type of the map keys.

known_map [Pdecl]
known_map [Decl]
language [Env]
let_defn [Expr]
logic_decl [Decl]
ls_defn [Decl]
lsymbol [Term]
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]
mlw_file [Pmodule]
mod_inst [Pmodule]
mod_unit [Pmodule]
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.

negative_format [Number]
node_ID [Itp_communication]
node_type [Itp_communication]
notation [Ident]
notification [Itp_communication]
notifier [Session_itp]
number_support [Number]
number_support_kind [Number]
oneway [Ity]
overload [Pmodule]
part_real_format [Number]
pat_ghost [Expr]
pathname [Env]
pattern [Term]
pattern_node [Term]
pdecl [Pdecl]
pdecl_node [Pdecl]
pmodule [Pmodule]
pmodule_uc [Pmodule]
position [Loc]
post [Ity]

postcondition: eps result .

pp [Pp]
pre [Ity]

precondition: pre_fmla

pre_pattern [Expr]
preid [Ident]

a user-created type of unregistered identifiers

prelude [Printer]
prelude_map [Printer]
printer [Printer]
printer_args [Printer]
printer_mapping [Printer]
prog_pattern [Expr]
prog_symbol [Pmodule]
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]
pvsymbol [Ity]
quant [Term]
rc_value [Rc]
real_constant [Number]
real_format [Number]
real_literal [Number]
rec_defn [Expr]
reg_branch [Expr]
region [Ity]
report [Controller_itp.Make]
resource_limit [Call_provers]
rs_kind [Expr]
rs_logic [Expr]
rsymbol [Expr]
section [Rc]

Section in rc file

session [Session_itp]
simple_family [Rc]

A family w/o arguments in rc files

spec [Debug.Args]
stat [Debug]
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_map [Printer]
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 [Term]
term_bound [Term]
term_branch [Term]
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]
ty [Ty]
ty_node [Ty]
type_def [Ty]
tysymbol [Ty]
update_info [Itp_communication]
variant [Expr]

tau * (tau -> tau -> prop)

vs_graph [Decl]
vsymbol [Term]
xsymbol [Ity]