Index of values

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 x s returns a set containing the same elements as s, plus x.

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

add_builtin lang builtin adds new builtin libraries to lang.

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

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

add_left s x is the same as add x s.

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

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

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

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

all2_fn pr z a b return true if pr a b is true, otherwise raise FoldSkip

all_fn pr z a return true if pr a is true, otherwise raise FoldSkip

any2_fn pr z a b return false if pr a b is false, otherwise raise FoldSkip

any_fn pr z a return false if pr a is false, otherwise raise FoldSkip

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@*".

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 f [a1;..;an] returns (f a1)@...@(f an)

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 a registered 1-to-1 or a 1-to-n, directly.

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

add string delimiter " "

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

base_language is the root of the tree of supported languages.

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

Return the list of all bindings of the given map.

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.

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

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

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

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

Return the number of elements in a set.

Return the number of bindings of a map.

same as Printer.catch_unsupportedType but use UnsupportedDecl instead of UnsupportedType

same as Printer.catch_unsupportedType but use UnsupportedExpr instead of UnsupportedType

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 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 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 s id opr npr changes the prover of the proof attempt using prover opr by the new prover npr.

check_exhaustive section keys check that only the keys in keys appear inside the section section

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

check_range c ir checks that c is in the range described by ir, and raises OutOfRange c if not.

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

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

removes the first n elements of a list; raises Invalid_argument if the list is not long enough

removes (and returns) the last element of a list

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

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

Total ordering between sets.

Total ordering between maps.

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

"computer" division, i.e division rounds towards zero, and thus mod x y has the same sign as x

contains s x is the same as mem x s.

contains m x is the same as mem x m.

create_alias_decl id args def creates a new alias type declaration.

create_alias_itysymbol id args def creates a new type alias.

creates a controller for the given session.

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

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.

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

create_float_decl id fp creates a new float type declaration.

create_float_itysymbol id f creates a new float type.

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

start a new printer with a sanitizing function and a blacklist

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 ~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 id args constructors creates a declaration for a non-recursive algebraic type.

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

create_range_decl id ir creates a new range type declaration.

create_range_itysymbol id r creates a new range type.

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

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

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

create_region id s tl rl creates a fresh region.

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

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

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

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 cty converts a cty of a partial application into a cty of a fully applied application, returning a mapping.

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

cty_ghost cty returns cty.cty_effect.eff_ghost

cty_ghostify ghost cty ghostifies the effect of cty.

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

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

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

cty_reads cty returns the set of external dependencies of cty.

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

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 f t1 t2 adds to task t1 the declarations f d for each declaration d of task t2.

decl_l f t1 t2: on each declaration d of task t2 (with f d = ld_1; ld_2; ... ld_n), create n duplicates (newt_i) of t1 with the declaration d_i replaced by ld_i.

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

Default delay for the scheduler timeout

editor name used when no specific editor known for a prover

Option for specifying a debug flag to set

Option for setting all info flags

Option for printing the list of debug flags

Option for setting a specific flag

diff f s1 s2 computes the difference of two sets

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

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

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

domain m returns the set of keys of bindings in m

Print only if the flag is set

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

e_fold does not descend into Cfun

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

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

Return the list of all elements of the given set.

An empty Rc

The empty set.

The empty map.

An empty section

create an empty_session in the directory specified by the argument

test if a string ends with another

comparisons

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

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

Division and modulo operators with the convention that modulo is always non-negative.

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

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

raises Invalid_argument is rs_field is None

ffalse constant function false

File

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 d f th produces a filename for the prover of driver d, for a theory th from filename f

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

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

find the uniq prover that verify the filter.

test if the prover match the filter prover

resolve prover shortcut in filter

Get all the provers that match this filter

returns the coercion, or raises Not_found

Same as Hashtbl.find

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

return the first binding or the given value if none found

return the first binding or the given value if none found

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

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

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

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

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

return the first binding or None if none found

return the first binding or None if none found

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

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

The combinaison of list_first and list_find_nth.

get the description of the flag

Iterating transformations

Same as Hashtbl.fold

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

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 f d o returns d if o is None, and f d x if o is Some x

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.

fold the common keys of two map at the same time

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.

fold the keys which appear in one of the two maps

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

fold_all_session s f acc folds on the whole session

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

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

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

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

generalisation of Lists.fold_product; not tail-recursive

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

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

forget all idents

forget an ident

from_channel cin returns the Rc of the input channel cin

from_file filename returns the Rc of the file filename

Same as Rc.get_int but on bool

Same as Rc.get_intl but on bool

add the extra_options to the command

get_conf_file config get the rc file corresponding to this configuration

Get the formatter used when printing debug material

returns the set of editors

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

get_family rc name return all the sections of the family name in rc

get_home_dir () returns the home dir of the user

get_int ~default section key one key to one value

get_intl ~default section key one key to many value

returns the loadpath of a given environment

get_main config get the main section stored in the Rc file

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

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

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

returns new results from why3server, in an unordered fashion.

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

return the prover shortcuts

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 config get the prover family stored in the Rc file.

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

get_section rc name

get_simple_family rc name return all the sections of the simple family name in rc

Same as Rc.get_int but on string

Same as Rc.get_intl but on string

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 s id name l tl adds the transformation name as a child of the task id of the session s.

true when ident has one of the attributes above

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

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

the same as Hashtbl.hash

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

create a duplicate pre-ident with given attributes

create a duplicate pre-ident

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

create a fresh pre-ident

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

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

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

create a localized pre-ident

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

add the indentation at the first line

these four functions construct integer constant terms from some string s of digits in the corresponding base.

inter f s1 s2 computes the intersection of two sets

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

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

non-blocking function that asks for prover interruption

test if the hashtbl is empty

test if the hashtbl is empty

Test whether a set is empty or not.

Test whether a map is empty or not.

test if the flag is an info flag

check if the map has the given number of elements

check if the map has the given number of elements

test if a prover is detected

Same as Hashtbl.iter

iter f s applies f to all elements of s.

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

iterf f min max step

a pure type symbol is immutable and has no mutable components

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

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 s tl rl creates an Ityapp type.

a closed type contains no type variables

a fragile type may contain a component with a broken invariant

fresh regions are created when needed.

pure snapshots are substituted when needed.

replaces regions with pure snapshots

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

Return the list of all keys of the given map.

Returns true if the printer already knows the id.

Same as Hashtbl.length

list the known flags

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

wrapper for loading a driver from a file that may be relative to the datadir.

loads a driver from a file

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

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 path returns the location of the library file specified by path.

get the flag

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

tries to reconstruct a definition from a defining axiom.

raises Invalid_argument is rs_logic is not an RLls

a shortcut less efficient than possible

a shortcut less efficient than possible

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.

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

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

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

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

fold and map at the same time

mark_obsolete s id marks id as obsolete in s

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

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

Same as Hashtbl.mem

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

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

convenience function, memoize a function

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

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

merge_config config filename merge the content of filename into config

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

min, max, abs

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

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

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

give transformation a name without registering

get the next step of the enumeration

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

number of digits

construct a set from a list of elements

construct a map from a list of bindings.

conversions

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_tagged_* m f allow to do a transformation having all the tagged declarations in a set as argument of f.

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

chop or pad the given string on the right up to the given length

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 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 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 cmp l returns the list of the congruence classes with respect to cmp.

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

power of small integers.

the first n elements of a list

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

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

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

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

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

print_pair_delim left_delim middle_delim right_delim

Pretty-print a Call_provers.prover_answer

Pretty-print a prover_result.

produce a realization of the given theory using the given driver

equality predicate

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

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

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

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

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.

an open-close wrapper around read_channel

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

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

real_const_dec integer_part decimal_part exp return the real that corresponds to "integer_part.decimal_part * 10^exp".

register a new flag.

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 a new info flag.

register_language parent convert adds a leaf to the language tree.

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

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

reload_files 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.

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

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

remove_left s x is the same as remove x s.

Remove the counter-example attributes from an attribute set

remove_prefix pref s removes the prefix pref from s.

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

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

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

remove_suffix suff s removes the suffix suff from s.

remove_transformation s id removes the transformation id from the session s

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

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.

raises Not_found if the argument is not a its_ts

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

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

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

raises Not_found if the argument is not a pv_vs

raises Not_found if the argument is not a rs_logic

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

generic sanitizer taking a separate encoder for the first letter

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

save_config config save the configuration

save_session s Save the session s

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 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 c id cb schedules a transformation for a goal specified by id; the function cb will be called each time the transformation status changes.

Same as Rc.set_int but on bool

Same as Rc.set_intl but on bool

set_compare = compare (fun _ _ -> 0)

Set the formatter used when printing debug material

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

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

replace the set of editors

set_equal = equal (fun _ _ -> true)

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

set_family rc name family add all the section in family using the associated string as argument of the family name in rc.

Modify the state of a flag

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

set_int ?default section key value add the association key to value in the section if value is not default.

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

set_int ?default section key lvalue add the associations key to all the lvalue in the section if value is not default.

set_main config main replace the main section by the given one

set the prover shortcuts

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

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

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

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

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

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

Same as Rc.set_int but on string

Same as Rc.set_intl but on string

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

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

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

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

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 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 c s splits s into substrings, taking as delimiter the character c, and returns the list of substrings.

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

stack_trace flag

start the enumeration of the given map

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

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

same as Pp.string_of but without newline

Uniquify string

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

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

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

basic operations

(syntax_arguments templ print_arg fmt l) prints in the formatter fmt the list l using the template templ and the printer print_arg

(syntax_arguments templ print_arg fmt l) prints in the formatter fmt the list l using the template templ and the printer print_arg

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

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_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_fold fnT fnF = t_fold (t_selecti fnT fnF)

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

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

t_is_lambda t returns true if t is a 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_map fnT fnF = t_map (t_select fnT fnF)

t_map_cont is t_map in continuation-passing style