<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Ctxt (bindlib.Bindlib.Ctxt)</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; Ctxt</nav><header class="odoc-preamble"><h1>Module <code><span>Bindlib.Ctxt</span></code></h1><p>A functor that can be used to obtain context-manipulating functions, given the specification of a renaming policy. The defined <code>ctxt</code> type as well as the obtained functions can then be used as a drop-in replacement for their default counterparts (found at the top level of the <code>Bindlib</code> module).</p></header><nav class="odoc-toc"><ul><li><a href="#parameters">Parameters</a></li><li><a href="#signature">Signature</a></li></ul></nav><div class="odoc-content"><h2 id="parameters"><a href="#parameters" class="anchor"></a>Parameters</h2><div class="odoc-spec"><div class="spec parameter" id="argument-1-R" class="anchored"><a href="#argument-1-R" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="argument-1-R/index.html">R</a></span><span> : <a href="../module-type-Renaming/index.html">Renaming</a></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><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><span> = <a href="argument-1-R/index.html#type-ctxt">R.ctxt</a></span></code></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><div class="odoc-spec"><div class="spec value" id="val-free_vars" class="anchored"><a href="#val-free_vars" class="anchor"></a><code><span><span class="keyword">val</span> free_vars : <span><span><span class="type-var">'a</span> <a href="../index.html#type-box">box</a></span> <span class="arrow">&#45;&gt;</span></span> <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-new_var_in" class="anchored"><a href="#val-new_var_in" class="anchor"></a><code><span><span class="keyword">val</span> new_var_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span><span class="type-var">'a</span> <a href="../index.html#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="../index.html#type-var">var</a></span> * <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-new_mvar_in" class="anchored"><a href="#val-new_mvar_in" class="anchor"></a><code><span><span class="keyword">val</span> new_mvar_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span>( <span><span><span class="type-var">'a</span> <a href="../index.html#type-var">var</a></span> <span class="arrow">&#45;&gt;</span></span> <span class="type-var">'a</span> )</span> <span class="arrow">&#45;&gt;</span></span> <span><span>string array</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="../index.html#type-mvar">mvar</a></span> * <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind_in" class="anchored"><a href="#val-unbind_in" class="anchor"></a><code><span><span class="keyword">val</span> unbind_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="../index.html#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="../index.html#type-var">var</a></span> * <span class="type-var">'b</span> * <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-unbind2_in" class="anchored"><a href="#val-unbind2_in" class="anchor"></a><code><span><span class="keyword">val</span> unbind2_in : 
  <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="../index.html#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="../index.html#type-binder">binder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'a</span> <a href="../index.html#type-var">var</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span> * <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind_in" class="anchored"><a href="#val-unmbind_in" class="anchor"></a><code><span><span class="keyword">val</span> unmbind_in : <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span> <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="../index.html#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span> <span><span class="type-var">'a</span> <a href="../index.html#type-mvar">mvar</a></span> * <span class="type-var">'b</span> * <a href="#type-ctxt">ctxt</a></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-unmbind2_in" class="anchored"><a href="#val-unmbind2_in" class="anchor"></a><code><span><span class="keyword">val</span> unmbind2_in : 
  <span><a href="#type-ctxt">ctxt</a> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'b</span> )</span> <a href="../index.html#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span><span>( <span class="type-var">'a</span>, <span class="type-var">'c</span> )</span> <a href="../index.html#type-mbinder">mbinder</a></span> <span class="arrow">&#45;&gt;</span></span>
  <span><span class="type-var">'a</span> <a href="../index.html#type-mvar">mvar</a></span> * <span class="type-var">'b</span> * <span class="type-var">'c</span> * <a href="#type-ctxt">ctxt</a></span></code></div></div></div></body></html>