Index of values

apply_box bf ba applies the boxed function bf to a boxed argument ba inside the 'a bindbox type.

bind mkfree name f constructs a boxed binder from the function f.

bind_apply bb barg substitute the boxed binder bb with the boxed value barb in the bindbox type.

bind_in ctxt mkfree name f is like bind mkfree name f, but it handles the context.

bind_mvar xs b binds the variables of xs in b to get a boxed binder.

bind_var x b binds the variable x in b to produce a boxed binder.

binder_closed b test whether the binder b is closed (i.e., does not contain any free variable).

binder_compose_left f b precomposes the binder b with the function f without changing anything at the binding structure.

binder_compose_rigth b f postcomposes the binder b with the function f without changing anything at the binding structure.

binder_constant b tests whether the binder b is constant (i.e., its bound variable does not occur).

binder_from_fun name f transform a function into a binder.

binder_name returns the name of the variable bound by the binder.

binder_occur b tests whether the bound variable occurs in b.

binder_rank b gives the number of free variables contained in b.

box e puts the value e into the 'a bindbox type, assuming that it is closed.

box_apply f ba applies the function f to a boxed argument ba.

box_apply2 f ba bb applies the function f to two boxed arguments ba and bb.

box_apply3 is similar to box_apply2.

box_apply4 is similar to box_apply2 and box_apply3.

box_array bs shifts the array type of bs into the bindbox.

box_list bs shifts the list type of bs into the bindbox.

box_of_var x builds a 'a bindbox from the 'a var x.

box_opt bo shifts the option type of bo into the bindbox.

box_pair ba bb is the same as box_apply2 (fun a b -> (a,b)) ba bb.

box_rev_list bs shifts the list type of bs into the bindbox, while reversing the list (for efficiency).

box_trible is similar to box_pair, but for triples.

compare_vars x y safely compares x and y.

copy_var x name mkfree makes a copy of variable x, with a potentially different name and mkfree function.

dummy_bindbox can be used for initialising structires (e.g., arrays).

empty_ctxt denotes the empty context.

eq_binder eq f g tests the equality between f and g.

eq_mbinder eq f g tests the equality between two mbinder f and g.

eq_vars x y safely computes the equality of x and y.

fixpoint bb constructs a binder fixpoint.

hash_var x computes a hash for variable x.

is_closed b checks whether the bindbox b is closed.

is_subst b checks whether the bindbox b was substituted.

mbind mkfree names f constructs a boxed binder from function f, using mkfree and names to build the bound variables.

mbind_apply bb bargs substitute the boxed binder bb with the boxed array of values barbs in the bindbox type.

mbind_in ctxt mkfree names f is similar to mbind mkfree names f, but it handles the context.

mbinder_arity b gives the arity of the mbinder.

mbinder_closed b indicates whether b is closed.

mbinder_constant b indicates whether the mbinder b is constant.

mbinder_from_fun is similar to binder_from_fun.

mbinder_names b return the array of the names of the variables bound by the mbinder b.

mbinder_occurs b returns an array of bool indicating if the variables that are bound occur (i.e., are used).

msubst b vs substitutes (using application) the array of variables bound by b with the values vs.

mvbind mkfree names f constructs a boxed binder from the function f as the mbind function does.

name_of x returns a printable name for variable x.

new_mvar mkfree names creates a new array of variables using a function mkfree (see new_var) and a name.

new_mvar_in ctxt mkfree names is similar to new_mvar mkfree names, but it handles the context (see new_var_in).

new_var mkfree name creates a new variable using a function mkfree and a name.

new_var_in ctxt mkfree name is similar to new_var mkfree name, but the variable names is chosen not to collide with the context ctxt.

occur x b tells whether variable x occurs in the bindbox b.

prefix_of x returns the string prefix of variable x's name, which is only the first part of its full name (obtained with name_of x).

reset_counter () resets the unique identifier counter on which Bindlib relies.

subst b v substitutes (using application) the variable bound by b with the value b.

suffix_of x returns the int suffix of variable x's name.

uid_of x returns a unique identifier of the given variable.

unbind mkfree b breaks down the binder b into a variable, and the term in which this variable is now free.

unbind2 mkfree f g is similar to unbind mkfree f, but substitutes both f and g using the same fresh variable.

unbind_in ctxt mkfree b is similar to unbind mkfree b, but it handles the context (see new_mvar_in).

unbox e can be called when the construction of a term is finished (e.g., when the desired variables have all been bound).

unmbind mkfree b breaks down the binder b into variables, and the term in which these variables are now free.

unmbind2 mkfree f g is similar to unmbind mkfree f, but it substitutes both f and g using the same fresh variables.

munbind_in ctxt mkfree b is like munbind mkfree b, but it handles the context (see new_mvar_in).

vbind mkfree name f constructs a boxed binder from the function f, as the bind function does.