Documentation of branch “master” at 197637e7

coq · Jan 16, 2025 · b4d9fdc · b4d9fdc
1 parent 198fb9c
commit b4d9fdc
Show file tree

Hide file tree

Showing 72 changed files with 149 additions and 151 deletions.
diff --git a/master/api/rocq-runtime/Declarations/index.html b/master/api/rocq-runtime/Declarations/index.html
diff --git a/master/api/rocq-runtime/Mod_declarations/index.html b/master/api/rocq-runtime/Mod_declarations/index.html
diff --git a/master/corelib/html/Corelib.BinNums.IntDef.html b/master/corelib/html/Corelib.BinNums.IntDef.html
@@ -58,7 +58,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab21"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>
+<a id="lab5"></a><h1 class="section">Binary Integers, Definitions of Operations</h1>
 
 <div class="paragraph"> </div>
 
@@ -73,7 +73,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab22"></a><h2 class="section">Doubling and variants</h2>
+<a id="lab6"></a><h2 class="section">Doubling and variants</h2>
 
 </div>
 <div class="code">
@@ -106,7 +106,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab23"></a><h2 class="section">Subtraction of positive into Z</h2>
+<a id="lab7"></a><h2 class="section">Subtraction of positive into Z</h2>
 
 </div>
 <div class="code">
@@ -129,7 +129,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab24"></a><h2 class="section">Addition</h2>
+<a id="lab8"></a><h2 class="section">Addition</h2>
 
 </div>
 <div class="code">
@@ -152,7 +152,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab25"></a><h2 class="section">Opposite</h2>
+<a id="lab9"></a><h2 class="section">Opposite</h2>
 
 </div>
 <div class="code">
@@ -172,7 +172,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab26"></a><h2 class="section">Subtraction</h2>
+<a id="lab10"></a><h2 class="section">Subtraction</h2>
 
 </div>
 <div class="code">
@@ -187,7 +187,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab27"></a><h2 class="section">Multiplication</h2>
+<a id="lab11"></a><h2 class="section">Multiplication</h2>
 
 </div>
 <div class="code">
@@ -210,7 +210,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab28"></a><h2 class="section">Power function</h2>
+<a id="lab12"></a><h2 class="section">Power function</h2>
 
 </div>
 <div class="code">
@@ -233,7 +233,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab29"></a><h2 class="section">Comparison</h2>
+<a id="lab13"></a><h2 class="section">Comparison</h2>
 
 </div>
 <div class="code">
@@ -302,7 +302,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab30"></a><h2 class="section">Minimum and maximum</h2>
+<a id="lab14"></a><h2 class="section">Minimum and maximum</h2>
 
 </div>
 <div class="code">
@@ -325,7 +325,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab31"></a><h2 class="section">Conversions</h2>
+<a id="lab15"></a><h2 class="section">Conversions</h2>
 
 <div class="paragraph"> </div>
 
@@ -389,11 +389,11 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab32"></a><h2 class="section">Euclidean divisions for binary integers</h2>
+<a id="lab16"></a><h2 class="section">Euclidean divisions for binary integers</h2>
 
 <div class="paragraph"> </div>
 
-<a id="lab33"></a><h2 class="section">Floor division</h2>
+<a id="lab17"></a><h2 class="section">Floor division</h2>
 
 <div class="paragraph"> </div>
 
@@ -484,7 +484,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab34"></a><h2 class="section">Trunc Division</h2>
+<a id="lab18"></a><h2 class="section">Trunc Division</h2>
 
 <div class="paragraph"> </div>
 
@@ -545,7 +545,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="lab35"></a><h2 class="section">Parity functions</h2>
+<a id="lab19"></a><h2 class="section">Parity functions</h2>
 
 </div>
 <div class="code">
@@ -563,7 +563,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab36"></a><h2 class="section">Division by two</h2>
+<a id="lab20"></a><h2 class="section">Division by two</h2>
 
 <div class="paragraph"> </div>
 
@@ -586,7 +586,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab37"></a><h2 class="section">Square root</h2>
+<a id="lab21"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">

diff --git a/master/corelib/html/Corelib.BinNums.NatDef.html b/master/corelib/html/Corelib.BinNums.NatDef.html
@@ -52,7 +52,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab38"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>
+<a id="lab1"></a><h1 class="section">Binary natural numbers, definitions of operations</h1>
 
 </div>
 <div class="code">
@@ -64,7 +64,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab39"></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="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>
 
 </div>
 <div class="code">
@@ -80,7 +80,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab40"></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="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>
 
 </div>
 <div class="code">
@@ -96,7 +96,7 @@ <h1 class="libtitle">Library Corelib.BinNums.NatDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab41"></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="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>
 
 </div>
 <div class="code">

diff --git a/master/corelib/html/Corelib.BinNums.PosDef.html b/master/corelib/html/Corelib.BinNums.PosDef.html
@@ -49,7 +49,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab1"></a><h1 class="section">Binary positive numbers, operations</h1>
+<a id="lab22"></a><h1 class="section">Binary positive numbers, operations</h1>
 
 <div class="paragraph"> </div>
 
@@ -97,11 +97,11 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h1 class="section">Operations over positive numbers</h1>
+<a id="lab23"></a><h1 class="section">Operations over positive numbers</h1>
 
 <div class="paragraph"> </div>
 
-<a id="lab3"></a><h2 class="section">Successor</h2>
+<a id="lab24"></a><h2 class="section">Successor</h2>
 
 </div>
 <div class="code">
@@ -118,7 +118,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Addition</h2>
+<a id="lab25"></a><h2 class="section">Addition</h2>
 
 </div>
 <div class="code">
@@ -154,7 +154,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab5"></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="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>
 
 </div>
 <div class="code">
@@ -171,7 +171,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></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="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>
 
 </div>
 <div class="code">
@@ -188,7 +188,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">An auxiliary type for subtraction</h2>
+<a id="lab28"></a><h2 class="section">An auxiliary type for subtraction</h2>
 
 </div>
 <div class="code">
@@ -203,7 +203,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></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="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>
 
 </div>
 <div class="code">
@@ -220,7 +220,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></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="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>
 
 </div>
 <div class="code">
@@ -237,7 +237,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>-2</span></h2>
+<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>
 
 </div>
 <div class="code">
@@ -254,7 +254,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Subtraction, result as a mask</h2>
+<a id="lab32"></a><h2 class="section">Subtraction, result as a mask</h2>
 
 </div>
 <div class="code">
@@ -287,7 +287,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></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="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>
 
 </div>
 <div class="code">
@@ -303,7 +303,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Multiplication</h2>
+<a id="lab34"></a><h2 class="section">Multiplication</h2>
 
 </div>
 <div class="code">
@@ -320,7 +320,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Iteration over a positive number</h2>
+<a id="lab35"></a><h2 class="section">Iteration over a positive number</h2>
 
 </div>
 <div class="code">
@@ -337,7 +337,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Division by 2 rounded below but for 1</h2>
+<a id="lab36"></a><h2 class="section">Division by 2 rounded below but for 1</h2>
 
 </div>
 <div class="code">
@@ -370,7 +370,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Comparison on binary positive numbers</h2>
+<a id="lab37"></a><h2 class="section">Comparison on binary positive numbers</h2>
 
 </div>
 <div class="code">
@@ -396,7 +396,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h2 class="section">Boolean equality and comparisons</h2>
+<a id="lab38"></a><h2 class="section">Boolean equality and comparisons</h2>
 
 </div>
 <div class="code">
@@ -418,7 +418,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab18"></a><h2 class="section">A Square Root function for positive numbers</h2>
+<a id="lab39"></a><h2 class="section">A Square Root function for positive numbers</h2>
 
 <div class="paragraph"> </div>
 
@@ -566,7 +566,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab19"></a><h2 class="section">From binary positive numbers to Peano natural numbers</h2>
+<a id="lab40"></a><h2 class="section">From binary positive numbers to Peano natural numbers</h2>
 
 </div>
 <div class="code">
@@ -588,7 +588,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab20"></a><h2 class="section">From Peano natural numbers to binary positive numbers</h2>
+<a id="lab41"></a><h2 class="section">From Peano natural numbers to binary positive numbers</h2>
 
 </div>
 <div class="code">

diff --git a/master/corelib/html/Corelib.Classes.CMorphisms.html b/master/corelib/html/Corelib.Classes.CMorphisms.html
@@ -49,7 +49,7 @@ <h1 class="libtitle">Library Corelib.Classes.CMorphisms</h1>
 </div>
 
 <div class="doc">
-<a id="lab112"></a><h1 class="section">Typeclass-based morphism definition and standard, minimal instances</h1>
+<a id="lab95"></a><h1 class="section">Typeclass-based morphism definition and standard, minimal instances</h1>
 
 
 <div class="paragraph"> </div>
@@ -78,7 +78,7 @@ <h1 class="libtitle">Library Corelib.Classes.CMorphisms</h1>
 </div>
 
 <div class="doc">
-<a id="lab113"></a><h1 class="section">Morphisms.</h1>
+<a id="lab96"></a><h1 class="section">Morphisms.</h1>
 
 
 <div class="paragraph"> </div>