Index of values

A
apply_box [Bindlib]

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

B
bind [Bindlib]

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

bind_apply [Bindlib]

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

bind_in [Bindlib]

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

bind_mvar [Bindlib]

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

bind_var [Bindlib]

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

binder_closed [Bindlib]

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

binder_compose_left [Bindlib]

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

binder_compose_right [Bindlib]

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

binder_constant [Bindlib]

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

binder_from_fun [Bindlib]

binder_from_fun name f transform a function into a binder.

binder_name [Bindlib]

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

binder_occur [Bindlib]

binder_occur b tests whether the bound variable occurs in b.

binder_rank [Bindlib]

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

box [Bindlib]

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

box_apply [Bindlib]

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

box_apply2 [Bindlib]

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

box_apply3 [Bindlib]

box_apply3 is similar to box_apply2.

box_apply4 [Bindlib]

box_apply4 is similar to box_apply2 and box_apply3.

box_array [Bindlib]

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

box_list [Bindlib]

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

box_of_var [Bindlib]

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

box_opt [Bindlib]

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

box_pair [Bindlib]

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

box_rev_list [Bindlib]

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

box_triple [Bindlib]

box_trible is similar to box_pair, but for triples.

C
compare_vars [Bindlib]

compare_vars x y safely compares x and y.

copy_var [Bindlib]

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

D
dummy_bindbox [Bindlib]

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

E
empty_ctxt [Bindlib]

empty_ctxt denotes the empty context.

eq_binder [Bindlib]

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

eq_mbinder [Bindlib]

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

eq_vars [Bindlib]

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

F
fixpoint [Bindlib]

fixpoint bb constructs a binder fixpoint.

H
hash_var [Bindlib]

hash_var x computes a hash for variable x.

I
is_closed [Bindlib]

is_closed b checks whether the bindbox b is closed.

is_substituted [Bindlib]

is_subst b checks whether the bindbox b was substituted.

L
lift_box [Bindlib.Lift2]
lift_box [Bindlib.Lift]
M
map [Bindlib.Map2]
map [Bindlib.Map]
mbind [Bindlib]

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

mbind_apply [Bindlib]

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

mbind_in [Bindlib]

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

mbinder_arity [Bindlib]

mbinder_arity b gives the arity of the mbinder.

mbinder_closed [Bindlib]

mbinder_closed b indicates whether b is closed.

mbinder_constant [Bindlib]

mbinder_constant b indicates whether the mbinder b is constant.

mbinder_from_fun [Bindlib]

mbinder_from_fun is similar to binder_from_fun.

mbinder_names [Bindlib]

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

mbinder_occurs [Bindlib]

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

mbinder_rank [Bindlib]
msubst [Bindlib]

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

mvbind [Bindlib]

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

N
name_of [Bindlib]

name_of x returns a printable name for variable x.

new_mvar [Bindlib]

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

new_mvar_in [Bindlib]

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

new_var [Bindlib]

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

new_var_in [Bindlib]

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.

O
occur [Bindlib]

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

P
prefix_of [Bindlib]

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

R
reset_counter [Bindlib]

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

S
subst [Bindlib]

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

suffix_of [Bindlib]

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

U
uid_of [Bindlib]

uid_of x returns a unique identifier of the given variable.

unbind [Bindlib]

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

unbind2 [Bindlib]

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

unbind_in [Bindlib]

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

unbox [Bindlib]

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

unmbind [Bindlib]

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

unmbind2 [Bindlib]

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

unmbind_in [Bindlib]

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

V
vbind [Bindlib]

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