Index of values


_done [Session_scheduler.Todo]
one task is stopped with information

A
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_builtin [Env]
add_builtin lang builtin adds new builtin libraries to lang.
add_data_decl [Task]
add_data_decl [Theory]
add_decl [Mlw_module]
add_decl [Task]
add_decl [Theory]
add_decl_with_tuples [Theory]
add_external_proof [Session]
add_file [Session_scheduler.Make]
add_file es f adds the file with filename f in the proof session, the file name must be given relatively to the session dir given to open_session
add_file [Session]
Add a real file by its filename.
add_ind_decl [Task]
add_ind_decl [Theory]
add_invariant [Mlw_module]
add_invariant [Mlw_decl]
add_logic_decl [Task]
add_logic_decl [Theory]
add_meta [Mlw_module]
add_meta [Task]
add_meta [Theory]
add_metas_to_goal [Session]
keys are normally generated
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 [Task]
add_param_decl [Theory]
add_pdecl [Mlw_module]
add_pdecl ~wp m d adds declaration d in module m.
add_plugin [Whyconf]
add_proof_to_goal [Session]
add_prop_decl [Task]
add_prop_decl [Theory]
add_registered_metas [Session]
Metas
add_registered_transformation [Session]
Apply a real transformation by its why3 name, raise Session.NoTask if the goal doesn't contain a task.
add_tdecl [Task]
add_transf_to_goal [Session]
add_transformation [Session]
Add a transformation by its subgoals
add_ty_decl [Task]
add_ty_decl [Theory]
all [Util]
all2 [Util]
all2_fn [Util]
all2_fn pr z a b return true if pr a b is true, otherwise raise FoldSkip
all_fn [Util]
all_fn pr z a return true if pr a is true, otherwise raise FoldSkip
alld [Util]
any [Util]
any2 [Util]
any2_fn [Util]
any2_fn pr z a b return false if pr a b is false, otherwise raise FoldSkip
any_fn [Util]
any_fn pr z a return false if pr a is false, otherwise raise FoldSkip
anyd [Util]
append_to_model_element_name [Ident]
The returned set of labels will contain the same set of labels as argument labels except that a label of the form "model_trace:*@*" will be "model_trace:*to_append@*".
append_to_model_trace_label [Ident]
The returned set of labels will contain the same set of labels as argument labels except that a label of the form "model_trace:*" will be "model_trace:*to_append".
apply [Lists]
apply f [a1;..;an] returns (f a1)@...@(f an)
apply [Opt]
apply2 [Opt]
asym_label [Term]
aty_app [Mlw_ty]
apply a function specification to a variable argument
aty_filter [Mlw_ty]
remove from the given arrow every effect that is covered neither by the arrow's arguments nor by the given pvset
aty_full_inst [Mlw_ty]
the substitution must cover not only aty_vars aty but also every type variable and every region in aty_spec
aty_of_expr [Mlw_expr]
aty_pvset [Mlw_ty]
raises Not_found if the spec contains non-pv variables
aty_vars [Mlw_ty]
aty_vars_match [Mlw_ty]
this only compares the types of arguments and results, and ignores the spec.

B
base_language [Env]
base_language is the root of the tree of supported languages.
bindings [Extmap.S]
Return the list of all bindings of the given map.
bool_theory [Theory]
bounded_split [Strings]
bounded_split c s n do the same as split c s but splits into n substring at most.
builtin_theory [Theory]

C
call_on_buffer [Driver]
call_on_buffer [Call_provers]
Call a prover on the task printed in the Buffer.t given.
call_on_file [Call_provers]
cancel [Session_scheduler.Make]
cancel a marks all proofs under a as obsolete
cancel_scheduled_proofs [Session_scheduler.Make]
cancels all currently scheduled proof attempts.
capitalize [Strings]
cardinal [Extset.S]
Return the number of elements in a set.
cardinal [Extmap.S]
Return the number of bindings of a map.
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]
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_all [Session_scheduler.Make]
check_all session callback reruns all the proofs of the session, and reports for all proofs the current result and the new one (does not change the session state).
check_exhaustive [Rc]
check_exhaustive section keys check that only the keys in keys appear inside the section section
check_post [Mlw_ty]
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]
removes the first n elements of a list; raises Invalid_argument if the list is not long enough
chop_last [Lists]
removes (and returns) the last element of a list
clean [Session_scheduler.Make]
clean a removes failed attempts below a where there at least one successful attempt or transformation
clear [Weakhtbl.S]
clone_data_decl [Mlw_decl]
clone_export [Mlw_module]
clone_export [Task]
clone_export [Theory]
clone_export_theory [Mlw_module]
clone_meta [Theory]
clone_meta td_meta sm produces from td_meta a new Meta tdecl instantiated with respect to sm.
clone_theory [Theory]
close_module [Mlw_module]
close_namespace [Mlw_module]
close_namespace [Theory]
close_theory [Theory]
cntexample [Whyconf]
compare [Stdlib.OrderedHashedType]
compare [Extset.S]
Total ordering between sets.
compare [Extmap.S]
Total ordering between maps.
compare [Lists]
compare [Opt]
cons [Lists]
const [Util]
const2 [Util]
const3 [Util]
convert_unknown_prover [Session_scheduler.Make]
Same as Session_tools.convert_unknown_prover
convert_unknown_prover [Session_tools]
try to add new proof_attempt with known provers for all proof attempt with unknown provers
copy [Weakhtbl.S]
copy [Strings]
copy_external_proof [Session]
copy an external proof.
copy_metas [Session]
keys are copied
copy_proof [Session]
copy_transf [Session]
create [Session_scheduler.OBSERVER]
returns a fresh key, a new child of the given parent if any
create [Session_scheduler.Todo]
create init step callback
create [Weakhtbl.S]
create [Strings]
create_data_decl [Mlw_decl]
create_data_decl [Decl]
create_decl [Theory]
create_env [Env]
creates an environment from a "loadpath", a list of directories containing loadable Why3/WhyML/etc files
create_exn_decl [Mlw_decl]
create_fsymbol [Term]
create_fun_defn [Mlw_expr]
create_ident_printer [Ident]
start a new printer with a sanitizing function and a blacklist
create_ind_decl [Decl]
create_inst [Theory]
create_itysymbol [Mlw_ty]
creation of a symbol for type in programs
create_label [Ident]
create_let_decl [Mlw_decl]
create_let_defn [Mlw_expr]
create_let_ps_defn [Mlw_expr]
create_let_pv_defn [Mlw_expr]
create_logic_decl [Decl]
create_lsymbol [Term]
create_meta [Theory]
create_module [Mlw_module]
create_null_clone [Theory]
create_param_decl [Decl]
create_plsymbol [Mlw_expr]
create_post [Mlw_ty]
create_prop_decl [Decl]
create_prsymbol [Decl]
create_psymbol [Mlw_expr]
create_psymbol [Term]
create_pvsymbol [Mlw_ty]
create_rec_decl [Mlw_decl]
create_rec_defn [Mlw_expr]
create_region [Mlw_ty]
create_session [Session]
create a new session in the given directory.
create_tag [Weakhtbl]
create_theory [Theory]
create_tvsymbol [Ty]
create_ty_decl [Mlw_decl]
create_ty_decl [Decl]
create_tysymbol [Ty]
create_use [Theory]
create_val_decl [Mlw_decl]
create_vsymbol [Term]
create_xsymbol [Mlw_ty]

D
d_equal [Decl]
d_hash [Decl]
datadir [Whyconf]
debug [Session]
The debug flag "session"
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.
decl_fold [Decl.DeclTF]
decl_fold [Decl]
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
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_shortcut [Debug.Args]
Option for setting a specific flag
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.
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.
domain [Extmap.S]
domain m returns the set of keys of binding m
dprintf [Debug]
Print only if the flag is set
dummy_tag [Weakhtbl]

E
e_abstract [Mlw_expr]
e_absurd [Mlw_expr]
e_any [Mlw_expr]
e_app [Mlw_expr]
e_app e el builds the application of e to arguments el.
e_arrow [Mlw_expr]
e_arrow p argl res instantiates the program function symbol p into a program expression having the given types of the arguments and the result.
e_assert [Mlw_expr]
e_assign [Mlw_expr]
e_case [Mlw_expr]
e_const [Mlw_expr]
e_false [Mlw_expr]
e_find [Mlw_expr]
e_find pr e returns a sub-expression of e satisfying pr.
e_fold [Mlw_expr]
e_for [Mlw_expr]
e_ghost [Mlw_expr]
e_if [Mlw_expr]
e_label [Mlw_expr]
e_label_add [Mlw_expr]
e_label_copy [Mlw_expr]
e_lapp [Mlw_expr]
e_lazy_and [Mlw_expr]
e_lazy_or [Mlw_expr]
e_let [Mlw_expr]
e_loop [Mlw_expr]
e_not [Mlw_expr]
e_now [Mlw_wp]
e_plapp [Mlw_expr]
e_purify [Mlw_expr]
e_raise [Mlw_expr]
e_rec [Mlw_expr]
e_true [Mlw_expr]
e_try [Mlw_expr]
e_value [Mlw_expr]
e_void [Mlw_expr]
edit_proof [Session_scheduler.Make]
edits the given proof attempt using the appropriate editor
edit_proof_v3 [Session_scheduler.Make]
edits the given proof attempt using the appropriate editor but don't modify the session
editor_by_id [Whyconf]
return the configuration of the editor if found, otherwise return Not_found
eff_assign [Mlw_ty]
eff_compare [Mlw_ty]
eff_diverge [Mlw_ty]
eff_empty [Mlw_ty]
eff_equal [Mlw_ty]
eff_full_inst [Mlw_ty]
eff_ghostify [Mlw_ty]
eff_is_empty [Mlw_ty]
eff_raise [Mlw_ty]
eff_refresh [Mlw_ty]
eff_remove_raise [Mlw_ty]
eff_reset [Mlw_ty]
eff_stale_region [Mlw_ty]
eff_union [Mlw_ty]
eff_write [Mlw_ty]
elements [Extset.S]
Return the list of all elements of the given set.
empty [Rc]
An empty Rc
empty [Extset.S]
The empty set.
empty [Extmap.S]
The empty map.
empty_inst [Theory]
empty_limit [Call_provers]
empty_ns [Theory]
empty_section [Rc]
An empty section
ends_with [Strings]
test if a string ends with another
env_tag [Env]
equal [Stdlib.OrderedHashedType]
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 [Lists]
equal [Opt]
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]

F
ffalse [Util]
ffalse constant function false
file_iter [Session]
file_iter_proof_attempt [Session]
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
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 uniq prover that verify the filter.
filter_proof_attempt [Session_tools]
remove all the proof attempts that do not satisfy the given predicate
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 [Weakhtbl.S]
find [Exthtbl.Private]
Same as Hashtbl.find
find [Extmap.S]
find x m returns the current binding of x in m, or raises Not_found if no such binding exists.
find_clone_tds [Task]
find_constructors [Mlw_decl]
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_definition [Mlw_decl]
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_inductive_cases [Decl]
find_invariant [Mlw_decl]
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]
first [Lists]
first f l returns the first result of the application of f to an element of l which doesn't return None.
first_nth [Lists]
The combinaison of list_first and list_find_nth.
flag_desc [Debug]
get the description of the flag
flatten_rev [Lists]
flip [Util]
fold [Weakhtbl.S]
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.
fold [Opt]
fold f d o returns d if o is None, and f d x if o is Some x
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_sub_goals_of_theory [Session]
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.map, List.iter and List.fold_left, but with element index passed as extra argument (in 0..len-1)
fold_product [Lists]
fold_product f acc l1 l2 apply the function f with the accumulator acc on all the pair of elements of l1 and l2 tail-recursive
fold_product_l [Lists]
generalisation of Lists.fold_product; not tail-recursive
fold_right [Opt]
foldi [Util]
foldk [Weakhtbl.S]
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 [Ident]
forget all idents
forget_id [Ident]
forget an ident
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_at [Mlw_wp]
fs_bool_false [Term]
fs_bool_true [Term]
fs_func_app [Term]
fs_now [Mlw_wp]
fs_old [Mlw_wp]
fs_tuple [Term]
fs_void [Mlw_expr]
full_invariant [Mlw_wp]

G
get [Opt]
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]
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_debug_formatter [Debug]
Get the formatter used when printing debug material
get_def [Opt]
get_edited_as_abs [Session]
return the edited filename after concatenation to session_dir
get_editors [Whyconf]
returns the set of editors
get_exn [Opt]
get_family [Whyconf]
get_family config name Same as Rc.get_family except name must not be prover
get_family [Rc]
get_family rc name return all the sections of the family name in rc
get_home_dir [Rc]
get_home_dir () returns the home dir of the user
get_int [Rc]
get_int ~default section key one key to one value
get_intl [Rc]
get_intl ~default section key one key to many value
get_into [Rc]
get_known [Mlw_module]
get_known [Theory]
get_loadpath [Env]
returns the loadpath of a given environment
get_main [Whyconf]
get_main config get the main section stored in the Rc file
get_mem [Call_provers]
get_model_element_name [Ident]
If labels contain a label of the form "model_trace:name@*", return "name".
get_model_trace_label [Ident]
Return a label of the form "model_trace:*".
get_model_trace_string [Ident]
If labels contain a label of the form "model_trace:mt_string", return "mt_string".
get_namespace [Mlw_module]
get_namespace [Theory]
get_policies [Whyconf]
get_project_dir [Session]
find the session which corresponds to the given file or return directly the given directory; return Not_found if the file or the directory doesn't exists
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_rev_decls [Theory]
get_section [Whyconf]
Access to the Rc.t
get_section [Rc]
get_section rc name
get_simple_family [Rc]
get_simple_family rc name return all the sections of the simple family name in rc
get_steps [Call_provers]
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]
get_theory [Mlw_module]
get_time [Call_provers]
get_used_provers [Session]
Get the set of provers which appear in the session
goal_expl [Session]
Return the explication of a goal
goal_iter [Session]
goal_iter_leaf_goal [Session]
iter all the goals which are a leaf (no transformations are applied on it)
goal_iter_proof_attempt [Session]
goal_task [Session]
Return the task of a goal.
goal_task_option [Session]
Return the task of a goal.
goal_task_or_recover [Session]
same as goal_task but recover the task goal and all the one of this theory if this goal task have been released

H
has_prefix [Strings]
has_prefix pref s returns true if s s starts with prefix pref
hash [Stdlib.OrderedHashedType]
hash [Exthtbl]
the same as Hashtbl.hash
highord_theory [Theory]

I
id_clone [Ident]
create a duplicate pre-ident
id_compare [Ident]
id_derive [Ident]
create a derived pre-ident (inherit labels and location)
id_equal [Ident]
id_fresh [Ident]
create a fresh pre-ident
id_hash [Ident]
id_lab [Ident]
create a duplicate pre-ident with given labels
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_user [Ident]
create a localized pre-ident
idle [Session_scheduler.OBSERVER]
a handler for a delayed function, that can be called when there is nothing else to do.
idle [Session_scheduler.Base_scheduler]
incr [Debug.Stats]
inhabited [Opt]
init [Session_scheduler.OBSERVER]
run after the creation
init [Session_scheduler.Make]
init max
initialize [Whyconf.Args]
inst_constructors [Mlw_decl]
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.
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_empty_sm [Theory]
is_fs_tuple [Term]
is_fs_tuple_id [Term]
is_info_flag [Debug]
test if the flag is an info flag
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_ts_tuple [Ty]
is_ts_tuple_id [Ty]
iter [Session]
iter [Weakhtbl.S]
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 [Opt]
iter_file [Session]
iter_goal [Session]
iter_metas [Session]
iter_proof_attempt [Session]
iter_session [Session]
iter_theory [Session]
iter_theory f th applies f to all root goals of theory th
iter_transf [Session]
iterf [Util]
iterf f min max step
iteri [Lists]
iterk [Weakhtbl.S]
its_clone [Mlw_ty]
its_equal [Mlw_ty]
its_hash [Mlw_ty]
ity_all [Mlw_ty]
ity_any [Mlw_ty]
ity_app [Mlw_ty]
ity_app_fresh [Mlw_ty]
ity_bool [Mlw_ty]
ity_closed [Mlw_ty]
ity_equal [Mlw_ty]
ity_equal_check [Mlw_ty]
ity_fold [Mlw_ty]
ity_full_inst [Mlw_ty]
ity_has_inv [Mlw_ty]
ity_hash [Mlw_ty]
ity_immutable [Mlw_ty]
ity_int [Mlw_ty]
ity_map [Mlw_ty]
ity_mark [Mlw_decl]
ity_match [Mlw_ty]
ity_nonghost_reg [Mlw_ty]
ity_of_expr [Mlw_expr]
ity_of_ty [Mlw_ty]
replaces every Tyapp with Itypur
ity_of_vty [Mlw_ty]
ity_pur [Mlw_ty]
ity_s_all [Mlw_ty]
ity_s_any [Mlw_ty]
ity_s_fold [Mlw_ty]
ity_subst_empty [Mlw_ty]
ity_unit [Mlw_ty]
ity_var [Mlw_ty]

J
join [Strings]
join sep l joins all the strings in l together, in the same order, separating them by sep

K
keep_on_simp_label [Term]
key_any [Session]
return the key of an element of the tree
keys [Extmap.S]
Return the list of all keys of the given map.
known_add_decl [Mlw_decl]
known_add_decl [Decl]
known_id [Mlw_decl]
known_id [Decl]

L
lab_compare [Ident]
lab_equal [Ident]
lab_hash [Ident]
lemma_label [Mlw_wp]
length [Weakhtbl.S]
length [Exthtbl.Private]
Same as Hashtbl.length
libdir [Whyconf]
limit_max [Call_provers]
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]
load_driver [Driver]
loads a driver from a file
load_plugins [Whyconf]
load_prover [Session]
load a prover
loadpath [Whyconf]
local_decls [Task]
takes the result of 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.
lookup_flag [Debug]
get the flag
lookup_meta [Theory]
lookup_nonghost_reg [Mlw_ty]
ls_app_inst [Term]
ls_arg_inst [Term]
ls_compare [Term]
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_ty_freevars [Term]

M
main_loop [Session_scheduler.Base_scheduler]
main_loop () run the main loop.
make_ls_defn [Decl]
make_ppattern [Mlw_expr]
make_record [Decl]
make_record_pattern [Decl]
make_record_update [Decl]
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 [Opt]
map2 [Opt]
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 [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 [Lists]
mapi [Util]
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_theory [Mlw_wp]
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 [Weakhtbl.S]
mem [Exthtbl.Private]
Same as Hashtbl.mem
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_config [Whyconf]
merge_config config filename merge the content of filename into config
merge_known [Mlw_decl]
merge_known [Decl]
meta_equal [Theory]
meta_hash [Theory]
metas_iter [Session]
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.
mk_filter_prover [Whyconf]
mk_limit [Call_provers]
mk_tds [Task]
mlw_language [Mlw_module]
mod0 [Debug.Stats]
mod1 [Debug.Stats]
mod2 [Debug.Stats]

N
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
notify [Session_scheduler.OBSERVER]
notify modification of node of the session
notify_timer_state [Session_scheduler.OBSERVER]
this function is called when timer state changes.
notify_timer_state [Session_scheduler.Base_scheduler]
These functions have the properties required by OBSERVER
ns_find_its [Mlw_module]
ns_find_ls [Mlw_module]
ns_find_ls [Theory]
ns_find_ns [Mlw_module]
ns_find_ns [Theory]
ns_find_pl [Mlw_module]
ns_find_pr [Theory]
ns_find_prog_symbol [Mlw_module]
ns_find_ps [Mlw_module]
ns_find_pv [Mlw_module]
ns_find_ts [Mlw_module]
ns_find_ts [Theory]
ns_find_type_symbol [Mlw_module]
ns_find_xs [Mlw_module]
null_invariant [Mlw_decl]

O
of_list [Extset.S]
construct a set from a list of elements
of_list [Extmap.S]
construct a map from a pair of bindings
on_meta [Task]
on_meta_excl [Task]
on_tagged_ls [Task]
on_tagged_pr [Task]
on_tagged_ts [Task]
on_tagged_ty [Task]
on_theory [Task]
on_used_theory [Task]
open_ls_defn [Decl]
open_ls_defn_cb [Decl]
open_namespace [Mlw_module]
open_namespace [Theory]
open_post [Mlw_ty]
option_list [Debug.Args]
Print the list of flags if requested (in this case return true).
oty_compare [Ty]
oty_cons [Ty]
oty_equal [Ty]
oty_freevars [Ty]
oty_hash [Ty]
oty_inst [Ty]
oty_match [Ty]
oty_type [Ty]

P
pad_right [Strings]
chop or pad the given string on the right up to the given length
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_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.
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_all [Term]
pat_any [Term]
pat_app [Term]
pat_as [Term]
pat_fold [Term]
pat_map [Term]
pat_or [Term]
pat_var [Term]
pat_wild [Term]
pl_clone [Mlw_expr]
pl_equal [Mlw_expr]
play_all [Session_scheduler.Make]
play_all es sched l runs every prover of list l on all goals and sub-goals of the session, with the given time limit.
plugins [Whyconf]
pluginsdir [Whyconf]
post_wait_call [Call_provers]
Thread-safe non-blocking function that should be called when the prover's exit status was obtained from a prior call of Unix.waitpid
pr_equal [Decl]
pr_hash [Decl]
prefix [Lists]
the first n elements of a list
preid_name [Ident]
prepare_task [Driver]
Split the previous function in two simpler functions
print [Debug.Stats]
print_any [Session]
Print a subtree with a pstree format (cf Tree module)
print_attempt_status [Session]
print_external_proof [Session]
print_filter_prover [Whyconf]
print_meta_desc [Theory]
print_prover [Whyconf]
print_prover_answer [Call_provers]
print_prover_parseable_format [Whyconf]
print_prover_result [Call_provers]
Pretty-print a prover_result.
print_session [Session]
Print a session with a pstree format (cf Tree module)
print_task [Driver]
print_task_prepared [Driver]
print_theory [Driver]
produce a realization of the given theory using the given driver
proof_verified [Session]
Return Some t if the proof is not obsolete and the result is valid.
prove_task [Driver]
prove_task_prepared [Driver]
prover_call_pid [Call_provers]
Return the pid of the prover
prover_on_goal [Session_scheduler.Make]
prover_on_goal es sched ?cntexample ?timelimit p g same as redo_external_proof but creates or reuses existing proof_attempt
prover_parseable_format [Whyconf]
ps_app [Term]
ps_equ [Term]
equality predicate
ps_equal [Mlw_expr]
pv_equal [Mlw_ty]
pv_old [Mlw_decl]

Q
query_call [Call_provers]
Thread-safe non-blocking function that checks if the prover has finished.

R
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_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 [Mlw_module]
read_module_or_theory [Mlw_module]
read_session [Session]
Read a session stored on the disk.
read_theory [Env]
read_theory env path th returns the theory path.th from the library.
recover_theory_tasks [Session]
Recover all the sub-goal (not only strict) of this theory
reg_all [Mlw_ty]
reg_any [Mlw_ty]
reg_equal [Mlw_ty]
reg_equal_check [Mlw_ty]
reg_fold [Mlw_ty]
reg_full_inst [Mlw_ty]
reg_hash [Mlw_ty]
reg_iter [Mlw_ty]
reg_match [Mlw_ty]
reg_occurs [Mlw_ty]
register [Debug.Stats]
register_flag [Debug]
register a new flag.
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]
register a new info flag.
register_int [Debug.Stats]
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.
release_sub_tasks [Session]
apply the previous function on this goal and its its sub-goal
release_task [Session]
remove the task stored in this goal
remove [Session_scheduler.OBSERVER]
removes a key
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_external_proof [Session]
remove_file [Session]
Remove a file
remove_metas [Session_scheduler.Make]
remove_metas [Session]
Remove the addition of metas
remove_model_labels [Ident]
Returns a copy of labels without labels "model" and "model_projected".
remove_old [Mlw_wp]
remove_prefix [Strings]
remove_prefix pref s removes the prefix pref from s.
remove_proof_attempt [Session_scheduler.Make]
remove_transformation [Session_scheduler.Make]
remove_transformation [Session]
Remove a transformation
replace [Extmap.S]
replace e x v m binds x to v in m if x is already bound, and raises e otherwise.
replay [Session_scheduler.Make]
replay es sched ~obsolete_only ~context_unproved_goals_only a reruns proofs under a if obsolete_only is set then does not rerun non-obsolete proofs if context_unproved_goals_only is set then only rerun proofs whose previous answer was 'valid'
reset [Session_scheduler.OBSERVER]
deletes all keys
restore_its [Mlw_ty]
raises Not_found if the argument is not a its_ts
restore_module [Mlw_module]
retrieves a module from its underlying theory raises Not_found if no such module exists
restore_path [Mlw_module]
restore_path id returns the triple (library path, module, qualified symbol name) if the ident was ever introduced in a module declaration.
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_pl [Mlw_expr]
raises Not_found if the argument is not a pl_ls
restore_pv [Mlw_ty]
raises Not_found if the argument is not a pv_vs
rev_map_fold_left [Lists]
rev_split [Strings]
run_external_proof [Session_scheduler.Make]
run_external_proof es sched ?cntexample ?callback p reruns an existing proof attempt p
run_external_proof_v3 [Session_scheduler.Make]
run_external_proof_v3 env_session sched pa ?cntexample callback the callback is applied with callback pa p limits old_result status.
run_prover [Session_scheduler.Make]
run_prover es sched p a runs prover p on all goals under a the proof attempts are only scheduled for running, and they will be started asynchronously when processors are available.
run_strategy [Session_scheduler.Make]
run_strategy_on_goal [Session_scheduler.Make]
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]
Save a session on disk
schedule_any_timeout [Session_scheduler.Make]
run it when an action slot/worker/cpu is available.
schedule_proof_attempt [Session_scheduler.Make]
session_iter [Session]
session_iter_proof_attempt [Session]
set [Weakhtbl.S]
set [Strings]
set_archive [Session_scheduler.Make]
set_archived [Session]
set_bool [Rc]
Same as Rc.set_int but on bool
set_booll [Rc]
Same as Rc.set_intl but on bool
set_cntexample [Whyconf]
set_compare [Extmap.S]
set_compare = compare (fun _ _ -> 0)
set_debug_formatter [Debug]
Set the formatter used when printing debug material
set_diff [Extmap.S]
set_diff = diff (fun _ _ _ -> None)
set_disjoint [Extmap.S]
set_disjoint = disjoint (fun _ _ _ -> false)
set_edited_as [Session]
set_editors [Whyconf]
replace the set of editors
set_equal [Extmap.S]
set_equal = equal (fun _ _ -> true)
set_family [Whyconf]
set_family config name Same as Rc.set_family except name must not be prover
set_family [Rc]
set_family rc name family add all the section in family using the associated string as argument of the family name in rc.
set_file_expanded [Session]
open one level or close all the sub-level
set_flag [Debug]
Modify the state of a flag
set_flags_selected [Debug.Args]
Set the flags selected by debug_all, debug or a shortcut.
set_goal_expanded [Session]
set_int [Rc]
set_int ?default section key value add the association key to value in the section if value is not default.
set_inter [Extmap.S]
set_inter = inter (fun _ x _ -> Some x)
set_intl [Rc]
set_int ?default section key lvalue add the associations key to all the lvalue in the section if value is not default.
set_limits [Whyconf]
set_main [Whyconf]
set_main config main replace the main section by the given one
set_maximum_running_proofs [Session_scheduler.Make]
set_memlimit [Session]
set_metas_expanded [Session]
set_obsolete [Session]
set_plugins [Whyconf]
set_policies [Whyconf]
set_proof_state [Session]
set_prover_shortcuts [Whyconf]
set the prover shortcuts
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]
set_section config name Same as Rc.set_section except name must not be "main"
set_section [Rc]
set_section rc name section add a section section with name name in rc.
set_simple_family [Rc]
set_simple_family rc name family add all the section in family using the associated string as argument of the family name in rc.
set_string [Rc]
Same as Rc.set_int but on string
set_stringl [Rc]
Same as Rc.set_intl but on string
set_submap [Extmap.S]
set_submap = submap (fun _ _ _ -> true)
set_theory_expanded [Session]
set_timelimit [Session]
set_transf_expanded [Session]
set_union [Extmap.S]
set_union = union (fun _ x _ -> Some x)
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.
spec_check [Mlw_ty]
verify that the spec corresponds to the result type
spec_pvset [Mlw_ty]
raises Not_found if the spec contains non-pv variables
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 [Strings]
split c s splits s into substrings, taking as delimiter the character c, and returns the list of substrings.
split_theory [Task]
split_theory th s t returns the tasks of th added to t that end by one of s.
stack_trace [Debug]
stack_trace flag
start [Session_scheduler.Todo]
one task is started
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]
stepregexp [Call_provers]
stepregexp s n creates a regular expression to match the number of steps.
stop [Session_scheduler.Todo]
one task is stopped without information
string_unique [Ident]
Uniquify string
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.
subset [Extset.S]
subset s1 s2 tests whether the set s1 is a subset of s2.
syntax_map [Driver]

T
t_all [Term.TermTF]
t_all [Term]
t_and [Term]
t_and_asym [Term]
t_and_asym_simp [Term]
t_and_asym_simp_l [Term]
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_at_old [Mlw_wp]
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_simp [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_const [Term]
t_eps [Term]
t_eps_close [Term]
t_equ [Term]
t_equ_simp [Term]
t_equal [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_freevars [Term]
t_func_app [Term]
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]
t_gen_map [Term]
t_hash [Term]
t_if [Term]
t_if_simp [Term]
t_iff [Term]
t_iff_simp [Term]
t_implies [Term]
t_implies_simp [Term]
t_is_lambda [Term]
t_is_lambda t returns true if t is a lambda-term.
t_label [Term]
t_label_add [Term]
t_label_copy [Term]
t_label_remove [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_simp [Term]
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_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_simp [Term]
t_or_asym_simp_l [Term]
t_or_simp [Term]
t_or_simp_l [Term]
t_pred_app [Term]
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]
t_prop [Term]
t_prop t checks that t is prop-typed and returns t
t_pvset [Mlw_ty]
raises Not_found if the term contains non-pv variables
t_quant [Term]
t_quant_close [Term]
t_quant_close_simp [Term]
t_quant_simp [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_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 by mapping mt simultaneously in substitution mv and in term t.
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_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 [Mlw_expr]
tag [Stdlib.TaggedType]
tag [Weakhtbl.Weakey]
tag_equal [Weakhtbl]
tag_hash [Weakhtbl]
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]
td_equal [Theory]
td_hash [Theory]
tds_compare [Task]
tds_empty [Task]
tds_equal [Task]
tds_hash [Task]
test_flag [Debug]
Return the state of the flag
test_noflag [Debug]
th_mark_at [Mlw_wp]
th_mark_old [Mlw_wp]
theory_iter [Session]
theory_iter_proof_attempt [Session]
timelimit [Whyconf]
timeout [Session_scheduler.OBSERVER]
a handler for functions that must be called after a given time elapsed, in milliseconds.
timeout [Session_scheduler.Base_scheduler]
timeregexp [Call_provers]
Converts a regular expression with special markers '%h','%m', '%s','%i' (for milliseconds) into a value of type timeregexp
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
toggle_flag [Debug]
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]
transf_iter [Session]
transf_iter_proof_attempt [Session]
transform [Session_scheduler.Make]
transform es sched tr a applies registered transformation tr on all leaf goals under a.
transform_goal [Session_scheduler.Make]
transform es sched tr g applies registered transformation tr on the given goal.
transform_proof_attempt [Session_tools]
replace all the proof attempts of the given session by the application of the given registered transformation followed by a proof_attempt with the same prover and time limit (but undone)
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.
ts_bool [Ty]
ts_compare [Ty]
ts_equal [Ty]
ts_func [Ty]
ts_hash [Ty]
ts_int [Ty]
ts_mark [Mlw_decl]
ts_pred [Ty]
ts_real [Ty]
ts_tuple [Ty]
ts_unit [Mlw_ty]
the same as Ty.ts_tuple 0
ttrue [Util]
ttrue constant function true
tuple_theory [Theory]
tuple_theory_name [Theory]
tv_compare [Ty]
tv_equal [Ty]
tv_hash [Ty]
tv_of_string [Ty]
ty_all [Ty]
ty_any [Ty]
ty_app [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_mark [Mlw_decl]
ty_match [Ty]
ty_match sigma0 pat sub returns a type substitution sigma such that sigma pat = sub.
ty_of_ity [Mlw_ty]
all aliases expanded, all regions removed
ty_of_vty [Mlw_ty]
convert arrows to the unit type
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_tuple [Ty]
ty_unit [Mlw_ty]
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]

U
uncapitalize [Strings]
uninstalled_prover [Session_scheduler.OBSERVER]
When a prover must be called on a task but it is currently not installed, what policy to apply
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.
unit_theory [Theory]
unknown_to_known_provers [Session_tools]
return others, same name, same version
unload_provers [Session]
forces unloading of all provers, to force reading again the configuration
unset_flag [Debug]
update_edit_external_proof [Session]
return the absolute path of the edited file update with the current goal
update_env_session_config [Session]
updates the configuration
update_session [Session_scheduler.Make]
Same as Session.update_session except initialization is done.
update_session [Session]
reload the given session with the given environnement : the files are reloaded, apply again the transformation, if some goals appear try to find to which goal in the given session it corresponds. The last case meant that the session was obsolete.
use_export [Mlw_module]
use_export [Task]
use_export [Theory]
use_export_theory [Mlw_module]
used_symbols [Task]
takes the result of 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

V
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.
vars_empty [Mlw_ty]
vars_freeze [Mlw_ty]
vars_union [Mlw_ty]
verbose [Session_scheduler.Base_scheduler]
vs_compare [Term]
vs_equal [Term]
vs_hash [Term]
vty_arrow [Mlw_ty]
vty_vars [Mlw_ty]
collect the type variables and regions in arguments and values, but ignores the spec

W
wait_on_call [Call_provers]
Thread-safe blocking function that waits until the prover finishes.
warn_clone_not_abstract [Theory]
why3_regexp_of_string [Whyconf]
wp_let [Mlw_wp]
wp_rec [Mlw_wp]
wp_val [Mlw_wp]

X
xs_equal [Mlw_ty]
xs_exit [Mlw_module]