<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Renaming (bindlib.Bindlib.Renaming)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">bindlib</a> &#x00BB; <a href="../index.html">Bindlib</a> &#x00BB; Renaming</nav><header class="odoc-preamble"><h1>Module type <code><span>Bindlib.Renaming</span></code></h1><p>Module type giving the specification of a renaming policy, to be used with the <code>Ctxt</code> functor.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type" id="type-ctxt" class="anchored"><a href="#type-ctxt" class="anchor"></a><code><span><span class="keyword">type</span> ctxt</span></code></div><div class="spec-doc"><p>Type representing a set of variable names.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-empty_ctxt" class="anchored"><a href="#val-empty_ctxt" class="anchor"></a><code><span><span class="keyword">val</span> empty_ctxt : <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>empty_ctxt</code> represents an empty context.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-reset_context_for_closed_terms" class="anchored"><a href="#val-reset_context_for_closed_terms" class="anchor"></a><code><span><span class="keyword">val</span> reset_context_for_closed_terms : bool</span></code></div><div class="spec-doc"><p><code>reset_context_for_closed_terms</code> indicates whether the context should be reset to the empty context when calling <code>unbind_in</code> or <code>munbind_in</code> on a closed binder (which cannot capture names). If set to <code>true</code>, printing a λ-term will produce “λx.λx.x” rather than “λx.λx0.x0”, or “λx.x (λx.x)” rather than “λx.x (λx0.x0)”.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-skip_constant_binders" class="anchored"><a href="#val-skip_constant_binders" class="anchor"></a><code><span><span class="keyword">val</span> skip_constant_binders : bool</span></code></div><div class="spec-doc"><p><code>skip_constant_binders</code> 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)”.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-constant_binder_name" class="anchored"><a href="#val-constant_binder_name" class="anchor"></a><code><span><span class="keyword">val</span> constant_binder_name : <span>string option</span></span></code></div><div class="spec-doc"><p><code>constant_binder_name</code> optionally provides a representation for a binder that is constant, to highlight the absence of a name. When this value is defined to be <code>Some(s)</code>, then <code>s</code> is used as name for all such binders. For example, if <code>s</code> is &quot;_&quot; then we would get “λ_.λx.x”. Note that if the value of <code>constant_binder_name</code> is not <code>None</code>, <code>skip_constant_binder</code> is ignored.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-new_name" class="anchored"><a href="#val-new_name" class="anchor"></a><code><span><span class="keyword">val</span> new_name : <span>string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> string * <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>new_name name ctxt</code> creates a name that is fresh in context <code>ctxt</code>. The given <code>name</code> indicates a prefered name (or base for the name). Note that the returned context extends <code>ctxt</code> with the new name.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-reserve_name" class="anchored"><a href="#val-reserve_name" class="anchor"></a><code><span><span class="keyword">val</span> reserve_name : <span>string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-ctxt">ctxt</a></span></code></div><div class="spec-doc"><p><code>reserve_name name ctxt</code> extends context <code>ctxt</code> by reserving <code>name</code> as a free variable name.</p></div></div></div></body></html>