[ docs ] CI docs generation

https://github.com/stefan-hoeck/idris2-pack-db/actions/runs/11619950651

docs/deptycheck/docs/docs/Deriving.DepTyCheck.Gen.Core.Util.html

@@ -61,4 +61,4 @@
 </script>
 
 </header>
-<div class="container"><div id="module-header"><h1>Deriving.DepTyCheck.Gen.Core.Util</h1><span style="float:right">(<a href="Deriving.DepTyCheck.Gen.Core.Util.src.html">source</a>)</span><pre></pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Data.Fin.Split<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Decidable.Equality<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Derive</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><code><span class="keyword">data</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;:&ensp;<span class="name type">Type</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><br>  <b>Constructors</b>:<br><dl class="decls">  <dt id="Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><span class="name constructor">DeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><span class="name constructor">NotDeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl><br>  <b>Hints</b>:<br><dl class="decls">  <dt id="$resolved15410"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="$resolved15409"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span></code></dt>  <dt id="$resolved15408"><code><span class="type resolved" title="Prelude.Interfaces.Monoid"><span class="name type">Monoid</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="$resolved15407"><code><span class="type resolved" title="Prelude.Interfaces.Semigroup"><span class="name type">Semigroup</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><span class="name function">BindExprFun</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Types.Nat"><span class="name type">Nat</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</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="Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</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="Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><span class="name function">analyseDeepConsApp</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.NamesInfoInTypes"><span class="name type">NamesInfoInTypes</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;(<span class="boundvar">collectConsDetermInfo</span>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.SortedSet.SortedSet"><span class="name type">SortedSet</span></span>&ensp;<span class="type resolved" title="Language.Reflection.TT.Name"><span class="name type">Name</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Language.Reflection.TTImp.TTImp"><span class="name type">TTImp</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Prelude.Types.Either"><span class="name type">Either</span></span>&ensp;<span class="name type">String</span>&ensp;(<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;<span class="boundvar">collectConsDetermInfo</span>)</code></dt><dd><pre>  Analyses whether the given expression can be an expression of free variables applies (maybe deeply) to a number of data constructors.<br>  <br>  Returns which of given free names are actually used in the given expression, in order of appearance in the expression.<br>  Notice that applied free names may repeat as soon as one name is used several times in the given expression.<br>  <br>  Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))<br>  is also returned.<br>  This function requires bind variable names as input.<br>  It returns correct bind expression only when all given bind names are different.</pre><br>  <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-0659bcc2c</footer></body></html>
+<div class="container"><div id="module-header"><h1>Deriving.DepTyCheck.Gen.Core.Util</h1><span style="float:right">(<a href="Deriving.DepTyCheck.Gen.Core.Util.src.html">source</a>)</span><pre></pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Data.Fin.Split<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Decidable.Equality<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Derive</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><code><span class="keyword">data</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;:&ensp;<span class="name type">Type</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><br>  <b>Constructors</b>:<br><dl class="decls">  <dt id="Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><span class="name constructor">DeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><span class="name constructor">NotDeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl><br>  <b>Hints</b>:<br><dl class="decls">  <dt id="$resolved15470"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="$resolved15469"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span></code></dt>  <dt id="$resolved15468"><code><span class="type resolved" title="Prelude.Interfaces.Monoid"><span class="name type">Monoid</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt>  <dt id="$resolved15467"><code><span class="type resolved" title="Prelude.Interfaces.Semigroup"><span class="name type">Semigroup</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><span class="name function">BindExprFun</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Types.Nat"><span class="name type">Nat</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</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="Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</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="Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><span class="name function">analyseDeepConsApp</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.NamesInfoInTypes"><span class="name type">NamesInfoInTypes</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;(<span class="boundvar">collectConsDetermInfo</span>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.SortedSet.SortedSet"><span class="name type">SortedSet</span></span>&ensp;<span class="type resolved" title="Language.Reflection.TT.Name"><span class="name type">Name</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Language.Reflection.TTImp.TTImp"><span class="name type">TTImp</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Prelude.Types.Either"><span class="name type">Either</span></span>&ensp;<span class="name type">String</span>&ensp;(<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;<span class="boundvar">collectConsDetermInfo</span>)</code></dt><dd><pre>  Analyses whether the given expression can be an expression of free variables applies (maybe deeply) to a number of data constructors.<br>  <br>  Returns which of given free names are actually used in the given expression, in order of appearance in the expression.<br>  Notice that applied free names may repeat as soon as one name is used several times in the given expression.<br>  <br>  Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))<br>  is also returned.<br>  This function requires bind variable names as input.<br>  It returns correct bind expression only when all given bind names are different.</pre><br>  <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-0659bcc2c</footer></body></html>