Documentation of branch “master” at 9c5edb2a

coq · Feb 14, 2025 · 6c5b09d · 6c5b09d
1 parent d7eaf50
commit 6c5b09d
Show file tree

Hide file tree

Showing 281 changed files with 1,354 additions and 1,354 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="lab25"></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>
 
@@ -291,7 +291,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab26"></a><h2 class="section">Doubling and variants</h2>
+<a id="lab6"></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="lab27"></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">
@@ -347,7 +347,7 @@ <h1 class="libtitle">Library Corelib.BinNums.IntDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab28"></a><h2 class="section">Addition</h2>
+<a id="lab8"></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="lab29"></a><h2 class="section">Opposite</h2>
+<a id="lab9"></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="lab30"></a><h2 class="section">Subtraction</h2>
+<a id="lab10"></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="lab31"></a><h2 class="section">Multiplication</h2>
+<a id="lab11"></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="lab32"></a><h2 class="section">Power function</h2>
+<a id="lab12"></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="lab33"></a><h2 class="section">Comparison</h2>
+<a id="lab13"></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="lab34"></a><h2 class="section">Minimum and maximum</h2>
+<a id="lab14"></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="lab35"></a><h2 class="section">Conversions</h2>
+<a id="lab15"></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="lab36"></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="lab37"></a><h2 class="section">Floor division</h2>
+<a id="lab17"></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="lab38"></a><h2 class="section">Trunc Division</h2>
+<a id="lab18"></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="lab39"></a><h2 class="section">Parity functions</h2>
+<a id="lab19"></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="lab40"></a><h2 class="section">Division by two</h2>
+<a id="lab20"></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="lab41"></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/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="lab5"></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>
 
@@ -315,11 +315,11 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></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="lab7"></a><h2 class="section">Successor</h2>
+<a id="lab24"></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="lab8"></a><h2 class="section">Addition</h2>
+<a id="lab25"></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="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>
+<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">
@@ -389,7 +389,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>
+<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">
@@ -406,7 +406,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></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">
@@ -421,7 +421,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>
+<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">
@@ -438,7 +438,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>
+<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">
@@ -455,7 +455,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>
+<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">
@@ -472,7 +472,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></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">
@@ -505,7 +505,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<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>
+<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">
@@ -521,7 +521,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h2 class="section">Multiplication</h2>
+<a id="lab34"></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="lab18"></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">
@@ -555,7 +555,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab19"></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">
@@ -588,7 +588,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab20"></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">
@@ -614,7 +614,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab21"></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">
@@ -636,7 +636,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab22"></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>
 
@@ -784,7 +784,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab23"></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">
@@ -806,7 +806,7 @@ <h1 class="libtitle">Library Corelib.BinNums.PosDef</h1>
 </div>
 
 <div class="doc">
-<a id="lab24"></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/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="lab82"></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>
@@ -296,7 +296,7 @@ <h1 class="libtitle">Library Corelib.Classes.CMorphisms</h1>
 </div>
 
 <div class="doc">
-<a id="lab83"></a><h1 class="section">Morphisms.</h1>
+<a id="lab96"></a><h1 class="section">Morphisms.</h1>
 
 
 <div class="paragraph"> </div>

diff --git a/master/corelib/Corelib.Classes.CRelationClasses.html b/master/corelib/Corelib.Classes.CRelationClasses.html
@@ -267,7 +267,7 @@ <h1 class="libtitle">Library Corelib.Classes.CRelationClasses</h1>
 </div>
 
 <div class="doc">
-<a id="lab90"></a><h1 class="section">Typeclass-based relations, tactics and standard instances</h1>
+<a id="lab91"></a><h1 class="section">Typeclass-based relations, tactics and standard instances</h1>
 
 
 <div class="paragraph"> </div>
@@ -672,7 +672,7 @@ <h1 class="libtitle">Library Corelib.Classes.CRelationClasses</h1>
 We can already dualize all these properties. 
 <div class="paragraph"> </div>
 
-<a id="lab91"></a><h1 class="section">Standard instances.</h1>
+<a id="lab92"></a><h1 class="section">Standard instances.</h1>
 
 </div>
 <div class="code">
@@ -825,7 +825,7 @@ <h1 class="libtitle">Library Corelib.Classes.CRelationClasses</h1>
 </div>
 
 <div class="doc">
-<a id="lab92"></a><h3 class="section">Partial Order.</h3>
+<a id="lab93"></a><h3 class="section">Partial Order.</h3>
 
    A partial order is a preorder which is additionally antisymmetric.
    We give an equivalent definition, up-to an equivalence crelation

diff --git a/master/corelib/Corelib.Classes.Equivalence.html b/master/corelib/Corelib.Classes.Equivalence.html
@@ -267,7 +267,7 @@ <h1 class="libtitle">Library Corelib.Classes.Equivalence</h1>
 </div>
 
 <div class="doc">
-<a id="lab84"></a><h1 class="section">Typeclass-based setoids. Definitions on <span class="inlinecode"><span class="id" title="var">Equivalence</span></span>.</h1>
+<a id="lab86"></a><h1 class="section">Typeclass-based setoids. Definitions on <span class="inlinecode"><span class="id" title="var">Equivalence</span></span>.</h1>
 
 
 <div class="paragraph"> </div>

diff --git a/master/corelib/Corelib.Classes.Init.html b/master/corelib/Corelib.Classes.Init.html
@@ -267,7 +267,7 @@ <h1 class="libtitle">Library Corelib.Classes.Init</h1>
 </div>
 
 <div class="doc">
-<a id="lab89"></a><h1 class="section">Initialization code for typeclasses, setting up the default tactic</h1>
+<a id="lab90"></a><h1 class="section">Initialization code for typeclasses, setting up the default tactic</h1>
 
    for instance search.