Index of values

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

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

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 b f postcomposes the binder b with the function f.

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

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 injects the value e into the 'a box 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 box.

box_binder f b boxes the binder b using the boxing function f.

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

box_mbinder f b boxes the multiple binder b using the boxings function f.

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

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

box_rev_list bs is similar to box_list bs, but the produced boxed list is reversed (it is hence more efficient).

box_trible is similar to box_pair, but for triples.

box_var x builds a 'a box from the 'a var x.

compare_vars x y safely compares x and y.

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

dummy_box can be used for initialising structures like 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 of the two multiple binders f and g.

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

hash_var x computes a hash for variable x.

is_closed b checks whether the box b is closed.

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

mbinder_arity b gives the arity of the mbinder.

mbinder_closed b indicates whether b is closed.

mbinder_compose b f postcomposes the multiple binder b with f.

mbinder_constant b indicates whether the mbinder b is constant.

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 the variables bound by b with the values vs.

name_of x returns a printable name for variable x.

names_of xs returns printable names for the variables of xs.

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

raw_binder name bind rank mkfree value builds a binder using the value function as its definition.

raw_mbinder names binds rank value is similar to raw_binder, but it is applied to a multiple binder.

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

subst b v substitutes the variable bound by b with the value v.

uid_of x returns a unique identifier of the given variable.

uids_of xs returns the unique identifiers of the variables of xs.

unbind b substitutes the binder b using a fresh variable.

unbind2 f g is similar to unbind f, but it substitutes two binders f and g at once using the same fresh variable.

unbind_in ctxt b is similar to unbind b, but it handles the context as explained in the documentation of 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 b substitutes the multiple binder b with fresh variables.

unmbind2 f g is similar to unmbind f, but it substitutes two multiple binder f and g at once, using the same fresh variables.

unmbind_in ctxt b is like unmbind b, but it handles the context as is explained in the documentation of new_mvar_in.