Documentation of branch “master” at 530d7a4d

Author: coqbot

master/api/rocq-runtime/Declareops/index.html

@@ -276,7 +276,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab5"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>
+<a id="lab23"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>
 
 <div class="paragraph"> </div>
 
@@ -291,7 +291,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Doubling and variants</h2>
+<a id="lab24"></a><h2 class="section">Doubling and variants</h2>
 
 </div>
 <div class="code">
@@ -324,7 +324,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">Subtraction of positive into Z</h2>
+<a id="lab25"></a><h2 class="section">Subtraction of positive into Z</h2>
 
 </div>
 <div class="code">
@@ -347,7 +347,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Addition</h2>
+<a id="lab26"></a><h2 class="section">Addition</h2>
 
 </div>
 <div class="code">
@@ -370,7 +370,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Opposite</h2>
+<a id="lab27"></a><h2 class="section">Opposite</h2>
 
 </div>
 <div class="code">
@@ -390,7 +390,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Subtraction</h2>
+<a id="lab28"></a><h2 class="section">Subtraction</h2>
 
 </div>
 <div class="code">
@@ -405,7 +405,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Multiplication</h2>
+<a id="lab29"></a><h2 class="section">Multiplication</h2>
 
 </div>
 <div class="code">
@@ -428,7 +428,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></a><h2 class="section">Power function</h2>
+<a id="lab30"></a><h2 class="section">Power function</h2>
 
 </div>
 <div class="code">
@@ -451,7 +451,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Comparison</h2>
+<a id="lab31"></a><h2 class="section">Comparison</h2>
 
 </div>
 <div class="code">
@@ -520,7 +520,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Minimum and maximum</h2>
+<a id="lab32"></a><h2 class="section">Minimum and maximum</h2>
 
 </div>
 <div class="code">
@@ -543,7 +543,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Conversions</h2>
+<a id="lab33"></a><h2 class="section">Conversions</h2>
 
 <div class="paragraph"> </div>
 
@@ -607,11 +607,11 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Euclidean divisions for binary integers</h2>
+<a id="lab34"></a><h2 class="section">Euclidean divisions for binary integers</h2>
 
 <div class="paragraph"> </div>
 
-<a id="lab17"></a><h2 class="section">Floor division</h2>
+<a id="lab35"></a><h2 class="section">Floor division</h2>
 
 <div class="paragraph"> </div>
 
@@ -702,7 +702,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab18"></a><h2 class="section">Trunc Division</h2>
+<a id="lab36"></a><h2 class="section">Trunc Division</h2>
 
 <div class="paragraph"> </div>
 
@@ -763,7 +763,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 No infix notation for rem, otherwise it becomes a keyword 
 <div class="paragraph"> </div>
 
-<a id="lab19"></a><h2 class="section">Parity functions</h2>
+<a id="lab37"></a><h2 class="section">Parity functions</h2>
 
 </div>
 <div class="code">
@@ -781,7 +781,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab20"></a><h2 class="section">Division by two</h2>
+<a id="lab38"></a><h2 class="section">Division by two</h2>
 
 <div class="paragraph"> </div>
 
@@ -804,7 +804,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab21"></a><h2 class="section">Square root</h2>
+<a id="lab39"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">

master/corelib/Corelib.BinNums.IntDef.html

@@ -270,7 +270,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab1"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>
+<a id="lab40"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>
 
 </div>
 <div class="code">
@@ -282,7 +282,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>
+<a id="lab41"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>
 
 </div>
 <div class="code">
@@ -298,7 +298,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab3"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>
+<a id="lab42"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>
 
 </div>
 <div class="code">
@@ -314,7 +314,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">The successor of a <span class="inlinecode"><span class="id" title="var">N</span></span> can be seen as a <span class="inlinecode"><span class="id" title="var">positive</span></span></h2>
+<a id="lab43"></a><h2 class="section">The successor of a <span class="inlinecode"><span class="id" title="var">N</span></span> can be seen as a <span class="inlinecode"><span class="id" title="var">positive</span></span></h2>
 
 </div>
 <div class="code">

master/corelib/Corelib.BinNums.NatDef.html

@@ -267,7 +267,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab22"></a><h1 class="section">Binary positive numbers, operations</h1>
+<a id="lab3"></a><h1 class="section">Binary positive numbers, operations</h1>
 
 <div class="paragraph"> </div>
 
@@ -313,11 +313,11 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab23"></a><h1 class="section">Operations over positive numbers</h1>
+<a id="lab4"></a><h1 class="section">Operations over positive numbers</h1>
 
 <div class="paragraph"> </div>
 
-<a id="lab24"></a><h2 class="section">Successor</h2>
+<a id="lab5"></a><h2 class="section">Successor</h2>
 
 </div>
 <div class="code">
@@ -334,7 +334,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab25"></a><h2 class="section">Addition</h2>
+<a id="lab6"></a><h2 class="section">Addition</h2>
 
 </div>
 <div class="code">
@@ -370,7 +370,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab26"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>-1</span></h2>
+<a id="lab7"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>-1</span></h2>
 
 </div>
 <div class="code">
@@ -387,7 +387,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab27"></a><h2 class="section">The predecessor of a positive number can be seen as a <span class="inlinecode"><span class="id" title="var">N</span></span></h2>
+<a id="lab8"></a><h2 class="section">The predecessor of a positive number can be seen as a <span class="inlinecode"><span class="id" title="var">N</span></span></h2>
 
 </div>
 <div class="code">
@@ -404,7 +404,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab28"></a><h2 class="section">An auxiliary type for subtraction</h2>
+<a id="lab9"></a><h2 class="section">An auxiliary type for subtraction</h2>
 
 </div>
 <div class="code">
@@ -419,7 +419,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab29"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>
+<a id="lab10"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>+1</span></h2>
 
 </div>
 <div class="code">
@@ -436,7 +436,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab30"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>
+<a id="lab11"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span></span></h2>
 
 </div>
 <div class="code">
@@ -453,7 +453,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab31"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>-2</span></h2>
+<a id="lab12"></a><h2 class="section">Operation <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">-&gt;</span> <span class="inlinecode">2*<span class="id" title="var">x</span>-2</span></h2>
 
 </div>
 <div class="code">
@@ -470,7 +470,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab32"></a><h2 class="section">Subtraction, result as a mask</h2>
+<a id="lab13"></a><h2 class="section">Subtraction, result as a mask</h2>
 
 </div>
 <div class="code">
@@ -503,7 +503,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab33"></a><h2 class="section">Subtraction, result as a positive, returning 1 if <span class="inlinecode"><span class="id" title="var">x</span>&lt;=<span class="id" title="var">y</span></span></h2>
+<a id="lab14"></a><h2 class="section">Subtraction, result as a positive, returning 1 if <span class="inlinecode"><span class="id" title="var">x</span>&lt;=<span class="id" title="var">y</span></span></h2>
 
 </div>
 <div class="code">
@@ -519,7 +519,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab34"></a><h2 class="section">Multiplication</h2>
+<a id="lab15"></a><h2 class="section">Multiplication</h2>
 
 </div>
 <div class="code">
@@ -536,7 +536,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab35"></a><h2 class="section">Iteration over a positive number</h2>
+<a id="lab16"></a><h2 class="section">Iteration over a positive number</h2>
 
 </div>
 <div class="code">
@@ -553,7 +553,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab36"></a><h2 class="section">Division by 2 rounded below but for 1</h2>
+<a id="lab17"></a><h2 class="section">Division by 2 rounded below but for 1</h2>
 
 </div>
 <div class="code">
@@ -586,7 +586,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab37"></a><h2 class="section">Comparison on binary positive numbers</h2>
+<a id="lab18"></a><h2 class="section">Comparison on binary positive numbers</h2>
 
 </div>
 <div class="code">
@@ -612,7 +612,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab38"></a><h2 class="section">Boolean equality and comparisons</h2>
+<a id="lab19"></a><h2 class="section">Boolean equality and comparisons</h2>
 
 </div>
 <div class="code">
@@ -634,7 +634,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab39"></a><h2 class="section">A Square Root function for positive numbers</h2>
+<a id="lab20"></a><h2 class="section">A Square Root function for positive numbers</h2>
 
 <div class="paragraph"> </div>
 
@@ -782,7 +782,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab40"></a><h2 class="section">From binary positive numbers to Peano natural numbers</h2>
+<a id="lab21"></a><h2 class="section">From binary positive numbers to Peano natural numbers</h2>
 
 </div>
 <div class="code">
@@ -804,7 +804,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab41"></a><h2 class="section">From Peano natural numbers to binary positive numbers</h2>
+<a id="lab22"></a><h2 class="section">From Peano natural numbers to binary positive numbers</h2>
 
 </div>
 <div class="code">

master/corelib/Corelib.BinNums.PosDef.html

@@ -267,7 +267,7 @@ <h1 class="libtitle">Library Corelib.Classes.CMorphisms</h1>
 </div>
 
 <div class="doc">
-<a id="lab95"></a><h1 class="section">Typeclass-based morphism definition and standard, minimal instances</h1>
+<a id="lab114"></a><h1 class="section">Typeclass-based morphism definition and standard, minimal instances</h1>
 
 
 <div class="paragraph"> </div>
@@ -296,7 +296,7 @@ <h1 class="libtitle">Library Corelib.Classes.CMorphisms</h1>
 </div>
 
 <div class="doc">
-<a id="lab96"></a><h1 class="section">Morphisms.</h1>
+<a id="lab115"></a><h1 class="section">Morphisms.</h1>
 
 
 <div class="paragraph"> </div>