package bindlib

Type representing a set of variable names.

empty_ctxt represents an empty context.

reset_context_for_closed_terms indicates whether the context should be reset to the empty context when calling unbind_in or munbind_in on a closed binder (which cannot capture names). If set to true, printing a λ-term will produce “λx.λx.x” rather than “λx.λx0.x0”, or “λx.x (λx.x)” rather than “λx.x (λx0.x0)”.

skip_constant_binders indicates whether binders that are constant must be skipped (i.e., not recorded in the context). This permits reusing the name in a lower binder like in “λx.λx.x”, but not in “λx.x (λx.x)”.

constant_binder_name optionally provides a representation for a binder that is constant, to highlight the absence of a name. When this value is defined to be Some(s), then s is used as name for all such binders. For example, if s is "_" then we would get “λ_.λx.x”. Note that if the value of constant_binder_name is not None, skip_constant_binder is ignored.

new_name name ctxt creates a name that is fresh in context ctxt. The given name indicates a prefered name (or base for the name). Note that the returned context extends ctxt with the new name.

reserve_name name ctxt extends context ctxt by reserving name as a free variable name.