Index of values

A
abs [Mlmpfr_wrapper]
abs [BigInt]
abs_int [Number]
abs_real [Number]
add [Mlmpfr_wrapper]
add [Extset.S]

add x s returns a set containing the same elements as s, plus x.

add [Extmap.S]

add x y m returns a map containing the same bindings as m, plus a binding of x to y.

add [Coercion]

adds a new coercion from function ls: ty1 -> ty2 raises an error if this introduces a cycle, i.e. a coercion from ty2 to ty1 is already defined;, function ls cannot be used as a coercion, e.g. ty1 = ty2;, a coercion from ty1 to ty2 is already defined

add [BigInt]
add_body [Ptree_helpers.I]
add_body [Ptree_helpers.F]
add_builtin [Env]

add_builtin lang builtin adds new builtin libraries to lang.

add_clone_internal [Theory]
add_command [Whyconf.Args]
add_data_decl [Theory]
add_data_decl [Task]
add_decl [Typing.Unsafe]
add_decl [Typing]
add_decl [Theory]
add_decl [Task]
add_decl_with_tuples [Theory]
add_decls [Trans]
add_extra_config [Whyconf]

add_extra_config config filename merges the content of filename into config

add_file [Controller_itp]

add_file cont ?fmt fname parses the source file fname and add the resulting theories to the session of cont.

add_file_section [Session_itp]

add_file_section s fp ths adds a new 'file' section in session s, named fp, containing fresh theory subsections corresponding to theories ths.

add_flush [Pp]
add_ind_decl [Theory]
add_ind_decl [Task]
add_int [BigInt]
add_left [Extset.S]

add_left s x is the same as add x s.

add_logic_decl [Theory]
add_logic_decl [Task]
add_meta [Theory]
add_meta [Task]
add_meta [Pmodule]
add_new [Extset.S]

add_new e x s adds x to s if s does not contain x, and raises e otherwise.

add_new [Extmap.S]

add_new e x v m binds x to v in m if x is not bound, and raises e otherwise.

add_param_decl [Theory]
add_param_decl [Task]
add_pdecl [Pmodule]

add_pdecl ~vc m d adds declaration d in module m.

add_plugin [Whyconf]
add_post [Ptree_helpers.I]
add_post [Ptree_helpers.F]
add_pre [Ptree_helpers.I]
add_pre [Ptree_helpers.F]
add_premises [Pinterp_core]

add_premises ts p adds the terms ts to the premises.

add_prop [Ptree_helpers.I]
add_prop [Ptree_helpers.F]
add_prop_decl [Theory]
add_prop_decl [Task]
add_provers [Whyconf]

add_provers config provers shortcuts augments the prover family of config by the one given in provers, and with the given shortcuts.

add_registered_lang [Itp_server]
add_rliteral_map [Printer]
add_strategy [Whyconf]
add_syntax_map [Printer]
add_tdecl [Task]
add_tdecls [Trans]

add_decls ld t1 adds decls ld at the end of the task t1 (before the goal)

add_timing [Debug.Stats]

Record a raw timing obtained externally, e.g., from prover execution.

add_ty_decl [Theory]
add_ty_decl [Task]
all [Util]
all2 [Util]
all2_fn [Util]

all2_fn pr z a b returns true if pr a b is true, otherwise raises Util.FoldSkip.

all_fn [Util]

all_fn pr z a returns true if pr a is true, otherwise raises Util.FoldSkip.

all_options [Whyconf.Args]
alld [Util]
alt [Pp]
alt2 [Pp]
annot_attr [Ity]
ansi_color_tags [Util]

Functions to interpret tags as ANSI terminal color codes.

any [Util]
any2 [Util]
any2_fn [Util]

any2_fn pr z a b returns false if pr a b is false, otherwise raises Util.FoldSkip.

any_fn [Util]

any_fn pr z a returns false if pr a is false, otherwise raises Util.FoldSkip.

any_iter_proof_attempt [Session_itp]
any_proved [Session_itp]
anyd [Util]
append_to_model_element_name [Ident]

The returned set of attributes will contain the same set of attributes as argument attrs except that an attribute of the form "model_trace:*@*" will be "model_trace:*to_append@*".

append_to_model_trace_attr [Ident]

The returned set of attributes will contain the same set of attributes as argument attrs except that an attribute of the form "model_trace:*" will be "model_trace:*to_append".

apply [Trans]
apply [Lists]

apply f [a1;..;an] returns (f a1)@...@(f an).

apply_trans_to_goal [Session_itp]

apply_trans_to_goal s env tr args id applies the transformation tr with arguments args to the goal id, and returns the subtasks.

apply_transform [Trans]

apply a registered 1-to-1 or a 1-to-n, directly.

apply_transform_args [Trans]

apply a registered 1-to-1 or a 1-to-n or a trans with args, directly

aprinter [Pretty.Printer]

printer for identifiers of type variables

arrow [Pp]
asd [Pp]

add string delimiter " "

asym_split [Term]
attr_compare [Ident]
attr_equal [Ident]
attr_hash [Ident]
attr_w_non_conservative_extension_no [Theory]
axiom_of_invariant [Pdecl]

axiom_of_invariant itd returns a closed formula that postulates the type invariant of itd for all values of the type

B
base_language [Env]

base_language is the root of the tree of supported languages.

base_language_builtin [Env]

base_language_builtin path returns the builtin theories defined by the base language.

begin_let [Ptree_helpers.I]
begin_let [Ptree_helpers.F]
begin_module [Ptree_helpers.I]

see begin_module above

begin_module [Ptree_helpers.F]
best_non_empty_giant_step_rac_result [Check_ce]

Select the best non empty model based on the result of the giant-step RAC execution, with the following classification: RAC_done (Res_fail _ , _) > RAC_done (Res_normal, _) > RAC_done (Res_stuck _ , _) > RAC_done (Res_incomplete _ , _) > RAC_not_done _

bind [Trans]
bind_comp [Trans]
bind_ls [Pinterp_core]
bind_pvs [Pinterp_core]
bind_rs [Pinterp_core]
bind_vs [Pinterp_core]
bindings [Extmap.S]

Return the list of all bindings of the given map.

bisect_proof_attempt [Controller_itp.Make]

bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed cont id runs a bisection process based on the proof attempt id of the session managed by cont.

blocking [Controller_itp.Scheduler]

Set to true when the scheduler should wait for results of why3server (script), false otherwise (ITP which needs reactive scheduling)

bool [Pp]
bool_module [Pmodule]
bool_theory [Theory]
bool_value [Pinterp_core]
bounded_split [Strings]

bounded_split c s n do the same as split c s but splits into n substring at most.

break_attr [Ity]
build_naming_tables [Args_wrapper]

builds a naming tabl from a task, suitable for both parsing/typing transformation arguments and for printing the task, with coherent identifiers names.

builtin_attr [Ident]

indicates that the related ident comes from a builtin of the language, for instance the builtin `ref` in WhyML.

builtin_module [Pmodule]
builtin_theory [Theory]
C
c_any [Expr]
c_app [Expr]
c_fun [Expr]
c_ghost [Expr]
c_pur [Expr]
c_rs_subst [Expr]
call_editor [Call_provers]
call_on_buffer [Call_provers]

Build a prover call on the task already printed in the Buffer.t given.

capitalize [Strings]
cardinal [Extset.S]

Return the number of elements in a set.

cardinal [Extmap.S]

Return the number of bindings of a map.

catch_unsupportedDecl [Printer]
catch_unsupportedTerm [Printer]
catch_unsupportedType [Printer]

catch_unsupportedType f return a function which applied on arg: return f arg if f arg does not raise Printer.Unsupported exception, raise UnsupportedType (arg,s) if f arg raises Unsupported s

change [Extset.S]

change f x s returns a set containing the same elements as s, except x which is added to s if f (mem x s) returns true and removed otherwise.

change [Extmap.S]

change f x m returns a map containing the same bindings as m, except the binding of x in m is changed from y to f (Some y) if m contains a binding of x, otherwise the binding of x becomes f None.

change_prover [Session_itp]

change_prover s id opr npr changes the prover of the proof attempt using prover opr by the new prover npr.

char_is_uppercase [Strings]
char_to_alnum [Ident]
char_to_alnumus [Ident]
char_to_alpha [Ident]
char_to_lalnum [Ident]
char_to_lalnumus [Ident]
char_to_lalpha [Ident]
char_to_ualpha [Ident]
check_assume_posts [Pinterp_core]
check_assume_term [Pinterp_core]
check_assume_terms [Pinterp_core]
check_assume_type_invs [Pinterp_core]
check_exhaustive [Rc]

check_exhaustive section keys checks that only the keys in keys appear inside the section section.

check_float [Number]

check_float c fp is the same as compute_float c fp but does not return any value.

check_literal [Term]
check_post [Pinterp_core]

Check a post-condition t by binding the result variable to the term vt representing the result value.

check_posts [Pinterp_core]
check_range [Number]

check_range c ir checks that c is in the range described by ir.

check_syntax_logic [Printer]

check_syntax_logic ls syntax check that syntax doesn't mention arguments that ls doesn't have

check_syntax_type [Printer]

check_syntax_type tys syntax check that syntax doesn't mention arguments that tys doesn't have

check_term [Pinterp_core]
check_term_dummy [Pinterp_core]
check_terms [Pinterp_core]
check_type_invs [Pinterp_core]
check_variant [Pinterp_core]
choose [Extset.S]

Return one element of the given set, or raise Not_found if the set is empty.

choose [Extmap.S]

Return one binding of the given map, or raise Not_found if the map is empty.

chop [Lists]

chop n l removes the first n elements of l.

chop_last [Lists]

Remove (and return) the last element of a list.

classify [Check_ce]

Classify a counterexample based on the results of the normal and giant-step RAC executions.

clean [Controller_itp.Make]

Remove each proof attempt or transformation that are below proved goals, that are either obsolete or not valid.

clean_model [Model_parser]
clear [Weakhtbl.S]
clone_export [Theory]
clone_export [Task]
clone_export [Pmodule]
clone_meta [Theory]

clone_meta td_meta th sm produces from td_meta a new Meta tdecl instantiated with respect to sm.

clone_post_result [Ity]
clone_theory [Theory]
close_file [Typing]
close_file_and_formatter [Pp]
close_formatter [Pp]
close_module [Typing]
close_module [Pmodule]
close_scope [Typing]
close_scope [Theory]
close_scope [Pmodule]
close_theory [Theory]
cmp [Util]

Create a comparison function using lexical order defined by a list of comparators.

cmp_lists [Util]

Create a comparison function for lists using lexical order defined by a list of comparators.

cmptr [Util]

Create a comparator by a projection and a comparison function between projected values

cmptr_direct [Util]
coercion_attr [Pretty]

Attribute to put on unary functions to make them considered as coercions, hence not printed by default.

colon [Pp]
comma [Pp]
commands [Getopt]

commands hold the name of the currently running command, Sys.argv.(0) by default.

common_options [Whyconf.Args]
compare [Wstdlib.OrderedHashedType]
compare [Loc]
compare [Lists]
compare [Extset.S]

Total ordering between sets.

compare [Extmap.S]

Total ordering between maps.

compare [BigInt]
compare_real [Number]

Compare two real values.

compare_values [Pinterp_core]
complete_initialization [Whyconf.Args]
compose [Trans]
compose_l [Trans]
compute_float [Number]

compute_float c fp checks that c is a float literal representable in the format fp.

compute_model_trace_field [Ident]

Take an optional projection name and the depths of its occurrence and return the built field attribute associated

compute_term_dummy [Pinterp_core]

An implementation that is just the identity, i.e.

computer_div [BigInt]
computer_div_mod [BigInt]
computer_mod [BigInt]
concrete_apply_equ [Model_parser]
concrete_apply_from_ls [Model_parser]
concrete_const_bool [Model_parser]
concrete_var_from_vs [Model_parser]
cons [Lists]
const [Util]
const [Ptree_helpers]
const2 [Util]
const3 [Util]
const_pi [Mlmpfr_wrapper]
constant_formatted [Pp]
constant_string [Pp]
constr_value [Pinterp_core]
contains [Extset.S]

contains s x is the same as mem x s.

contains [Extmap.S]

contains m x is the same as mem x m.

copy [Weakhtbl.S]
copy_paste [Controller_itp.Make]
create [Ptree_helpers.F]
create [Pretty]

create spr apr tpr ppr creates a new pretty-printing module from the printer spr for variables and functions, apr for type variables, tpr for type symbols and ppr for proposition names.

create [Weakhtbl.S]
create_alias_decl [Pdecl]

create_alias_decl id args def creates a new alias type declaration.

create_alias_itysymbol [Ity]

create_alias_itysymbol id args def creates a new type alias.

create_attribute [Ident]
create_call_result_attr [Ident]

A call result attribute on a counterexample model element marks the result of a call at the given location

create_call_set [Decl]
create_constructor [Expr]
create_controller [Controller_itp]

creates a controller for the given session.

create_cty [Ity]

create_cty ?mask ?defensive args pre post xpost oldies effect result creates a new cty.

create_cty_defensive [Ity]

same as create_cty, except that type variables in the result and exceptional results are spoiled and fresh regions in the result and exceptional results are reset.

create_data_decl [Decl]
create_debugging_trans [Trans]
create_decl [Theory]
create_eid_attr [Expr]

create_eid_attr id generates an attribute corresponding to the given expression identifier id

create_env [Env]

creates an environment from a "loadpath", a list of directories containing loadable Why3/WhyML/etc files

create_exn_decl [Pdecl]
create_float_decl [Pdecl]

create_float_decl id fp creates a new float type declaration.

create_float_itysymbol [Ity]

create_float_itysymbol id f creates a new float type.

create_fsymbol [Term]

~constr is the number of constructors of the type in which the symbol is a constructor otherwise it must be the default 0.

create_ident_printer [Ident]

start a new printer with a sanitizing function and a blacklist

create_ind_decl [Decl]
create_let_decl [Pdecl]
create_logic_decl [Decl]
create_lsymbol [Term]
create_meta [Theory]
create_model_element [Model_parser]

Creates a counterexample model element.

create_model_trace_attr [Ident]
create_module [Pmodule]
create_param_decl [Decl]
create_plain_record_decl [Pdecl]

create_plain_record_decl ~priv ~mut id args fields invl witn creates a declaration for a non-recursive record type, possibly private and/or mutable.

create_plain_record_itysymbol [Ity]

create_plain_record_itysymbol ~priv ~mut id args fields invl creates a new type symbol for a non-recursive record type, possibly private or mutable.

create_plain_variant_decl [Pdecl]

create_plain_variant_decl id args constructors creates a declaration for a non-recursive algebraic type.

create_plain_variant_itysymbol [Ity]

create_plain_variant_itysymbol id args fields creates a new type symbol for a non-recursive algebraic type.

create_post [Ity]
create_prog_pattern [Expr]
create_projection [Expr]
create_prop_decl [Decl]
create_prsymbol [Decl]
create_psymbol [Term]
create_pure_decl [Pdecl]
create_pvsymbol [Ity]
create_range [Number]
create_range_decl [Pdecl]

create_range_decl id ir creates a new range type declaration.

create_range_itysymbol [Ity]

create_range_itysymbol id r creates a new range type.

create_rec_itysymbol [Ity]

create_rec_itysymbol id args creates a new type symbol for a recursively defined type.

create_rec_record_decl [Pdecl]

create_rec_record_decl its fields creates a declaration for a recursive record type.

create_rec_variant_decl [Pdecl]

create_rec_variant_decl id args constructors creates a declaration for a recursive algebraic type.

create_region [Ity]

create_region id s tl rl creates a fresh region.

create_rsymbol [Expr]

If ?kind is supplied and is not RKnone, then cty must have no effects except for resets which are ignored.

create_tag [Weakhtbl]
create_theory [Theory]
create_tvsymbol [Ty]
create_ty_decl [Decl]
create_type_decl [Pdecl]
create_tysymbol [Ty]
create_use [Theory]
create_user_id [Typing.Unsafe]
create_user_prog_id [Typing.Unsafe]
create_vs_graph [Decl]
create_vsymbol [Term]
create_written_attr [Ident]

The vc_written attribute is built during VC generation: it is used to track the location of the creation of variables.

create_xsymbol [Ity]
cty_add_post [Ity]

cty_add_post cty fl appends post-conditions in fl to cty.cty_post.

cty_add_pre [Ity]

cty_add_pre fl cty appends pre-conditions in fl to cty.cty_pre.

cty_apply [Ity]

cty_apply cty pvl rest res instantiates cty up to the types in pvl, rest, and res, then applies it to the arguments in pvl, and returns the computation type of the result, rest -> res, with every type variable and region in pvl being frozen.

cty_exec [Ity]

cty_exec cty converts a cty of a partial application into a cty of a fully applied application, returning a mapping.

cty_exec_post [Ity]

cty_exec_post cty returns a post-condition appropriate for use with local let-functions in VC generation.

cty_from_formula [Expr]
cty_ghost [Ity]

cty_ghost cty returns cty.cty_effect.eff_ghost

cty_ghostify [Ity]

cty_ghostify ghost cty ghostifies the effect of cty.

cty_pure [Ity]

cty_pure cty verifies that cty has no side effects except allocations.

cty_read_post [Ity]

cty_read_post cty pvs adds pvs to cty.cty_effect.eff_reads.

cty_read_pre [Ity]

cty_read_pre pvs cty adds pvs to cty.cty_effect.eff_reads.

cty_reads [Ity]

cty_reads cty returns the set of external dependencies of cty.

cty_tuple [Ity]

cty_tuple pvl returns a nullary tuple-valued cty with an appropriate cty_mask.

current_offset [Loc]
D
d_equal [Decl]
d_hash [Decl]
datadir [Whyconf]
debug [Call_provers]

debug flag for the calling procedure (option "--debug call_prover") If set call_on_buffer prints on stderr the commandline called and the output of the prover.

debug_array_as_update_chains_not_epsilon [Pinterp_core]

The debug parameter "rac-array-as-update-chains", a parameter for the conversion of arrays to terms in RAC.

debug_attrs [Call_provers]

Print attributes in model

debug_parse_only [Typing]
debug_trace_exec [Pinterp_core]

Print debug information during the interpretation of an expression.

debug_type_only [Typing]
decl [Trans]

decl f t1 t2 appends to task t1 the set of declarations f d for each declaration d of task t2, similarly to a "flat_map" operation on lists.

decl_fold [Decl.DeclTF]
decl_fold [Decl]

open recursion style.

decl_goal_l [Trans]

decl_goal_l f t1 t2 does the same as Trans.decl_l except that it can differentiate a new axiom added to a task from a new goal added to a task.

decl_l [Trans]

decl_f f t1 t2 produces a set of tasks obtained by appending new declarations to task t1.

decl_map [Decl.DeclTF]
decl_map [Decl]
decl_map_fold [Decl.DeclTF]
decl_map_fold [Decl]
decr [Debug.Stats]
default_config [Whyconf]

default_config filename create a default configuration which is going to be saved in filename

default_delay_ms [Controller_itp]

Default delay for the scheduler timeout

default_editor [Whyconf]

Editor name used when no specific editor is known for a prover

default_printing_info [Printer]

Empty mapping

default_value_of_type [Pinterp_core]

Return the default value of the given type.

desc_debug [Debug.Args]

Option for specifying a debug flag to set.

desc_debug_all [Debug.Args]

Option for setting all info flags.

desc_debug_list [Debug.Args]

Option for printing the list of debug flags.

desc_no_warn [Loc.Args]

Option for specifying a warning flag to set.

desc_shortcut [Debug.Args]

Option for setting a specific flag.

desc_warning_list [Loc.Args]

Option for printing the list of warning flags.

describe_cntr_ctx [Pinterp_core]
dexpr [Typing.Unsafe]
diff [Extset.S]

diff f s1 s2 computes the difference of two sets

diff [Extmap.S]

diff f m1 m2 computes a map whose keys is a subset of keys of m1.

disable_warning [Loc]

disable_warning id globally disables the warning with this id.

discard_file [Typing]
disjoint [Extset.S]

disjoint s1 s2 tests whether the sets s1 and s2 are disjoint.

disjoint [Extmap.S]

disjoint pr m1 m2 verifies that for every common key in m1 and m2, pr is verified.

div [Mlmpfr_wrapper]
diverges [Ity]
domain [Extmap.S]

domain m returns the set of keys of bindings in m

dot [Pp]
dprintf [Debug]

Print only if the flag is set.

drec_defn [Typing.Unsafe]
drop_while [Lists]

drop_while p l drops the initial elements of l that satisty p.

dummy_position [Loc]

Dummy source position.

dummy_tag [Weakhtbl]
duplicate_ident_printer [Ident]

This is used to avoid editing the current (mutable) printer when raising exception or printing information messages for the user.

E
e_absurd [Expr]
e_and [Expr]
e_app [Expr]
e_assert [Expr]
e_assign [Expr]
e_attr_add [Expr]
e_attr_copy [Expr]
e_attr_push [Expr]
e_attr_set [Expr]
e_const [Expr]
e_exec [Expr]
e_exn [Expr]
e_false [Expr]
e_fold [Expr]

e_fold does not descend into Cfun

e_for [Expr]
e_func_app [Expr]
e_func_app_l [Expr]
e_ghost [Expr]
e_ghostify [Expr]
e_if [Expr]
e_let [Expr]
e_locate_effect [Expr]

e_locate_effect pr e looks for a minimal sub-expression of e whose effect satisfies pr and returns its location

e_match [Expr]
e_nat_const [Expr]
e_not [Expr]
e_or [Expr]
e_pur [Expr]
e_pure [Expr]
e_raise [Expr]
e_rs_subst [Expr]
e_true [Expr]
e_tuple [Expr]
e_var [Expr]
e_void [Expr]
e_while [Expr]
eapp [Ptree_helpers]
eapply [Ptree_helpers]
econst [Ptree_helpers]
editor_by_id [Whyconf]

return the configuration of the editor if found, otherwise raise Not_found

eff_assign [Ity]
eff_bind [Ity]
eff_bind_single [Ity]
eff_catch [Ity]
eff_diverge [Ity]
eff_empty [Ity]

Effect of a non-ghost total function without any observational effect of any kinds

eff_equal [Ity]
eff_escape [Ity]
eff_fusion [Ity]
eff_ghostify [Ity]
eff_ghostify_weak [Ity]
eff_partial [Ity]
eff_pure [Ity]
eff_raise [Ity]
eff_read [Ity]
eff_read_post [Ity]
eff_read_pre [Ity]
eff_read_single [Ity]
eff_read_single_post [Ity]
eff_read_single_pre [Ity]
eff_reset [Ity]
eff_reset_overwritten [Ity]
eff_spoil [Ity]
eff_union_par [Ity]
eff_union_seq [Ity]
eff_write [Ity]
eid_attribute_prefix [Ident]

the prefix string for expression identifiers in attributes

elements [Extset.S]

Return the list of all elements of the given set.

empty [Rc]

An empty configuration.

empty [Extset.S]

The empty set.

empty [Extmap.S]

The empty map.

empty [Coercion]
empty_formatted [Pp]
empty_inst [Theory]
empty_limit [Call_provers]
empty_log [Pinterp_core.Log]
empty_log_uc [Pinterp_core.Log]
empty_mod_inst [Pmodule]
empty_model [Model_parser]
empty_ns [Theory]
empty_ns [Pmodule]
empty_rc [Whyconf]
empty_section [Rc]

An empty section.

empty_session [Session_itp]

create an empty_session in the directory specified by the argument.

empty_spec [Ptree_helpers]
end_module [Ptree_helpers.I]
end_module [Ptree_helpers.F]
ends_with [Strings]

Test if a string ends with another.

env_tag [Env]
eq [BigInt]
equal [Wstdlib.OrderedHashedType]
equal [Pp]
equal [Loc]
equal [Lists]
equal [Extset.S]

equal s1 s2 tests whether the sets s1 and s2 are equal.

equal [Extmap.S]

equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.

equal_p [Mlmpfr_wrapper]
error [Loc]
errorm [Loc]
euclidean_div [BigInt]
euclidean_div_mod [BigInt]
euclidean_mod [BigInt]
evar [Ptree_helpers]
exec_global_fundef [Pinterp]

eval_global_fundef ~rac env pkm dkm rcl rdl e evaluates e and returns an evaluation result and a final variable environment (for both local and global variables).

exec_rs [Pinterp]

eval_rs ~rac env pm rs evaluates the definition of rs and returns an evaluation result and a final environment.

exists [Extset.S]

exists p s checks if at least one element of s satisfies the predicate p.

exists [Extmap.S]

exists p m checks if at least one binding of the map satisfy the predicate p.

exit_with_usage [Whyconf.Args]
exp [Mlmpfr_wrapper]
export_as_zip [Session_itp]

export_as_zip s produces a zip archive of the session file.

expr [Ptree_helpers]
extract [Loc]

extract p1 p2 build a source position from two OCaml lexing positions

extract_field [Ident]

Take an attribute and extract its depth, name if it was a field attribute ("field:depth:field_name")

F
fd_of_rs [Expr]

raises Invalid_argument is rs_field is None

ffalse [Util]

Constant function false

field [Pinterp_core]
field_get [Pinterp_core]
field_set [Pinterp_core]
file_format [Session_itp]
file_id [Session_itp]

File

file_iter_proof_attempt [Session_itp]
file_of_task [Driver]

file_of_task d f th t produces a filename for the prover of driver d, for a task t generated from a goal in theory named th of filename f

file_of_theory [Driver]

file_of_theory d f th produces a filename for the prover of driver d, for a theory th from filename f

file_path [Session_itp]
file_proved [Session_itp]
file_theories [Session_itp]
filter [Extset.S]

filter p s returns the set with all the elements of s that satisfy predicate p.

filter [Extmap.S]

filter p m returns the map with all the bindings in m that satisfy predicate p.

filter_one_prover [Whyconf]

find the unique prover that verifies the filter.

filter_prover [Whyconf]

test if the prover match the filter prover

filter_prover_with_shortcut [Whyconf]

resolve prover shortcut in filter

filter_provers [Whyconf]

Get all the provers that match this filter

find [Exthtbl.Private]

Same as Hashtbl.find

find [Weakhtbl.S]
find [Extmap.S]

find x m returns the current binding of x in m, or raises Not_found if no such binding exists.

find [Coercion]

returns the coercion, or raises Not_found

find_clone_tds [Task]
find_constructors [Decl]
find_def [Exthtbl.Private]

return the first binding or the given value if none found

find_def [Exthtbl.S]

return the first binding or the given value if none found

find_def [Extmap.S]

find_def x d m returns the current binding of x in m, or return d if no such binding exists.

find_exn [Exthtbl.Private]

return the first binding or raise the given exception if none found

find_exn [Exthtbl.S]

return the first binding or raise the given exception if none found

find_exn [Extmap.S]

find_exn exn x d m returns the current binding of x in m, or raise exn if no such binding exists.

find_file_from_path [Session_itp]

raise Not_found of path does not appear in session

find_inductive_cases [Decl]
find_its_defn [Pdecl]
find_logic_definition [Decl]
find_meta_tds [Task]
find_nth [Lists]

find_nth p l returns the index of the first element that satifies the predicate p.

find_opt [Exthtbl.Private]

return the first binding or None if none found

find_opt [Exthtbl.S]

return the first binding or None if none found

find_opt [Extmap.S]

find_opt x m returns the Some of the current binding of x in m, or return None if no such binding exists.

find_prop [Decl]
find_prop_decl [Decl]
find_symbol [Args_wrapper]
find_th [Session_itp]
find_variant [Decl]
first [Lists]

first f l returns the first result of the application of f to an element of l that doesn't return None.

first_arg [Whyconf.Args]
first_nth [Lists]

Combination of Lists.first and Lists.find_nth.

flatten_rev [Lists]
flip [Util]
float [Pp]
float_format_equal [Number]
float_value [Pinterp_core]
flush_log [Pinterp_core.Log]

Get the log and empty the log_uc

fma [Mlmpfr_wrapper]
focus_on_loading [Itp_server.Make]
fold [Trans]

Iterating transformations

fold [Opt]

fold f d o returns d if o is None, and f d x if o is Some x

fold [Exthtbl.Private]

Same as Hashtbl.fold

fold [Extset.S]

fold f s a computes (f eN ... (f e1 a)...), where e1 ... eN are the element of s in increasing order.

fold [Extmap.S]

fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.

fold2_inter [Extset.S]

fold2_inter f s1 s2 a computes (f eN ... (f e1 a) ...), where e1 ... eN are the elements of inter s1 s2 in increasing order.

fold2_inter [Extmap.S]

fold the common keys of two map at the same time

fold2_union [Extset.S]

fold2_union f s1 s2 a computes (f eN ... (f e1 a) ...), where e1 ... eN are the elements of union s1 s2 in increasing order.

fold2_union [Extmap.S]

fold the keys which appear in one of the two maps

fold_all_any [Session_itp]

fold_all_any s f acc any folds on all the subnodes of any

fold_all_session [Session_itp]

fold_all_session s f acc folds on the whole session

fold_decl [Trans]
fold_l [Trans]
fold_left [Extset.S]

same as Extset.S.fold but in the order of List.fold_left

fold_left [Extmap.S]

same as Extmap.S.fold but in the order of List.fold_left

fold_lefti [Lists]

Similar to List.fold_left, but with element index passed as extra argument (in 0..len-1).

fold_map [Trans]
fold_map_l [Trans]
fold_premises [Pinterp_core]

Fold the terms in the premises.

fold_product [Lists]

fold_product f acc l1 l2 applies the function f with the accumulator acc on all the pair of elements of l1 and l2; tail-recursive.

fold_product_l [Lists]

Generalization of Lists.fold_product; not tail-recursive.

foldi [Util]
for_all [Extset.S]

for_all p s checks if all the elements of s satisfy the predicate p.

for_all [Extmap.S]

for_all p m checks if all the bindings of the map satisfy the predicate p.

forget_all [Pretty.Printer]

flush id_unique

forget_all [Ident]

forget all idents

forget_cty [Ity]
forget_id [Ident]

forget an ident

forget_pv [Ity]
forget_reg [Ity]
forget_rs [Expr]
forget_tvs [Pretty.Printer]

flush id_unique for type vars

forget_var [Pretty.Printer]

flush id_unique for a variable

forget_xs [Ity]
format [Getopt]

format ~margin opts turns the option list opts into a string that is suitable for usage message.

formatted [Pp]
fprintf_any [Session_itp]
from_channel [Rc]

from_channel cin returns the Rc of the input channel cin.

from_file [Rc]

from_file filename returns the Rc of the file filename.

fs_app [Term]
fs_bool_false [Term]
fs_bool_true [Term]
fs_func_app [Term]

higher-order application symbol

fs_tuple [Term]

n-tuple

fs_void [Expr]
full_support [Number]
funlit [Ident]
G
ge [BigInt]
gen_syntax_arguments_prec [Printer]
get [Loc]

get p returns the file, the line and character numbers of the beginning and the line and character numbers of the end of the given position.

get_any_parent [Session_itp]
get_bool [Rc]

Same as Rc.get_int but on bool.

get_booll [Rc]

Same as Rc.get_intl but on bool.

get_boolo [Rc]

Same as Rc.get_into but on bool.

get_call_result_loc [Ident]

Get the call result location from an attribute.

get_complete_command [Whyconf]

add the extra_options to the command

get_conf_file [Whyconf]

get_conf_file config get the rc file corresponding to this configuration

get_counterexmp [Driver]

Returns true if counterexample should be get for the task (according to meta_get_counterexmp.

get_debug_formatter [Debug]

Get the formatter used when printing debug material.

get_dir [Session_itp]
get_do_rac [Pinterp]

Return true if RAC is enabled in the execution context.

get_editors [Whyconf]

returns the set of editors

get_eid_attr [Ident]

get_eid_attr s searches in the set s an attribute defining an expression identifier, as prefixed by eid_attribute_prefix.

get_element_name [Ident]
get_element_syntax [Pretty]
get_encapsulating_file [Session_itp]
get_encapsulating_theory [Session_itp]
get_env [Pinterp]

Return the environment of an execution context.

get_exec_calls_and_loops [Pinterp_core.Log]

Used for counterexamples.

get_exn [Opt]
get_family [Whyconf.User]

get_family config name Same as Rc.get_family except name must not be prover

get_family [Rc]

get_family rc name returns all the sections of the family name in rc.

get_filename [Driver]

Mangles a filename for the prover of the given driver

get_files [Session_itp]
get_float [Rc]
get_format [Env]

get_format ?format fname returns the format of the given file if None is given.

get_formatted_str [Mlmpfr_wrapper]
get_giant_steps [Pinterp]

Return true if the execution context is configured with giant steps.

get_home_dir [Util]

Return the home directory of the user.

get_hyp_name [Ident]

If attrs contains an attribute of the form "hyp_name:<s>" returns Some <s> or None if no attribute have this form

get_int [Rc]

get_int ?default section key returns the integer value associated to key key.

get_intl [Rc]

get_intl section key returns all the integer values associated to key key.

get_into [Rc]

get_into section key returns the integer value associated to key key if present, and None if missing.

get_loadpath [Env]

returns the loadpath of a given environment

get_log [Pinterp_core.Log]

Get the log

get_lsymbol_or_model_trace_name [Model_parser]

Given a model element me, returns the model_trace attribute if it exists in me.me_attrs, otherwise returns the name of the me.me_lsymbol.

get_main [Whyconf]

get_main config get the main section stored in the Rc file

get_mlw_file [Ptree_helpers.I]
get_mlw_file [Ptree_helpers.F]
get_model_element_name [Ident]

If attributes contain an attribute of the form "model_trace:name(@...)?", return "name".

get_model_elements [Model_parser]
get_model_term_attrs [Model_parser]
get_model_term_loc [Model_parser]
get_model_trace_attr [Ident]

Return an attribute of the form "model_trace:*".

get_model_trace_string [Ident]

If attrs contain an attribute of the form "model_trace:mt_string", return "mt_string".

get_namespace [Theory]
get_new_results [Call_provers]

returns new results from why3server, in an unordered fashion.

get_policies [Whyconf]
get_proof_attempt_ids [Session_itp]
get_proof_attempt_node [Session_itp]
get_proof_attempt_parent [Session_itp]
get_proof_attempts [Session_itp]
get_proof_expl [Session_itp]
get_proof_name [Session_itp]
get_proof_parent [Session_itp]
get_prover_config [Whyconf]

get_prover_config config prover gets the prover config as stored in the config.

get_prover_editor [Whyconf]
get_prover_editors [Whyconf]
get_prover_shortcuts [Whyconf]

return the prover shortcuts

get_prover_upgrade_policy [Whyconf]

get_prover_upgrade config returns a map providing the policy to follow for each absent prover (if it has already been decided by the user and thus stored in the config)

get_provers [Whyconf]

get_provers config get the prover family stored in the Rc file.

get_pvs [Pinterp_core]
get_rac [Pinterp]

Return the RAC engine of the execution context.

get_rac_results [Check_ce]

Given a list of models, return the list of these models together with the results of the execution of normal and giant-step RAC.

get_requests [Itp_server.Protocol]
get_rliteral_map [Printer]
get_section [Whyconf.User]

get_section config name Same as Rc.get_section except name must not be "main"

get_section [Rc]

get_section rc name

get_simple_family [Whyconf.User]

get_family config name Same as Rc.get_simple_family except name must not be prover

get_simple_family [Rc]

get_simple_family rc name returns all the sections of the simple family name in rc.

get_strategies [Whyconf]
get_string [Rc]

Same as Rc.get_int but on string.

get_stringl [Rc]

Same as Rc.get_intl but on string.

get_stringo [Rc]

Same as Rc.get_into but on string.

get_sub_tasks [Session_itp]
get_syntax_map [Printer]
get_task [Session_itp]
get_task_name_table [Session_itp]
get_timings [Debug.Stats]
get_trans_parent [Session_itp]
get_transf_args [Session_itp]
get_transf_name [Session_itp]
get_transformations [Session_itp]
get_undetached_children_no_pa [Controller_itp]
get_used_syms_decl [Decl]

get_used_syms_decl d returns the set of identifiers used (i.e., assumed to be defined before) in d

get_used_syms_ty [Decl]

get_used_syms_ty ty returns the set of identifiers used (i.e., assumed to be defined before) in ty

get_vs [Pinterp_core]
get_written_loc [Ident]

Get the location inside vc_written attribute.

goal [Trans]
goal_iter_proof_attempt [Session_itp]
goal_l [Trans]
graft_proof_attempt [Session_itp]

graft_proof_attempt s id pr file l adds a proof attempt with prover pr and limits l in the session s as a child of the task id.

graft_transf [Session_itp]

graft_transf s id name l tl adds the transformation name as a child of the task id of the session s.

greater_p [Mlmpfr_wrapper]
greaterequal_p [Mlmpfr_wrapper]
gt [BigInt]
H
handle_exn [Getopt]

handle_exn args exn terminates the program after printing the content of the Getopt.GetoptFailure exception.

has_a_model_attr [Ident]

true when ident has one of the attributes above

has_prefix [Strings]

has_prefix pref s returns true if s starts with prefix pref.

has_rac_assume [Ident]

Check if the attributes contain [@RAC:assume].

has_suffix [Strings]

has_suffix suff s returns true if s ends with suffix suff.

hash [Wstdlib.OrderedHashedType]
hash [Loc]
hash [Exthtbl]

the same as Hashtbl.hash

highord_module [Pmodule]
highord_theory [Theory]
hov [Pp]
hterm_generic [Term]
html_char [Pp]
html_string [Pp]

formats the string by escaping special HTML characters quote, double quote, <, > and &

I
id_attr [Ident]

create a duplicate pre-ident with given attributes

id_clone [Ident]

create a duplicate pre-ident

id_compare [Ident]
id_derive [Ident]

create a derived pre-ident (inherit attributes and location)

id_equal [Ident]
id_fresh [Ident]

create a fresh pre-ident

id_hash [Ident]
id_loc [Mlw_printer]

Create a unique dummy location

id_register [Ident]

register a pre-ident (you should never use this function)

id_unique [Ident]

use ident_printer to generate a unique name for ident an optional sanitizer is applied over the printer's sanitizer

id_unique_attr [Ident]

Do the same as id_unique except that it tries first to use the "name:" attribute to generate the name instead of id.id_string

id_user [Ident]

create a localized pre-ident

ident [Ptree_helpers]

ident ?attr ?loc s produce the identifier named s optionally with the given attributes and source location

identity [Trans]
identity_l [Trans]
idle [Controller_itp.Scheduler]

idle prio f registers the function f as a function to be called whenever there is nothing else to do.

ignore_theory [Theory]
import_namespace [Theory]
import_scope [Theory]
import_scope [Pmodule]
incomplete [Pinterp_core]
incr [Debug.Stats]
indent [Pp]

add the indentation at the first line

inf_p [Mlmpfr_wrapper]
init [Lists]
init_config [Whyconf]

init_config ?extra_config conf_file adds the automatically generated part of the configuration, and loads plugins

init_real [Pinterp]

Give a precision on real computation.

init_server [Itp_server.Make]
initialize [Whyconf.Args]
int [Pp]
int_literal [Number]
int_range_equal [Number]
int_value [Pinterp_core]
inter [Extset.S]

inter f s1 s2 computes the intersection of two sets

inter [Extmap.S]

inter f m1 m2 computes a map whose keys is a subset of the intersection of keys of m1 and of m2.

interleave_with_source [Model_parser]

Given a source code and a counterexample model, interleaves the source code with information about the counterexample.

interrupt [Controller_itp.Make]

discards all scheduled proof attempts or transformations, including the ones already running

interrupt_call [Call_provers]

non-blocking function that asks for prover interruption

interrupt_proof_attempts_for_goal [Controller_itp.Make]

discards all scheduled proof attempts for the given goal, including the ones that are already running

is_alias_type_def [Ty]
is_below [Session_itp]
is_detached [Session_itp]
is_e_false [Expr]
is_e_true [Expr]
is_e_void [Expr]
is_eid_attr [Ident]

is_eid_attr a tells whether a is an expression identifier attribute.

is_empty [Exthtbl.Private]

test if the hashtbl is empty

is_empty [Exthtbl.S]

test if the hashtbl is empty

is_empty [Extset.S]

Test whether a set is empty or not.

is_empty [Extmap.S]

Test whether a map is empty or not.

is_fatal [Session_itp]
is_field_id_attr [Ident]

indicates that the related ident is a field name, and its applications should be printed in dotted notation

is_float_type_def [Ty]
is_fs_tuple [Term]
is_fs_tuple_id [Term]
is_id_loc [Mlw_printer]
is_int [BigInt]
is_model_empty [Model_parser]
is_model_trace_attr [Ident]
is_num_elt [Extset.S]

check if the map has the given number of elements

is_num_elt [Extmap.S]

check if the map has the given number of elements

is_prover_known [Whyconf]

test if a prover is detected

is_range_ty [Pinterp_core]

Checks if the argument is a range type

is_range_type_def [Ty]
is_root [Itp_communication]
is_rs_tuple [Expr]
is_ts_tuple [Ty]
is_ts_tuple_id [Ty]
isb_empty [Ity]
iter [Exthtbl.Private]

Same as Hashtbl.iter

iter [Extset.S]

iter f s applies f to all elements of s.

iter [Extmap.S]

iter f m applies f to all bindings in map m.

iter_first [Util]

iter_first iter f returns the first result of f that is inhabitated, when applied on the elements encountered by iterator iter.

iterf [Util]

iterf f min max step

its_bool [Ity]
its_compare [Ity]
its_equal [Ity]
its_func [Ity]
its_hash [Ity]
its_int [Ity]
its_match_args [Ity]
its_match_regs [Ity]
its_pure [Ity]

a pure type symbol is immutable and has no mutable components

its_real [Ity]
its_ref [Pmodule]
its_str [Ity]
its_tuple [Ity]
its_unit [Ity]
ity_affected [Ity]

ity_affected wr ity returns true if the regions of ity are contained in the effect described by wr.

ity_app [Ity]

ity_app s tl rl creates an Ityapp type, if s is immutable, or, an Ityreg type on top of a fresh region, otherwise. If rl is empty, fresh subregions are created when needed.

ity_app_pure [Ity]

ity_app s tl rl creates an Ityapp type.

ity_bool [Ity]
ity_closed [Ity]

a closed type contains no type variables

ity_compare [Ity]
ity_components [Pinterp_core]

Gets the components of an ity

ity_equal [Ity]
ity_equal_check [Ity]
ity_exp_fold [Ity]
ity_fold [Ity]
ity_fragile [Ity]

a fragile type may contain a component with a broken invariant

ity_freeregs [Ity]
ity_freevars [Ity]
ity_freeze [Ity]
ity_frz_regs [Ity]
ity_full_inst [Ity]
ity_func [Ity]
ity_hash [Ity]
ity_int [Ity]
ity_match [Ity]
ity_of_ty [Ity]

fresh regions are created when needed.

ity_of_ty_pure [Ity]

pure snapshots are substituted when needed.

ity_pred [Ity]
ity_purify [Ity]

replaces regions with pure snapshots

ity_r_fold [Ity]
ity_r_occurs [Ity]
ity_r_reachable [Ity]
ity_r_stale [Ity]
ity_rch_fold [Ity]
ity_real [Ity]
ity_reg [Ity]
ity_s_fold [Ity]
ity_str [Ity]
ity_tuple [Ity]
ity_unit [Ity]
ity_v_fold [Ity]
ity_v_occurs [Ity]
ity_var [Ity]
J
join [Strings]

join sep l joins all the strings in l together, in the same order, separating them by sep.

join [Loc]

join p1 p2 attempts to join positions p1 and p2, returning a position that covers both of them.

json_log [Pinterp_core.Log]
json_model [Model_parser]

Counterexample model in JSON format.

json_prover_result [Call_provers]
K
keys [Extmap.S]

Return the list of all keys of the given map.

known_add_decl [Pdecl]
known_add_decl [Decl]
known_id [Pdecl]
known_id [Ident]

Returns true if the printer already knows the id.

known_id [Decl]
kp_attr [Vc]
L
last_non_empty_model [Check_ce]

Select the last non empty model.

lbrace [Pp]
lchevron [Pp]
ld_func_app [Expr]
le [BigInt]
length [Exthtbl.Private]

Same as Hashtbl.length

length [Weakhtbl.S]
less_p [Mlmpfr_wrapper]
lessequal_p [Mlmpfr_wrapper]
lessgreater_p [Mlmpfr_wrapper]
let_rec [Expr]
let_sym [Expr]
let_var [Expr]
libdir [Whyconf]
limit_max [Call_provers]
list_attributes [Ident]
list_flags [Debug]

List the known flags.

list_formats [Env]

list_formats lang returns the list of registered formats that can be translated to lang.

list_map_cont [Term]
list_metas [Theory]
list_model_parsers [Model_parser]
list_printers [Printer]

List registered printers

list_trans [Trans]
list_transforms [Trans]
list_transforms_l [Trans]
list_transforms_with_args [Trans]
list_transforms_with_args_l [Trans]
load_driver_file_and_extras [Driver]

load_driver_file_and_extras main env ~extra_dir file extras loads the driver in file file and with additional drivers in list extras, in the context of the configuration main and environment env.

load_driver_for_prover [Driver]

load_driver main env p loads the driver for prover p, in the context of the configuration main and environment env.

load_plugins [Whyconf]
load_session [Session_itp]

load_session dir load a session in directory dir; all the tasks are initialised to None

loadpath [Whyconf]
local_decls [Task]

takes the result of Task.used_symbols and returns the list of declarations that are not imported with those theories or derived thereof

locate_library [Env]

locate_library env path returns the location of the library file specified by path.

log [Mlmpfr_wrapper]
log_any_call [Pinterp_core.Log]
log_call [Pinterp_core.Log]
log_const [Pinterp_core.Log]
log_exec_ended [Pinterp_core.Log]
log_exec_main [Pinterp_core.Log]
log_failed [Pinterp_core.Log]
log_iter_loop [Pinterp_core.Log]
log_pure_call [Pinterp_core.Log]
log_stucked [Pinterp_core.Log]
log_val [Pinterp_core.Log]
lookup_flag [Debug]

Return the corresponding flag.

lookup_meta [Theory]
lookup_model_parser [Model_parser]
lookup_printer [Printer]
lookup_trans [Trans]
lookup_trans_desc [Trans]
lookup_transform [Trans]
lookup_transform_l [Trans]
lowercase [Strings]
lparen [Pp]
ls_app_inst [Term]
ls_arg_inst [Term]
ls_compare [Term]
ls_decr_of_rec_defn [Expr]
ls_defn_axiom [Decl]
ls_defn_decrease [Decl]

ls_defn_decrease ld returns a list of argument positions (numbered from 0) that ensures a lexicographical structural descent for every recursive call.

ls_defn_of_axiom [Decl]

tries to reconstruct a definition from a defining axiom.

ls_equal [Term]
ls_hash [Term]
ls_of_rs [Expr]

raises Invalid_argument is rs_logic is not an RLls

ls_ref_cons [Pmodule]
ls_ref_proj [Pmodule]
ls_ty_freevars [Term]
lsquare [Pp]
lt [BigInt]
M
make_from_int [Mlmpfr_wrapper]
make_from_str [Mlmpfr_wrapper]
make_ls_defn [Decl]
make_record [Decl]
make_record_pattern [Decl]
make_record_update [Decl]
make_zero [Mlmpfr_wrapper]
map [Exthtbl.Private]

a shortcut less efficient than possible

map [Exthtbl.S]

a shortcut less efficient than possible

map [Extmap.S]

map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.

map_filter [Extmap.S]

Same as Extmap.S.map, but may remove bindings.

map_fold [Opt]
map_fold_left [Lists]
map_fold_right [Lists]
map_join_left [Lists]
mapi [Util]
mapi [Extmap.S]

Same as Extmap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.

mapi_filter [Extmap.S]

Same as Extmap.S.mapi, but may remove bindings.

mapi_filter_fold [Extmap.S]

Same as Extmap.S.mapi_fold, but may remove bindings.

mapi_fold [Extmap.S]

fold and map at the same time

mark_as_obsolete [Controller_itp.Make]
mark_obsolete [Session_itp]

mark_obsolete s id marks id as obsolete in s

mask_adjust [Ity]
mask_equal [Ity]
mask_ghost [Ity]
mask_of_pv [Ity]
mask_spill [Ity]
mask_union [Ity]
max [Mlmpfr_wrapper]
max [BigInt]
max_binding [Extmap.S]

Same as Extmap.S.min_binding, but returns the largest binding of the given map.

max_elt [Extset.S]

Return the largest element of the given set or raise Not_found if the set is empty.

mem [Exthtbl.Private]

Same as Hashtbl.mem

mem [Weakhtbl.S]
mem [Extset.S]

mem x s returns true if s contains x, and false otherwise.

mem [Extmap.S]

mem x m returns true if m contains a binding for x, and false otherwise.

memlimit [Whyconf]
memo [Exthtbl.S]

convenience function, memoize a function

memoize [Weakhtbl.S]
memoize_option [Weakhtbl.S]
memoize_rec [Weakhtbl.S]
merge [Extset.S]

merge f s1 s2 computes a set whose elts is a subset of elts of s1 and of s2.

merge [Extmap.S]

merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

merge_files [Session_itp]

merge_files env ses old_ses merges the file sections of session s with file sections of the same name in old session old_ses.

merge_files_gen [Session_itp]

same as merge_files but takes the extra argument ~reparse_file_fun providing a customized method to reconstruct the theories to attach to files.

merge_known [Pdecl]
merge_known [Decl]
meta_coercion [Theory]
meta_equal [Theory]
meta_float [Theory]
meta_get_counterexmp [Driver]

Set in drivers that generate counterexamples

meta_hash [Theory]
meta_projection [Theory]
meta_proved_wf [Theory]

meta used to declare than a given predicate symbol is proved well-founded

meta_range [Theory]
meta_realized_theory [Printer]

Meta used for implementing modular realization of theories.

meta_record [Theory]
meta_remove_def [Printer]

Meta used to mark in a task function that must be removed before printing

meta_remove_logic [Printer]

Meta used to mark in a task function that must be removed before printing

meta_remove_prop [Printer]

Meta used to mark in a task proposition that must be removed before printing

meta_remove_type [Printer]

Meta used to mark in a task type that must be removed before printing

meta_syntax_literal [Printer]

Meta used to mark in a task literals that will be printed particularly.

meta_syntax_logic [Printer]

Meta used to mark in a task function that are associated with a syntax.

meta_syntax_type [Printer]

Meta used to mark in a task type that are associated with a syntax.

min [Mlmpfr_wrapper]
min [BigInt]
min_binding [Extmap.S]

Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.

min_elt [Extset.S]

Return the smallest element of the given set or raise Not_found if the set is empty.

minus [BigInt]
mk_check_term [Rac.Why]

Metas are applied to all tasks, the tasks are first reduce using trans, and if this is insufficient for deciding the term, checked using why_prover.

mk_check_term_lit [Rac.Why]

mk_rac_lit cnf env ?metas ?trans ?prover ?try_negate () configures the term reduction of RAC.

mk_cntr_ctx [Pinterp_core]

Construct a new Pinterp_core.cntr_ctx with a snapshot of the environment env.

mk_compute_term [Rac.Why]
mk_compute_term_lit [Rac.Why]

Create a compute_term function.

mk_ctx [Pinterp]

Create an execution context.

mk_empty_env [Pinterp_core]
mk_empty_env [Pinterp]

Pinterp_core.env repeated here for convenience.

mk_filter_prover [Whyconf]
mk_proxy_decl [Expr]

mk_proxy_decl ~ghost e returns a pair (ld,v) providing a fresh variable v that can be used as a substitute for expression e.

mk_rac [Pinterp_core]

Plain constructor for Pinterp_core.rac, ignore_incomplete is false by default.

mk_rac [Pinterp]

Pinterp_core.mk_rac repeated here for convenience.

mk_tds [Task]
mk_why_prover [Rac.Why]
mlw_file_of_sexp [Ptree]
mlw_language [Pmodule]
mlw_language_builtin [Pmodule]
mod0 [Debug.Stats]
mod1 [Debug.Stats]
mod2 [Debug.Stats]
mod_impl [Pmodule]
mod_impl_register [Pmodule]
model_for_positions_and_decls [Model_parser]

Given a model and a list of source-code positions returns model that contains only elements from the input model that are on these positions plus for every file in the model, elements that are in the positions of function declarations.

model_of_exec_log [Check_ce]

model_of_exec_log ~original_model log) populates a Model_parser.model from an execution log log

model_projected_attr [Ident]
model_vc_post_attr [Ident]
mterm_generic [Term]
mul [Mlmpfr_wrapper]
mul [BigInt]
mul_int [BigInt]
multibind_pvs [Pinterp_core]
multiplier [Controller_itp.Scheduler]

Number of allowed task given to why3server is this number times the number of allowed proc on the machine.

N
named [Trans]

give transformation a name without registering

nan_p [Mlmpfr_wrapper]
neg [Mlmpfr_wrapper]
neg_int [Number]
neg_real [Number]
newline [Pp]
newline2 [Pp]
next_enum [Extmap.S]

get the next step of the enumeration

next_ge_enum [Extmap.S]

get the next (or same) step of the enumeration which key is greater or equal to the given key

next_pos [Mlw_printer]

Generate a unique location.

notImplemented [Printer]

Should be used by the printer for handling partial implementation

nothing [Pp]
notify [Itp_server.Protocol]
ns_find_its [Pmodule]
ns_find_ls [Theory]
ns_find_ns [Theory]
ns_find_ns [Pmodule]
ns_find_pr [Theory]
ns_find_prog_symbol [Pmodule]
ns_find_pv [Pmodule]
ns_find_rs [Pmodule]
ns_find_ts [Theory]
ns_find_xs [Pmodule]
nt_attr [Vc]
num_digits [BigInt]
num_value [Pinterp_core]
O
of_int [BigInt]
of_list [Extset.S]

construct a set from a list of elements

of_list [Extmap.S]

construct a map from a list of bindings.

of_string [BigInt]
oldify_varl [Pinterp_core]

Prepare a variant for later call with Pinterp_core.check_variant.

on_cloned_theory [Trans]
on_cloned_theory [Task]
on_flag [Trans]

on_flag m ft def arg takes an exclusive meta m of type [MTstring], a hash table ft, a default flag value def, and an argument arg.

on_flag_t [Trans]
on_meta [Trans]
on_meta [Task]
on_meta_excl [Trans]
on_meta_excl [Task]
on_syntax_map [Printer]
on_tagged_ls [Trans]
on_tagged_ls [Task]
on_tagged_pr [Trans]
on_tagged_pr [Task]
on_tagged_ts [Trans]
on_tagged_ts [Task]
on_tagged_ty [Trans]
on_tagged_ty [Task]
on_used_theory [Trans]
on_used_theory [Task]
one [BigInt]
one_binder [Ptree_helpers]
op_cut [Ident]
op_equ [Ident]
op_get [Ident]
op_infix [Ident]
op_lcut [Ident]
op_neq [Ident]
op_prefix [Ident]
op_rcut [Ident]
op_set [Ident]
op_tight [Ident]
op_update [Ident]
open_file [Typing]
open_file_and_formatter [Pp]
open_formatter [Pp]
open_ls_defn [Decl]
open_ls_defn_cb [Decl]
open_module [Typing]
open_post [Ity]
open_post_with [Ity]
open_scope [Typing]
open_scope [Theory]
open_scope [Pmodule]
opt_config [Whyconf.Args]
option_list [Loc.Args]

Print the list of flags if requested (in this case return true).

option_list [Debug.Args]

Print the list of flags if requested (in this case return true).

oracle_dummy [Pinterp_core]

Always returns in None.

oracle_of_model [Check_ce]

Create an oracle from a (prover model-derived) candidate counterexample.

oracle_quant_var [Rac]

Derive an oracle for quantified variables from a normal oracle.

oracle_quant_var_dummy [Rac]

Always returns in None.

oty_compare [Ty]
oty_cons [Ty]
oty_equal [Ty]
oty_freevars [Ty]
oty_hash [Ty]
oty_inst [Ty]
oty_match [Ty]
oty_type [Ty]
overload_of_rs [Pmodule]
P
pa_proved [Session_itp]
pad_right [Strings]

Chop or pad the given string on the right up to the given length.

par [Trans]

parallelize transformations: par l will duplicate the current task in n new tasks, with n the length of l, and apply to each of this new task the corresponding transformation in l

parse_all [Getopt]

parse_all ~i opts extra args parses all the arguments from args, starting from index i (1 by default), calling Getopt.parse_one in turn.

parse_filter_prover [Whyconf]

parse the string representing a filter_prover: "name,version,altern", "name,version" -> "name,version,^.*", "name,,altern" -> "name,^.*,altern", "name" -> "name,^.*,^.*" regexp must start with ^.

parse_many [Getopt]

parse_many opts args i parses arguments from args starting at index i, calling Getopt.parse_one in turn.

parse_one [Getopt]

parse_one opts args i parses argument args.(i) using the option list opts.

parse_record [Decl]

parse_record kn field_list takes a list of record field assignments, checks it for well-formedness and returns the corresponding constructor, the full list of projection symbols, and the map from projection symbols to assigned values.

part [Lists]

part cmp l returns the list of the congruence classes with respect to cmp.

partial [Ity]
partition [Extset.S]

partition p s returns a pair of sets (s1, s2), where s1 contains all the elements of s that satisfy the predicate p, and s2 is the map with all the elements of s that do not satisfy p.

partition [Extmap.S]

partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.

pat [Ptree_helpers]
pat_all [Term]
pat_any [Term]
pat_app [Term]
pat_as [Term]
pat_fold [Term]
pat_map [Term]
pat_or [Term]
pat_var [Term]
pat_var [Ptree_helpers]
pat_wild [Term]
pd_bool [Pdecl]
pd_equ [Pdecl]
pd_func [Pdecl]
pd_func_app [Pdecl]
pd_ignore_term [Pdecl]
pd_int [Pdecl]
pd_real [Pdecl]
pd_str [Pdecl]
pd_tuple [Pdecl]
plugins [Whyconf]
pluginsdir [Whyconf]
pn_proved [Session_itp]
post_of_expr [Expr]
pow_int_pos [BigInt]
pow_int_pos_bigint [BigInt]
pp_decl [Mlw_printer]

Printer for declarations

pp_expr [Mlw_printer]

Printer for expressions

pp_mlw_file [Mlw_printer]

Printer for mlw files

pp_mode [Pinterp_core.Log]
pp_pattern [Mlw_printer]

Printer for patterns

pp_position [Loc]

pp_position fmt loc formats the position loc in the given formatter, in a human readable way, that is: either "filename", line l, characters bc--ec if the position is on a single line,, or "filename", line bl, character bc to line el, character ce if the position is multi-line. The file name is not printed if empty.

pp_position_no_file [Loc]

Similar to pp_position but do not show the file name.

pp_pty [Mlw_printer]

Printer for types

pp_term [Mlw_printer]

Printer for terms

pprinter [Pretty.Printer]

printer for identifiers of proposition

pr_equal [Decl]
pr_hash [Decl]
pred [BigInt]
prefix [Lists]

prefix n l returns the first n elements of l.

preid_name [Ident]
prepare_edition [Controller_itp.Make]

prepare_edition c ?file id pr prepare for editing the proof of node id with prover pr.

prepare_task [Driver]

Apply driver's transformations to the task

print [Extset.S]
print0 [Pp]
print_attr [Pretty.Printer]
print_attrs [Pretty.Printer]
print_binop [Pretty.Printer]
print_cexp [Expr]
print_classification_log_or_model [Check_ce]

Print classification log or the model, when the model is bad or incomplete (When the prover model is printed and ~json:`Values is given, only the values are printed as JSON.)

print_concrete_term [Model_parser]
print_cs [Pretty.Printer]
print_cs_qualified [Pretty.Printer]
print_cty [Ity]
print_data_decl [Pretty.Printer]
print_decl [Pretty.Printer]
print_decoded [Ident]
print_expr [Expr]
print_filter_prover [Whyconf]
print_id_attrs [Pretty.Printer]

prints attributes and location of an ident (but not the ident itself)

print_in_base [Number]

print_in_base radix digits fmt i prints the value of non-negative i in base radix.

print_in_file [Pp]
print_in_file_no_close [Pp]
print_ind_decl [Pretty.Printer]
print_int_constant [Number]
print_interface [Printer]
print_iter1 [Pp]
print_iter2 [Pp]

print_iter2 iter sep1 sep2 print1 print2 fmt t iter iterator on t : 'c print1 k sep2 () print2 v sep1 () print1 sep2 () ...

print_iter22 [Pp]

print_iter22 iter sep print fmt t iter iterator on t : 'c print k v sep () print k v sep () ...

print_its [Ity]
print_ity [Ity]
print_ity_full [Ity]
print_let_defn [Expr]
print_list [Pp]
print_list_delim [Pp]
print_list_next [Pp]
print_list_opt [Pp]
print_list_or_default [Pp]
print_list_par [Pp]
print_list_pre [Pp]
print_list_suf [Pp]
print_loc_as_attribute [Pretty.Printer]
print_log [Pinterp_core.Log]
print_logic_decl [Pretty.Printer]
print_logic_result [Pinterp]
print_ls [Pretty.Printer]
print_ls_qualified [Pretty.Printer]
print_meta [Trans]

print_meta f m is an identity transformation that prints every meta m in the task if flag d is set

print_meta_arg [Pretty.Printer]
print_meta_arg_type [Pretty.Printer]
print_meta_desc [Theory]
print_model [Model_parser]

Prints the counterexample model.

print_model_classification [Check_ce]

Print the classification with the classification log or model.

print_model_human [Model_parser]

Same as print_model but is intended to be human readable.

print_model_kind [Model_parser]
print_module [Pmodule]
print_msg [Itp_communication]
print_namespace [Pretty.Printer]
print_next_data_decl [Pretty.Printer]
print_next_ind_decl [Pretty.Printer]
print_next_logic_decl [Pretty.Printer]
print_notify [Itp_communication]
print_option [Pp]
print_option_or_default [Pp]
print_pair [Pp]
print_pair_delim [Pp]

print_pair_delim left_delim middle_delim right_delim

print_param_decl [Pretty.Printer]
print_pat [Pretty.Printer]
print_pdecl [Pdecl]
print_pkind [Pretty.Printer]
print_pr [Pretty.Printer]
print_pr_qualified [Pretty.Printer]
print_prelude [Printer]

Print a prelude

print_proofAttemptID [Session_itp]
print_proofNodeID [Session_itp]
print_prop_decl [Pretty.Printer]
print_prover [Whyconf]
print_prover_answer [Call_provers]
print_prover_parseable_format [Whyconf]
print_prover_result [Call_provers]

Pretty-print a prover_result.

print_prover_upgrade_policy [Whyconf]
print_pv [Ity]
print_pvty [Ity]
print_qualid [Typing]
print_quant [Pretty.Printer]
print_rac_result [Check_ce]

Print the result state of a RAC execution with the execution log

print_rac_result_state [Check_ce]

Print a RAC result state

print_real_constant [Number]
print_reg [Ity]
print_reg_name [Ity]
print_request [Itp_communication]
print_rs [Expr]
print_sequent [Pretty.Printer]
print_session [Controller_itp]
print_spec [Ity]
print_status [Controller_itp]
print_strategy_status [Controller_itp]
print_string [Pp]
print_task [Pretty.Printer]
print_task [Driver]

Prepare the task for the prover and prints it

print_task_prepared [Driver]
print_tdecl [Pretty.Printer]
print_term [Pretty.Printer]
print_th [Pretty.Printer]
print_th_prelude [Printer]

print the prelude of the theory present in the task

print_th_qualified [Pretty.Printer]
print_theory [Pretty.Printer]
print_theory [Driver]

produce a realization of the given theory using the given driver

print_trans_status [Controller_itp]
print_ts [Pretty.Printer]
print_ts_qualified [Pretty.Printer]
print_tv [Pretty.Printer]
print_tv_qualified [Pretty.Printer]
print_ty [Pretty.Printer]
print_ty_decl [Pretty.Printer]
print_ty_qualified [Pretty.Printer]
print_unit [Pmodule]
print_value [Pinterp_core]
print_vs [Pretty.Printer]
print_vs_qualified [Pretty.Printer]
print_vsty [Pretty.Printer]

prints ``variable : type''

print_xs [Ity]
prio_binop [Pretty]

priorities of each binary operators

protect_on [Pretty]

add parentheses around when first arugment is true.

prove_buffer_prepared [Driver]

Call prover on a task already prepared and printed in the buffer.

prove_task [Driver]
prove_task_prepared [Driver]

Call prover on a task prepared by prepare_task.

prover_parseable_format [Whyconf]
proxy_attr [Ident]
proxy_attrs [Expr]
ps_acc [Term]

acc r x means x is accessible for relation r

ps_app [Term]
ps_equ [Term]

equality predicate

ps_ignore [Term]
ps_wf [Term]

well_founded r means relation r is well-founded, that is, all elements are accessible

purefun_value [Pinterp_core]
pv_affected [Ity]

pv_affected wr pv returns true if the regions of pv are contained in the effect described by wr.

pv_compare [Ity]
pv_equal [Ity]
pv_hash [Ity]
pvs_affected [Ity]

pvs_affected wr pvs returns the set of pvsymbols from pvs whose regions are contained in the effect described by wr.

pvs_of_vss [Ity]
Q
qualid [Ptree_helpers]

qualid l produces the qualified identifier given by the path l, a list in the style of ["int";"Int"]

query_call [Call_provers]

non-blocking function that reports any new updates from the server related to a given prover call.

query_syntax [Printer]
R
rac_dummy [Pinterp_core]

Dummy RAC that always raises Failure.

rac_execute [Check_ce]

Execute a call to the program function given by the rsymbol using normal or giant-step RAC, using the given model as an oracle for program parameters (and during giant-steps).

range_value [Pinterp_core]

Returns a range value, or raises Incomplete if the value is outside the range.

rbrace [Pp]
rc_of_config [Whyconf]
rchevron [Pp]
read_channel [Env]

read_channel ?format lang env file ch returns the contents of ch in language lang.

read_config [Whyconf]

read_config conf_file : If conf_file is given, then if it is an empty string, an empty config is loaded,, if the file doesn't exist, Rc.CannotOpen is raised,, otherwise the content of the file is parsed and returned., If conf_file is None and the WHY3CONFIG environment variable exists, then the above steps are executed with the content of the variable (possibly empty)., If neither conf_file nor WHY3CONFIG are present, the file $HOME/.why3.conf (or $USERPROFILE/.why3.conf under Windows) is checked for existence: if present, the content is parsed and returned,, otherwise, we return the built-in default_config with a default configuration filename.

read_config_rc [Whyconf]

read_config_rc conf_file same rule than Whyconf.init_config but just returned the parsed Rc file

read_file [Session_itp]
read_file [Env]

an open-close wrapper around read_channel

read_library [Env]

read_library lang env path returns the contents of the library file specified by path.

read_module [Pmodule]
read_theory [Env]

read_theory env path th returns the theory path.th from the library.

real_literal [Number]

real_literal ~radix ~neg ~int ~frac ~exp builds the real value given by the mantissa int.frac and exponent exp.

real_value [Pinterp_core]
real_value [Number]

real_value ~pow2 ~pow5 n builds the value n * 2 ^ pow2 * 5 ^ pow5.

record_timing [Debug.Stats]

Wrap a function call with this function in order to record its execution time in a global table.

ref_attr [Pmodule]
ref_module [Pmodule]
reg_compare [Ity]
reg_equal [Ity]
reg_equal_check [Ity]
reg_exp_fold [Ity]
reg_fold [Ity]
reg_freeregs [Ity]
reg_freevars [Ity]
reg_freeze [Ity]
reg_full_inst [Ity]
reg_hash [Ity]
reg_match [Ity]
reg_r_fold [Ity]
reg_r_occurs [Ity]
reg_r_reachable [Ity]
reg_r_stale [Ity]
reg_rch_fold [Ity]
reg_s_fold [Ity]
reg_v_fold [Ity]
reg_v_occurs [Ity]
register [Debug.Stats]
register_any_call [Pinterp_core]
register_call [Pinterp_core]
register_call [Decl]
register_const_init [Pinterp_core]
register_ended [Pinterp_core]
register_env_transform [Trans]
register_env_transform_l [Trans]
register_exec_main [Pinterp_core]
register_failure [Pinterp_core]
register_flag [Debug]

Return the corresponding flag, after registering it if needed.

register_format [Env]

register_format ~desc lang fname exts parser registers a new format fname for files with extensions from the string list exts (without the separating dot).

register_info_flag [Debug]

Return the corresponding flag, after registering it if needed.

register_int [Debug.Stats]
register_iter_loop [Pinterp_core]
register_language [Env]

register_language parent convert adds a leaf to the language tree.

register_meta [Theory]
register_meta_excl [Theory]

With exclusive metas, each new meta cancels the previous one.

register_model_parser [Model_parser]
register_observer [Controller_itp.Make]

records a hook that will be called with the number of waiting tasks, scheduled tasks, and running tasks, each time these numbers change

register_printer [Printer]

register_printer ~desc name printer Register the printer printer so that drivers of prover can mention it using name.

register_pure_call [Pinterp_core]
register_remove_field [Model_parser]
register_res_value [Pinterp_core]
register_stucked [Pinterp_core]
register_transform [Trans]
register_transform_l [Trans]
register_transform_with_args [Trans]
register_transform_with_args_l [Trans]
register_used_value [Pinterp_core]
register_warning [Loc]

register_warning name desc registers a new warning under the given name with the given description.

relevant_for_counterexample [Ident]

true when ident is a constant value that should be used for counterexamples generation.

reload_files [Controller_itp]

reload_files c returns a pair (o,d): o true means there are obsolete goals, d means there are missed objects (goals, transformations, theories or files) that are now detached in the session returned.

reloc [Loc]

reloc l returns the location with character num augmented by !current_offset.

remove [Weakhtbl.S]
remove [Extset.S]

remove x s returns a set containing the same elements as s, except for x.

remove [Extmap.S]

remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.

remove_left [Extset.S]

remove_left s x is the same as remove x s.

remove_model_attrs [Ident]

Remove the counter-example attributes from an attribute set

remove_prefix [Strings]

remove_prefix pref s removes the prefix pref from s.

remove_proof_attempt [Session_itp]

remove_proof_attempt s id pr removes the proof attempt from the prover pr from the proof node id of the session s

remove_prop [Printer]

create a meta declaration for a proposition to remove

remove_subtree [Session_itp]

remove_subtree s a ~removed ~notification remove the subtree originating from node a in session s.

remove_subtree [Controller_itp]

remove a subtree of the session, taking care of not removing any proof attempt in progress.

remove_suffix [Strings]

remove_suffix suff s removes the suffix suff from s.

remove_transformation [Session_itp]

remove_transformation s id removes the transformation id from the session s

remove_unused_in_term [Term]

remove_unused_in_term polarity t removes from t the occurrences and uses of symbols marked with attribute Ident.unused_attr.

remove_user_policy [Whyconf.User]
rename_file [Session_itp]

rename_file s from_file to_file renames the file section in session s named from_file into to_file

replace [Extmap.S]

replace e x v m binds x to v in m if x is already bound, and raises e otherwise.

replay [Controller_itp.Make]

This function reruns all the proofs of the session under the given any (None means the whole session), and produces a report comparing the results with the former ones.

replay_print [Controller_itp.Make]
report_cntr [Pinterp_core]
report_cntr [Pinterp]
report_cntr_body [Pinterp_core]
report_cntr_head [Pinterp_core]
report_cntr_title [Pinterp_core]
report_eval_result [Pinterp]

Report an evaluation result

report_verdict [Check_ce]

Describe a verdict in a short sentence.

reset_proofs [Controller_itp.Make]

Remove each proof attempt or transformation that are below proved goals.

resolve_driver_name [Driver]

resolve_driver_name main dir ?extra_dir name resolves the driver name name into a file name.

restore_its [Ity]

raises Not_found if the argument is not a its_ts

restore_module [Pmodule]

retrieves a module from its underlying theory raises Not_found if no such module exists

restore_module_id [Pmodule]

retrieves a module from a program symbol defined in it Raises Not_found if the ident was never declared in/as a module.

restore_path [Theory]

restore_path id returns the triple (library path, theory, qualified symbol name) if the ident was ever introduced in a theory declaration.

restore_path [Pmodule]

restore_path id returns the triple (library path, module, qualified symbol name) if the ident was ever introduced in a module declaration.

restore_pv [Ity]

raises Not_found if the argument is not a pv_vs

restore_rs [Expr]

raises Not_found if the argument is not a rs_logic

restore_theory [Theory]
result_id [Ity]

result_id ?loc ?ql () returns a fresh pre-identifier whose name is appropriately chosen with respect to the optionally given list of post-conditions ("result" by default, as hard-coded in this module implementation).

return [Trans]
rev_filter [Lists]
rev_map_fold_left [Lists]
rev_split [Strings]
rewrite [Trans]

rewrite f t1 t2 appends to task t1 the declarations in t2 in which each top level formula t is replaced by f t *

rewriteTF [Trans]
rint [Mlmpfr_wrapper]
root_node [Itp_communication]
rparen [Pp]
rs_compare [Expr]
rs_equal [Expr]
rs_false [Expr]
rs_func_app [Expr]
rs_ghost [Expr]
rs_hash [Expr]
rs_kind [Expr]
rs_ref [Pmodule]
rs_ref_cons [Pmodule]
rs_ref_proj [Pmodule]
rs_true [Expr]
rs_tuple [Expr]
rs_void [Expr]
rsquare [Pp]
run_strat_on_goal [Controller_itp.Make]

run_strat_on_goal c id strat executes asynchronously the strategy strat on the goal id.

run_strategy_on_goal [Controller_itp.Make]

run_strategy_on_goal c id strat executes asynchronously the strategy strat on the goal id.

running_provers_max [Whyconf]
S
sanitizer [Ident]

generic sanitizer taking a separate encoder for the first letter

sanitizer' [Ident]

generic sanitizer taking a separate encoder for the first and last letter

save_config [Whyconf]

save_config config save the configuration

save_session [Session_itp]

save_session s Save the session s

schedule_edition [Controller_itp.Make]

schedule_edition c id pr ~callback ~notification runs the editor for prover pr on proofnode id on a file whose name is automatically generated.

schedule_proof_attempt [Controller_itp.Make]

schedule_proof_attempt ?proof_script_filename c id p ~timelimit ~callback ~notification schedules a proof attempt for a goal specified by id with the prover p with time limit timelimit; the function callback will be called each time the proof attempt status changes.

schedule_transformation [Controller_itp.Make]

schedule_transformation c id cb schedules a transformation for a goal specified by id; the function cb will be called each time the transformation status changes.

search_attribute_value [Ident]

search_attribute_value f attrs applies f to the attributes in attr and returns the first inhabited result, if any, or None otherwise.

search_model_element_call_result [Model_parser]

search_model_element_call_result m oid searches for a model element that holds the return value for a call with id oid.

search_model_element_for_id [Model_parser]

search_model_element_for_id m ?loc id searches for a model element for identifier id, at the location id.id_loc, or at loc, when given.

select_model [Check_ce]

Select one of the given models.

select_model_from_giant_step_rac_results [Check_ce]

Select a model based on the giant-step RAC execution results.

select_model_from_verdict [Check_ce]

Select a model based on the classification (itself based on the normal and giant-step RAC executions).

select_model_last_non_empty [Check_ce]

Select the last, non-empty model in the incremental list of models.

semi [Pp]
seq [Trans]
seq_l [Trans]
session_iter_proof_attempt [Session_itp]
session_iter_proof_node_id [Session_itp]
set [Weakhtbl.S]
set_argument_parsing_functions [Args_wrapper]
set_bool [Rc]

Same as Rc.set_int but on bool.

set_booll [Rc]

Same as Rc.set_intl but on bool.

set_boolo [Rc]

Same as Rc.set_into but on bool.

set_column [Pp.Ansi]
set_compare [Extmap.S]

set_compare = compare (fun _ _ -> 0)

set_datadir [Whyconf]
set_debug_formatter [Debug]

Set the formatter used when printing debug material.

set_default_editor [Whyconf.User]
set_default_editor [Whyconf]
set_default_prec [Mlmpfr_wrapper]
set_diff [Extmap.S]

set_diff = diff (fun _ _ _ -> None)

set_disjoint [Extmap.S]

set_disjoint = disjoint (fun _ _ _ -> false)

set_editors [Whyconf]

replace the set of editors

set_emax [Mlmpfr_wrapper]
set_emin [Mlmpfr_wrapper]
set_equal [Extmap.S]

set_equal = equal (fun _ _ -> true)

set_family [Whyconf.User]

set_family config name Same as Rc.set_family except name must not be prover

set_family [Rc]

set_family rc name family adds all the sections in family using the associated string as argument of the family name in rc.

set_file [Loc]

set_file f lb sets the file name to f in lb.

set_flag [Debug]
set_flags_selected [Loc.Args]

Set the flags selected by warning or a shortcut.

set_flags_selected [Debug.Args]

Set the flags selected by debug_all, debug or a shortcut.

set_float [Rc]
set_infer_invs [Vc]
set_int [Rc]

set_int ?default section key value associates value to key in the section, unless value is equal to default.

set_inter [Extmap.S]

set_inter = inter (fun _ x _ -> Some x)

set_intl [Rc]

set_intl section key lvalue associates to key all the values of lvalue.

set_into [Rc]

set_int section key value associates value to key in the section if it is not None.

set_libdir [Whyconf]
set_limits [Whyconf.User]
set_limits [Whyconf]
set_load_default_plugins [Whyconf]

Set if the plugins in the default path should be loaded

set_loadpath [Whyconf]
set_main [Whyconf]

set_main config main replace the main section by the given one

set_model_files [Model_parser]
set_partial_config [Itp_server]
set_partial_config [Controller_itp]

edit a minimal part of the configuration that should be safe to edit during execution of the server (provers config, editors)

set_plugins [Whyconf]
set_policies [Whyconf]
set_proof_script [Session_itp]
set_prover_editor [Whyconf.User]
set_prover_editors [Whyconf]
set_prover_shortcuts [Whyconf]

set the prover shortcuts

set_prover_upgrade_policy [Whyconf.User]
set_prover_upgrade_policy [Whyconf]

set_prover_upgrade c p cpu sets or updates the policy to follow if the prover p is absent from the system

set_provers [Whyconf]

set_provers config provers replace all the family prover by the one given

set_section [Whyconf.User]

set_section config name Same as Rc.set_section except name must not be "main"

set_section [Rc]

set_section rc name section adds a section section with name name in rc.

set_session_max_tasks [Controller_itp]

sets the maximum number of proof tasks that can be running at the same time.

set_session_memlimit [Controller_itp]

sets the default memlimit for proof attempts

set_session_prover_upgrade_policy [Controller_itp]
set_session_timelimit [Controller_itp]

sets the default timelimit for proof attempts

set_simple_family [Whyconf.User]

set_simple_family config name Same as Rc.set_simple_family except name must not be prover

set_simple_family [Rc]

set_simple_family rc name family adds all the section in family using the associated string as argument of the family name in rc.

set_stdlib [Whyconf]

Set if the standard library should be added to loadpath

set_string [Rc]

Same as Rc.set_int but on string.

set_stringl [Rc]

Same as Rc.set_intl but on string.

set_stringo [Rc]
set_submap [Extmap.S]

set_submap = submap (fun _ _ _ -> true)

set_union [Extmap.S]

set_union = union (fun _ x _ -> Some x)

set_warning_hook [Loc]

The default behavior is to emit warning on standard error, with position on a first line (if any) and message on a second line.

sexp_of_mlw_file [Ptree]
sign [BigInt]
signbit [Mlmpfr_wrapper]
simple_comma [Pp]
singleton [Trans]
singleton [Extset.S]

singleton x returns the one-element set that contains x.

singleton [Extmap.S]

singleton x y returns the one-element map that contains a binding y for x.

slash [Pp]
sn_decode [Ident]
snapshot [Pinterp_core]
snapshot_oldies [Pinterp_core]

Used for checking function variants

snapshot_vsenv [Pinterp_core]
sort_log_by_loc [Pinterp_core.Log]
sp_attr [Vc]
space [Pp]
split [Strings]

split c s splits s into substrings, taking as delimiter the character c, and returns the list of substrings.

split [Lists]

split n l returns (prefix n l, chop n l).

split [Extset.S]

split x s returns a triple (l, mem, r), where l is the set with all the elements of s that are strictly less than x; r is the set with all the elements of s that are strictly greater than x; mem is true if x belongs to s and false otherwise.

split [Extmap.S]

split x m returns a triple (l, data, r), where l is the map with all the bindings of m whose key is strictly less than x; r is the map with all the bindings of m whose key is strictly greater than x; data is None if m contains no binding for x, or Some v if m binds v to x.

split_theory [Task]

split_theory th s t returns the list of proof tasks that correspond to goals in th, in the order of appearance.

split_version [Util]

Split a version string into its components.

sprint_decl [Printer]
sprint_tdecl [Printer]
sprinter [Pretty.Printer]

printer for identifiers of variables and functions

sprintf [Pp]
sprintf_wnl [Pp]
sqrt [Mlmpfr_wrapper]
stack_trace [Debug]

"stack_trace" flag.

star [Pp]
start_enum [Extmap.S]

start the enumeration of the given map

start_ge_enum [Extmap.S]

start the enumeration of the given map at the first key which is greater or equal than the given one

stats [Debug]
stdlib_path [Whyconf]
stepregexp [Call_provers]

stepregexp s n creates a regular expression to match the number of steps.

sterm_generic [Term]
stop_split [Term]
store [Trans]
string [Pp]
string_list_of_qualid [Typing]
string_of [Pp]
string_of_rac_result_state [Check_ce]

String of the RAC result state variant

string_of_verdict [Check_ce]

The variant name of the verdict as a string.

string_of_wnl [Pp]

same as Pp.string_of but without newline

string_unique [Ident]

Uniquify string

string_value [Pinterp_core]
stuck [Pinterp_core]

Raise an exception Pinterp_core.Stuck with a formatted string.

stuck_for_fail [Pinterp_core]

Raise an exception Pinterp_core.Stuck and register in the log for a Fail (cntr_ctx, t).

sub [Mlmpfr_wrapper]
sub [BigInt]
subdomain [Extmap.S]

subdomain pr m returns the set of keys of bindings in m that satisfy predicate pr

submap [Extmap.S]

submap pr m1 m2 verifies that all the keys in m1 are in m2 and that for each such binding pr is verified.

subnormalize [Mlmpfr_wrapper]
subset [Extset.S]

subset s1 s2 tests whether the set s1 is a subset of s2.

subst_concrete_term [Model_parser]
succ [BigInt]
suffix_attr_name [Ident]

Add a suffix to all "name" attributes of attrs

syntax_arguments [Printer]

syntax_arguments templ print_arg fmt l prints in the formatter fmt the list l using the syntax templ, and the printer print_arg

syntax_arguments_prec [Printer]

syntax_arguments_prec templ print_arg prec_list fmt l prints in the formatter fmt the list l using the template templ, the printer print_arg, and the precedence list prec_list

syntax_arguments_typed [Printer]

syntax_arguments_typed templ print_arg print_type t fmt l prints in the formatter fmt the list l using the template templ, the printers print_arg and print_type.

syntax_arguments_typed_prec [Printer]

syntax_arguments_typed_prec templ print_arg print_type t prec_list fmt l prints in the formatter fmt the list l using the template templ, the printers print_arg and print_type, and the precedence list prec_list.

syntax_arity [Printer]

syntax_arity s returns the largest i such that the parameter %i occurs in s.

syntax_float_literal [Printer]
syntax_literal [Printer]

create a meta declaration for the builtin syntax of a literal

syntax_logic [Printer]

create a meta declaration for the builtin syntax of a function

syntax_map [Driver]
syntax_range_literal [Printer]
syntax_type [Printer]

create a meta declaration for the builtin syntax of a type

system_path [Session_itp]

the system-dependent absolute path associated to that file

T
t_all [Term.TermTF]
t_all [Term]
t_and [Term]
t_and_asym [Term]
t_and_asym_l [Term]
t_and_asym_simp [Term]
t_and_asym_simp_l [Term]
t_and_l [Term]
t_and_l_concrete [Model_parser]
t_and_simp [Term]
t_and_simp_l [Term]
t_any [Term.TermTF]
t_any [Term]
t_app [Term]
t_app_fold [Term]
t_app_infer [Term]
t_app_map [Term]
t_app_partial [Term]

t_app_partial ls tl tyl oty produces a closure of ls and applies it to tl using t_func_app.

t_attr_add [Term]
t_attr_copy [Term]

t_attr_copy src dst returns the term dst with attributes and locations augmented with those of term src

t_attr_remove [Term]
t_attr_set [Term]
t_binary [Term]
t_binary_simp [Term]
t_bool_false [Term]
t_bool_true [Term]
t_case [Term]
t_case_close [Term]
t_case_close_simp [Term]
t_case_fold [Term]
t_case_simp [Term]
t_clone_bound_id [Term]
t_close_bound [Term]
t_close_branch [Term]
t_close_quant [Term]
t_closed [Term]
t_closure [Term]

t_closure ls tyl oty returns a type-instantiated lambda-term \xx:tyl.(ls xx : oty), or ls : oty if ls is a constant.

t_compare [Term]
t_compare_generic [Term]
t_compare_strict [Term]
t_const [Term]
t_eps [Term]
t_eps_close [Term]
t_equ [Term]
t_equ_simp [Term]
t_equal [Term]
t_equal_generic [Term]
t_equal_strict [Term]
t_exists [Term]
t_exists_close [Term]
t_exists_close_merge [Term]

t_forall_close_merge vs f puts a universal quantifier over f; merges variable lists if f is already universally quantified; reuses triggers of f, if any, otherwise puts no triggers.

t_exists_close_simp [Term]
t_exists_simp [Term]
t_false [Term]
t_fold [Term.TermTF]

t_fold fnT fnF = t_fold (t_selecti fnT fnF)

t_fold [Term]
t_forall [Term]
t_forall_close [Term]
t_forall_close_merge [Term]
t_forall_close_simp [Term]
t_forall_simp [Term]
t_freepvs [Ity]

raises Not_found if the term contains a free variable which is not a pv_vs

t_freevars [Term]
t_func_app [Term]

value-typed application

t_func_app_beta [Term]

t_func_app_beta f a applies f to a performing beta-reduction when f is a lambda-term.

t_func_app_beta_l [Term]
t_func_app_l [Term]

value-typed application

t_gen_map [Term]
t_hash [Term]
t_hash_generic [Term]
t_hash_strict [Term]
t_if [Term]
t_if_simp [Term]
t_iff [Term]
t_iff_simp [Term]
t_implies [Term]
t_implies_simp [Term]
t_int_const [Term]
t_is_lambda [Term]

t_is_lambda t returns true if t is a lambda-term.

t_iter [Term]
t_lambda [Term]

t_lambda vl tr e produces a term eps f. (forall vl [tr]. f@vl = e) or eps f. (forall vl [tr]. f@vl = True <-> e if e is prop-typed.

t_let [Term]
t_let_close [Term]
t_let_close_simp [Term]

t_let_close_simp v t1 t2 constructs the term let v=t1 in t2 but if the term t1 is simple enough, then it produces the equivalent term t2[v<-t2] instead.

t_let_close_simp_keep_var [Term]

t_let_close_simp_keep_var v t1 t2 does the same as t_let_close_simp but when the second term is simple enough and keep is true, it produces the term let v=t1 in t2[v<-t2], keeping thus the variable v even if it is not used after the in

t_let_simp [Term]

similar to t_let_close_simp but on a term_bound

t_let_simp_keep_var [Term]

similar to t_let_close_simp_keep_var but on a term_bound

t_map [Term.TermTF]

t_map fnT fnF = t_map (t_select fnT fnF)

t_map [Term]
t_map_cont [Term.TermTF]
t_map_cont [Term]

t_map_cont is t_map in continuation-passing style

t_map_fold [Term.TermTF]
t_map_fold [Term]
t_map_sign [Term.TermTF]
t_map_sign [Term]

t_map_sign passes a polarity parameter, unfolds if-then-else and iff

t_map_simp [Term.TermTF]
t_map_simp [Term]

t_map_simp reconstructs the term using simplification constructors

t_nat_const [Term]

t_nat_const n builds the constant integer term n, n must be non-negative

t_neq [Term]
t_neq_simp [Term]
t_not [Term]
t_not_simp [Term]
t_occurs [Term]
t_open_bound [Term]
t_open_bound_cb [Term]
t_open_bound_with [Term]

t_open_bound_with t tb opens the binding tb and immediately replaces the corresponding bound variable with t

t_open_branch [Term]
t_open_branch_cb [Term]
t_open_lambda [Term]

t_open_lambda t returns a triple (vl,tr,e), such that t is equal to t_lambda vl tr e.

t_open_lambda_cb [Term]

the same as t_open_lambda but returns additionally an instance of t_lambda that restores the original term if applied to the physically same arguments.

t_open_quant [Term]
t_open_quant_cb [Term]
t_or [Term]
t_or_asym [Term]
t_or_asym_l [Term]
t_or_asym_simp [Term]
t_or_asym_simp_l [Term]
t_or_l [Term]
t_or_simp [Term]
t_or_simp_l [Term]
t_peek_bound [Term]
t_peek_branch [Term]
t_peek_quant [Term]
t_pred_app [Term]

prop-typed application

t_pred_app_beta [Term]

t_pred_app_beta f a applies f to a performing beta-reduction when f is a lambda-term.

t_pred_app_beta_l [Term]
t_pred_app_l [Term]

prop-typed application

t_prop [Term]

t_prop t checks that t is prop-typed and returns t

t_quant [Term]
t_quant_close [Term]
t_quant_close_simp [Term]
t_quant_simp [Term]
t_real_const [Term]
t_replace [Term]
t_s_all [Term]
t_s_any [Term]
t_s_fold [Term]
t_s_map [Term]
t_select [Term.TermTF]

t_select fnT fnF t is fnT t if t is a value, fnF t otherwise

t_selecti [Term.TermTF]

t_selecti fnT fnF acc t is t_select (fnT acc) (fnF acc) t

t_string_const [Term]
t_subst [Term]

t_subst m t substitutes variables in t by the variable mapping m

t_subst_single [Term]

t_subst_single v t1 t2 substitutes variable v in t2 by t1

t_subst_types [Term]

t_subst_types mt mv t substitutes type variables of term t by mapping mt.

t_true [Term]
t_tuple [Term]
t_ty_check [Term]

t_ty_check t ty checks that the type of t is ty

t_ty_fold [Term]
t_ty_freevars [Term]
t_ty_map [Term]
t_ty_subst [Term]

t_ty_subst mt mv t substitutes simultaneously type variables by mapping mt and term variables by mapping mv in term t

t_type [Term]

t_type t checks that t is value-typed and returns its type

t_undefined [Pinterp_core]
t_v_all [Term]
t_v_any [Term]
t_v_count [Term]
t_v_fold [Term]
t_v_map [Term]
t_v_occurs [Term]
t_var [Term]
t_vars [Term]
t_void [Expr]
tag [Wstdlib.TaggedType]
tag [Weakhtbl.Weakey]
tag_equal [Weakhtbl]
tag_hash [Weakhtbl]
tapp [Ptree_helpers]
task_clone [Task]
task_decls [Task]
task_equal [Task]
task_fold [Task]
task_goal [Task]
task_goal_fmla [Task]
task_hash [Task]
task_hd_equal [Task]
task_hd_hash [Task]
task_iter [Task]
task_known [Task]
task_meta [Task]
task_separate_goal [Task]

task_separate_goal t returns a pair (g,t') where g is the goal of the task t and t' is the rest.

task_tdecls [Task]
tconst [Ptree_helpers]
td_equal [Theory]
td_hash [Theory]
tdecl [Trans]
tdecl_l [Trans]
tds_compare [Task]
tds_empty [Task]
tds_equal [Task]
tds_hash [Task]
term [Ptree_helpers]
term_branch_size [Term]

term_branch_size t is the size of the term in the given term branch

term_of_expr [Expr]
term_of_post [Expr]
term_of_value [Pinterp_core]

Convert a value into a term.

term_size [Term]

term_size t is the size, i.e.

term_value [Pinterp_core]
terminal_has_color [Util]

Indicates if standard output supports ANSI terminal color codes (i.e.

test_flag [Debug]
test_noflag [Debug]
tgoal [Trans]
tgoal_l [Trans]
th_proved [Session_itp]
theory_goals [Session_itp]
theory_iter_proof_attempt [Session_itp]
theory_name [Session_itp]

Theory

theory_parent [Session_itp]
timelimit [Whyconf]
timeout [Controller_itp.Scheduler]

timeout ~ms f registers the function f as a function to be called every ms milliseconds.

timeregexp [Call_provers]

Converts a regular expression with special markers '%h','%m', '%s','%i' (for milliseconds) into a value of type timeregexp

tn_proved [Session_itp]
to_channel [Rc]

to_channel cout rc writes the Rc rc to the output channel out.

to_file [Rc]

to_file filename rc writes the Rc rc to the file filename.

to_formatter [Rc]

to_formatter fmt rc writes the Rc rc to the formatter fmt.

to_int [BigInt]
to_prop [Term]

to_prop t converts the term t of type bool or prop into a term of type prop.

to_small_integer [Number]
to_string [BigInt]
toggle_flag [Debug]
total [Ity]
tprinter [Pretty.Printer]

printer for identifiers of type symbols

tr_equal [Term]
tr_fold [Term.TermTF]
tr_fold [Term]
tr_map [Term.TermTF]
tr_map [Term]
tr_map_fold [Term.TermTF]
tr_map_fold [Term]
trace_goal [Trans]
transfer_loc [Loc]

transfer_loc from to sets the lex_start_p and lex_curr_p fields of to to the ones of from.

translate [Extset.S]

translate f s translates the elements in the set s by the function f.

translate [Extmap.S]

translate f m translates the keys in the map m by the function f.

try1 [Loc]
try2 [Loc]
try3 [Loc]
try4 [Loc]
try5 [Loc]
try6 [Loc]
try7 [Loc]
ts_bool [Ty]
ts_compare [Ty]
ts_equal [Ty]
ts_func [Ty]
ts_hash [Ty]
ts_int [Ty]
ts_match_args [Ty]
ts_real [Ty]
ts_ref [Pmodule]
ts_str [Ty]
ts_tuple [Ty]
ts_unit [Ity]

Same as Ty.ts_tuple 0.

ttrue [Util]

Constant function true

tuple_module [Pmodule]
tuple_theory [Theory]
tuple_theory_name [Theory]
tv_compare [Ty]
tv_equal [Ty]
tv_hash [Ty]
tv_of_string [Ty]
tvar [Ptree_helpers]
ty_all [Ty]
ty_any [Ty]
ty_app [Ty]
ty_app_arg [Pinterp_core]

ty_app_arg ts n ty returns the n-th argument of the type application of ts in ty.

ty_bool [Ty]
ty_closed [Ty]

ty_closed ty returns true when ty is not polymorphic

ty_compare [Ty]
ty_equal [Ty]
ty_equal_check [Ty]
ty_fold [Ty]
ty_freevars [Ty]
ty_func [Ty]
ty_hash [Ty]
ty_inst [Ty]
ty_int [Ty]
ty_map [Ty]

traverse only one level of constructor, if you want full traversal you need to call those function inside your function

ty_match [Ty]

ty_match sigma0 pat sub returns a type substitution sigma such that sigma pat = sub.

ty_match_args [Ty]
ty_of_ity [Ity]
ty_pred [Ty]
ty_real [Ty]
ty_s_all [Ty]
ty_s_any [Ty]
ty_s_fold [Ty]
ty_s_map [Ty]

visits every symbol of the type

ty_str [Ty]
ty_tuple [Ty]
ty_unit [Ity]
ty_v_all [Ty]
ty_v_any [Ty]
ty_v_fold [Ty]
ty_v_map [Ty]

visits every variable of the type

ty_var [Ty]
type_def_fold [Ty]
type_def_map [Ty]
type_expr_in_muc [Typing]
type_fmla_in_namespace [Typing]
type_mlw_file [Typing]
type_term_in_namespace [Typing]
U
uncapitalize [Strings]
undefined_value [Pinterp_core]
underscore [Pp]
union [Extset.S]

union f s1 s2 computes the union of two sets

union [Extmap.S]

union f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

union [Coercion]

union s1 s2 merges the coercions from s2 into s1 (as a new set of coercions) this is asymetric: a coercion from s2 may hide a coercion from s1

unit_binder [Ptree_helpers]
unit_module [Pmodule]
unit_value [Pinterp_core]
unknown_to_known_provers [Whyconf]

return others, same name, same version

unset_flag [Debug]
unsupported [Printer]
unsupportedDecl [Printer]

Should be used by the printer for handling the error of an unsupported declaration

unsupportedPattern [Printer]

Should be used by the printer for handling the error of an unsupported pattern

unsupportedTerm [Printer]

Should be used by the printer for handling the error of an unsupported term

unsupportedType [Printer]

Should be used by the printer for handling the error of an unsupported type

unused_attr [Ident]

attribute for unused variables kept for counterexample generation

unused_suffix [Ident]

Suffix for unused variables kept for counterexample generation

update_goal_node [Session_itp]

updates the proved status of the given goal node.

update_proof_attempt [Session_itp]

update_proof_attempt ?obsolete s id pr st update the status of the corresponding proof attempt with st.

update_section [Whyconf.User]
update_trans_node [Session_itp]

updates the proved status of the given transformation node.

uppercase [Strings]
use [Ptree_helpers.I]

see use_import above

use [Ptree_helpers.F]

see use_import above

use [Ptree_helpers]

use l produces the equivalent of "use (import) path" where path is denoted by l

use_export [Theory]
use_export [Task]
use_export [Pmodule]
used_symbols [Task]

takes the result of Task.used_theories and returns a map from symbol names to their theories of origin

used_theories [Task]

returns a map from theory names to theories themselves

user_position [Loc]

user_position f bl bc el ec builds the source position for file f, starting at line bl and character bc and ending at line el and character ec.

useraxiom_attr [Ident]
V
v_desc [Pinterp_core]
v_ty [Pinterp_core]
val_enum [Extmap.S]

get the current key value pair of the enumeration, return None if the enumeration reach the end

values [Extmap.S]

Return the list of all values of the given map.

vc [Vc]
vs_compare [Term]
vs_equal [Term]
vs_graph_drop [Decl]
vs_graph_let [Decl]
vs_graph_pat [Decl]
vs_hash [Term]
W
wait_on_call [Call_provers]

blocking function that waits until the prover finishes.

warn_axiom_abstract [Theory]
warn_clone_not_abstract [Theory]
warn_missing_diverges [Vc]
warn_missing_field [Rc]
warn_useless_at [Typing]
warning [Loc]

warning ~id ~loc fmt emits a warning in the given formattter fmt.

warning_clone_not_abstract [Theory]
wb_attr [Vc]
why3_keywords [Pretty]

the list of all WhyML keywords.

why3_regexp_of_string [Whyconf]
with_location [Loc]
with_marker [Mlw_printer]

Inform a printer to include the message (default: "XXX") as a comment before the expression, term, or pattern with the given location.

with_push_premises [Pinterp_core]

with_push_premises p f calls f in a new scope of premises in p.

without_warning [Loc]

Given a warning identifier, execute an inner operation with the warning temporarily disabled.

wnl [Pp]
wp_attr [Vc]
wrap [Args_wrapper]
wrap_and_register [Args_wrapper]
wrap_l [Args_wrapper]
X
xs_compare [Ity]
xs_equal [Ity]
xs_hash [Ity]
Z
zero [BigInt]
zero_p [Mlmpfr_wrapper]