Deploying to gh-pages from @ b944062 🚀

base/docs/Control.Function.FunExt.html

@@ -61,4 +61,4 @@
 </script>
 
 </header>
-<div class="container"><div id="module-header"><h1>Control.Function.FunExt<span style="float:right">(<a href="../source/Control.Function.FunExt.html">source</a>)</span></h1><pre></pre></div><code></code><h2>Definitions</h2><dl class="decls"><dt id="Control.Function.FunExt.FunExt"><code><span class="keyword">interface</span>&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;:&ensp;<span class="name type">Type</span></code></dt><dd><pre>  This interface contains a proposition for the function extensionality.<br>  It is not meant to be ever implemented.<br>  It can be used to mark properties as requiring function extensionality to hold,<br>  i.e. its main objective is to provide a universal way to formulate a conditional property<br>  that holds only in the presence of function extensionality.</pre><br>  <b>Methods</b>:<br><dl class="decls">  <dt id="Control.Function.FunExt.funExt"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt"><span class="name function">funExt</span></a>&ensp;:&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt></dl></dd><dt id="Control.Function.FunExt.funExt"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt"><span class="name function">funExt</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Control.Function.FunExt.funExt0"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt0"><span class="name function">funExt0</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd><dt id="Control.Function.FunExt.funExt1"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt1"><span class="name function">funExt1</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-f016dad5c</footer></body></html>
+<div class="container"><div id="module-header"><h1>Control.Function.FunExt<span style="float:right">(<a href="../source/Control.Function.FunExt.html">source</a>)</span></h1><pre></pre></div><code></code><h2>Definitions</h2><dl class="decls"><dt id="Control.Function.FunExt.FunExt"><code><span class="keyword">interface</span>&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;:&ensp;<span class="name type">Type</span></code></dt><dd><pre>  This interface contains a proposition for the function extensionality.<br>  It is not meant to be ever implemented.<br>  It can be used to mark properties as requiring function extensionality to hold,<br>  i.e. its main objective is to provide a universal way to formulate a conditional property<br>  that holds only in the presence of function extensionality.</pre><br>  <b>Methods</b>:<br><dl class="decls">  <dt id="Control.Function.FunExt.funExt"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt"><span class="name function">funExt</span></a>&ensp;:&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt></dl></dd><dt id="Control.Function.FunExt.funExt"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt"><span class="name function">funExt</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Control.Function.FunExt.funExt0"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt0"><span class="name function">funExt0</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd><dt id="Control.Function.FunExt.funExt1"><code><a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.funExt1"><span class="name function">funExt1</span></a>&ensp;:&ensp;<a class="type" href="Control.Function.FunExt.html#Control.Function.FunExt.FunExt"><span class="name type">FunExt</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;{<span class="keyword">0</span>&ensp;<span class="boundvar">b</span>&ensp;:&ensp;<span class="boundvar">a</span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span>}&ensp;<span class="keyword">-&gt;</span>&ensp;((<span class="boundvar">x</span>&ensp;:&ensp;<span class="boundvar">a</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="boundvar">x</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span>&ensp;<span class="boundvar">x</span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="boundvar">f</span>&ensp;<span class="keyword">=</span>&ensp;<span class="boundvar">g</span></code></dt><dd>  <b>Totality</b>:&ensp;<span class="keyword">total</span><br>  <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-b94406213</footer></body></html>