Documentation of branch “master” at bbe6a7fd

coq · Feb 12, 2025 · 6338751 · 6338751
1 parent 54d0fed
commit 6338751
Show file tree

Hide file tree

Showing 67 changed files with 142 additions and 142 deletions.
diff --git a/master/corelib/Corelib.BinNums.IntDef.html b/master/corelib/Corelib.BinNums.IntDef.html
@@ -276,7 +276,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="lab25"></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="lab22"></a><h2 class="section">Doubling and variants</h2>
+<a id="lab26"></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="lab23"></a><h2 class="section">Subtraction of positive into Z</h2>
+<a id="lab27"></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="lab24"></a><h2 class="section">Addition</h2>
+<a id="lab28"></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="lab25"></a><h2 class="section">Opposite</h2>
+<a id="lab29"></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="lab26"></a><h2 class="section">Subtraction</h2>
+<a id="lab30"></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="lab27"></a><h2 class="section">Multiplication</h2>
+<a id="lab31"></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="lab28"></a><h2 class="section">Power function</h2>
+<a id="lab32"></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="lab29"></a><h2 class="section">Comparison</h2>
+<a id="lab33"></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="lab30"></a><h2 class="section">Minimum and maximum</h2>
+<a id="lab34"></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="lab31"></a><h2 class="section">Conversions</h2>
+<a id="lab35"></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="lab32"></a><h2 class="section">Euclidean divisions for binary integers</h2>
+<a id="lab36"></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="lab37"></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="lab34"></a><h2 class="section">Trunc Division</h2>
+<a id="lab38"></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="lab35"></a><h2 class="section">Parity functions</h2>
+<a id="lab39"></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="lab36"></a><h2 class="section">Division by two</h2>
+<a id="lab40"></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="lab37"></a><h2 class="section">Square root</h2>
+<a id="lab41"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">

diff --git a/master/corelib/Corelib.BinNums.NatDef.html b/master/corelib/Corelib.BinNums.NatDef.html
@@ -270,7 +270,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">
@@ -282,7 +282,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">
@@ -298,7 +298,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">
@@ -314,7 +314,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/Corelib.BinNums.PosDef.html b/master/corelib/Corelib.BinNums.PosDef.html
@@ -267,7 +267,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="lab5"></a><h1 class="section">Binary positive numbers, operations</h1>
 
 <div class="paragraph"> </div>
 
@@ -315,11 +315,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="lab6"></a><h1 class="section">Operations over positive numbers</h1>
 
 <div class="paragraph"> </div>
 
-<a id="lab3"></a><h2 class="section">Successor</h2>
+<a id="lab7"></a><h2 class="section">Successor</h2>
 
 </div>
 <div class="code">
@@ -336,7 +336,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Addition</h2>
+<a id="lab8"></a><h2 class="section">Addition</h2>
 
 </div>
 <div class="code">
@@ -372,7 +372,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="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>-1</span></h2>
 
 </div>
 <div class="code">
@@ -389,7 +389,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="lab10"></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">
@@ -406,7 +406,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="lab11"></a><h2 class="section">An auxiliary type for subtraction</h2>
 
 </div>
 <div class="code">
@@ -421,7 +421,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="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>+1</span></h2>
 
 </div>
 <div class="code">
@@ -438,7 +438,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="lab13"></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">
@@ -455,7 +455,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="lab14"></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">
@@ -472,7 +472,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="lab15"></a><h2 class="section">Subtraction, result as a mask</h2>
 
 </div>
 <div class="code">
@@ -505,7 +505,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="lab16"></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">
@@ -521,7 +521,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Multiplication</h2>
+<a id="lab17"></a><h2 class="section">Multiplication</h2>
 
 </div>
 <div class="code">
@@ -538,7 +538,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="lab18"></a><h2 class="section">Iteration over a positive number</h2>
 
 </div>
 <div class="code">
@@ -555,7 +555,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="lab19"></a><h2 class="section">Division by 2 rounded below but for 1</h2>
 
 </div>
 <div class="code">
@@ -588,7 +588,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="lab20"></a><h2 class="section">Comparison on binary positive numbers</h2>
 
 </div>
 <div class="code">
@@ -614,7 +614,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="lab21"></a><h2 class="section">Boolean equality and comparisons</h2>
 
 </div>
 <div class="code">
@@ -636,7 +636,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="lab22"></a><h2 class="section">A Square Root function for positive numbers</h2>
 
 <div class="paragraph"> </div>
 
@@ -784,7 +784,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="lab23"></a><h2 class="section">From binary positive numbers to Peano natural numbers</h2>
 
 </div>
 <div class="code">
@@ -806,7 +806,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="lab24"></a><h2 class="section">From Peano natural numbers to binary positive numbers</h2>
 
 </div>
 <div class="code">

diff --git a/master/corelib/Corelib.Classes.CMorphisms.html b/master/corelib/Corelib.Classes.CMorphisms.html
@@ -267,7 +267,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="lab82"></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="lab113"></a><h1 class="section">Morphisms.</h1>
+<a id="lab83"></a><h1 class="section">Morphisms.</h1>
 
 
 <div class="paragraph"> </div>