aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_lemma_A.html
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-22 13:43:08 +0200
committerEnrico Tassi2019-05-22 15:34:14 +0200
commit748d716efb2f2f75946c8386e441ce1789806a39 (patch)
treefe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_lemma_A.html
parent415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_lemma_A.html')
-rw-r--r--docs/htmldoc/index_lemma_A.html89
1 files changed, 51 insertions, 38 deletions
diff --git a/docs/htmldoc/index_lemma_A.html b/docs/htmldoc/index_lemma_A.html
index fa3086e..ba5d7b7 100644
--- a/docs/htmldoc/index_lemma_A.html
+++ b/docs/htmldoc/index_lemma_A.html
@@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
-<title>mathcomp.ssreflect.tuple</title>
+<title>mathcomp.test_suite.hierarchy_test</title>
</head>
<body>
@@ -47,7 +47,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -79,14 +79,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -111,7 +111,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -143,7 +143,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -175,7 +175,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -207,7 +207,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -239,7 +239,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -271,7 +271,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -303,14 +303,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -335,7 +335,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -367,7 +367,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -399,7 +399,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -431,14 +431,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -463,7 +463,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
<hr/><a name="lemma_A"></a><h2>A (lemma)</h2>
@@ -509,6 +509,7 @@
<a href="mathcomp.solvable.abelian.html#abelian_type_abelem">abelian_type_abelem</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#abelian_type_homocyclic">abelian_type_homocyclic</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#abelian_rank1_cyclic">abelian_rank1_cyclic</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
+<a href="mathcomp.solvable.abelian.html#abelian_type_pgroup">abelian_type_pgroup</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#abelian_structure">abelian_structure</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#abelian_type_sorted">abelian_type_sorted</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
<a href="mathcomp.solvable.abelian.html#abelian_type_gt1">abelian_type_gt1</a> [in <a href="mathcomp.solvable.abelian.html">mathcomp.solvable.abelian</a>]<br/>
@@ -523,9 +524,6 @@
<a href="mathcomp.solvable.nilpotent.html#abelian_nil">abelian_nil</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#abelian_gen">abelian_gen</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
<a href="mathcomp.fingroup.fingroup.html#abelian1">abelian1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.field.closed_field.html#abstrXP">abstrXP</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#abstrX_mulM">abstrX_mulM</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
-<a href="mathcomp.field.closed_field.html#abstrX1">abstrX1</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#abszE">abszE</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#abszEsg">abszEsg</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
<a href="mathcomp.algebra.ssrint.html#abszEsign">abszEsign</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/>
@@ -614,9 +612,12 @@
<a href="mathcomp.algebra.mxalgebra.html#addmx_sub_adds">addmx_sub_adds</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.algebra.mxalgebra.html#addmx_sub">addmx_sub</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnA">addnA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#addnABC">addnABC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnAC">addnAC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnACA">addnACA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnBA">addnBA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#addnBAC">addnBAC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.ssrnat.html#addnBCA">addnBCA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnC">addnC</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnCA">addnCA</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#addnE">addnE</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
@@ -868,12 +869,21 @@
<a href="mathcomp.field.algebraics_fundamentals.html#alg_integral">alg_integral</a> [in <a href="mathcomp.field.algebraics_fundamentals.html">mathcomp.field.algebraics_fundamentals</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allP">allP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allpairsP">allpairsP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairsPdep">allpairsPdep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.tuple.html#allpairs_tupleP">allpairs_tupleP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allpairs_uniq">allpairs_uniq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairs_f">allpairs_f</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairs_uniq_dep">allpairs_uniq_dep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allpairs_catr">allpairs_catr</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairs_f_dep">allpairs_f_dep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairs_mapr">allpairs_mapr</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allpairs_mapl">allpairs_mapl</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allpairs_cat">allpairs_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#allPn">allPn</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#allPP">allPP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.tuple.html#all_tnthP">all_tnthP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#all_iffP">all_iffP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#all_iffLR">all_iffLR</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#all_map">all_map</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#all_nthP">all_nthP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#all_pred1_nseq">all_pred1_nseq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
@@ -893,6 +903,7 @@
<a href="mathcomp.ssreflect.seq.html#all_filterP">all_filterP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.ssreflect.seq.html#all_count">all_count</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.algebra.poly.html#all_roots_prod_XsubC">all_roots_prod_XsubC</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/>
+<a href="mathcomp.ssreflect.seq.html#all2E">all2E</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/>
<a href="mathcomp.solvable.alt.html#Alt_trans">Alt_trans</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.solvable.alt.html#Alt_index">Alt_index</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.solvable.alt.html#Alt_norm">Alt_norm</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
@@ -910,6 +921,8 @@
<a href="mathcomp.field.falgebra.html#amulr_inj">amulr_inj</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
<a href="mathcomp.character.mxrepresentation.html#annihilator_mxP">annihilator_mxP</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
<a href="mathcomp.ssreflect.ssrnat.html#anti_leq">anti_leq</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/>
+<a href="mathcomp.ssreflect.eqtype.html#anti_mono">anti_mono</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
+<a href="mathcomp.ssreflect.eqtype.html#anti_mono_in">anti_mono_in</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/>
<a href="mathcomp.fingroup.perm.html#apermE">apermE</a> [in <a href="mathcomp.fingroup.perm.html">mathcomp.fingroup.perm</a>]<br/>
<a href="mathcomp.solvable.alt.html#aperm_faithful">aperm_faithful</a> [in <a href="mathcomp.solvable.alt.html">mathcomp.solvable.alt</a>]<br/>
<a href="mathcomp.fingroup.action.html#aperm_is_action">aperm_is_action</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/>
@@ -1074,7 +1087,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -1106,14 +1119,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -1138,7 +1151,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -1170,7 +1183,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -1202,7 +1215,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -1234,7 +1247,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -1266,7 +1279,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -1298,7 +1311,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -1330,14 +1343,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -1362,7 +1375,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -1394,7 +1407,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -1426,7 +1439,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -1458,14 +1471,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -1490,7 +1503,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
</div>