Skip to content

Commit 5aab615

Browse files
affeldt-aistaffeldt-aist
authored
mca doc 1.10.0 (#110)
1 parent c79cca9 commit 5aab615

File tree

252 files changed

+153130
-6
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

252 files changed

+153130
-6
lines changed

‎analysis/htmldoc_1_10_0/coq2html.css‎

Lines changed: 214 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,214 @@
1+
2+
/* Classes:
3+
h1.title the title of the page
4+
div.coq encloses all generated body
5+
div.doc contents of (** *) comments
6+
div.footer footer
7+
summary.toggleproof "Proof." line
8+
div.proofscript contents of proof script
9+
span.docright contents of (**r *) comments
10+
span.bracket contents of [ ] within comments
11+
span.comment contents of (* *) comments
12+
span.string string literals "..."
13+
span.kwd Coq keyword
14+
span.id any other identifier
15+
*/
16+
17+
* {
18+
box-sizing: border-box;
19+
}
20+
21+
body {
22+
font-family: Arial, Helvetica;
23+
margin: 8px;
24+
font-size: large;
25+
}
26+
27+
main {
28+
margin-top: 0em;
29+
}
30+
31+
div.sidebar {
32+
left: 8px;
33+
height: 100vh;
34+
width: 250px;
35+
position: fixed;
36+
overflow-y: auto;
37+
}
38+
div.sidebar li {
39+
list-style: none;
40+
}
41+
div.sidebar ul {
42+
padding-inline-start: 10px;
43+
}
44+
45+
h1 {
46+
font-size: 1.5em;
47+
font-weight: bold;
48+
align-items: center;
49+
}
50+
h2 {
51+
margin-left: 0em;
52+
padding: 0px;
53+
color: #580909
54+
}
55+
56+
h3 {
57+
margin-left: 0em;
58+
padding: 0px;
59+
color: #C05001;
60+
}
61+
62+
h1, h2, h3 {
63+
font-family: sans-serif;
64+
65+
}
66+
67+
div.coq {
68+
margin-left: 250px; /* サイドバーの分だけ右にずらす */
69+
margin-right: 0%;
70+
font-family: monospace;
71+
72+
overflow-x: auto;
73+
overflow-y: auto;
74+
height: 100vh;
75+
}
76+
77+
div.doc {
78+
margin-left: 0%;
79+
margin-top: 0.2em;
80+
margin-bottom: 0.5em;
81+
font-family: serif;
82+
background-color: #f2f1f1;
83+
}
84+
85+
summary.toggleproof {
86+
list-style-position: outside;
87+
font-size: 0.8em;
88+
text-decoration: underline;
89+
}
90+
91+
div.proofscript {
92+
font-size: 0.8em;
93+
}
94+
95+
div.footer {
96+
margin-top: 1em;
97+
margin-bottom: 1em;
98+
font-size: 0.8em;
99+
font-style: italic;
100+
}
101+
102+
span.docright {
103+
position: absolute;
104+
left: 60%;
105+
width: 40%;
106+
font-family: serif;
107+
}
108+
109+
span.bracket {
110+
font-family: monospace;
111+
color: #008000;
112+
}
113+
114+
span.vernacular {
115+
color: #9400d3;
116+
}
117+
118+
span.gallina-kwd {
119+
color: #228b22;
120+
}
121+
122+
.hierarchy-builder {
123+
color: #ff4500;
124+
margin: 2em 0;
125+
border: solid 1px #cd0000;
126+
}
127+
128+
span.comment {
129+
color: #008000;
130+
}
131+
132+
span.string {
133+
color: Maroon;
134+
}
135+
136+
a:visited {color : #0000BF; text-decoration : none; }
137+
a:link {color : #0000BF; text-decoration : none; }
138+
a:hover {text-decoration : none; }
139+
a:active {text-decoration : none; }
140+
141+
.coq :target {
142+
background-color: yellow;
143+
transition: background-color 0.5s;
144+
}
145+
146+
pre.ssrdoc {
147+
border: solid 2px;
148+
padding-left: 1em;
149+
padding-right: 1em;
150+
}
151+
152+
div.ssrdoc {
153+
border: solid 2px;
154+
padding-left: 1em;
155+
padding-right: 1em;
156+
}
157+
158+
div.content {
159+
margin-left: 0px;
160+
padding-left: 12px;
161+
}
162+
163+
.warning {
164+
color: #cd0000;
165+
}
166+
167+
img.img-darkmode-enable {
168+
isolation: auto;
169+
}
170+
171+
.darkmode--activated .sidebar {
172+
color: white;
173+
}
174+
175+
.darkmode--activated .sidebar h2 {
176+
color: #a7f6f6;
177+
}
178+
179+
.darkmode--activated span.katex {
180+
color: white;
181+
}
182+
183+
.darkmode--activated span.docright {
184+
color: white;
185+
}
186+
187+
@media screen and (max-width:960px) {
188+
189+
body {
190+
font-family: Arial, Helvetica;
191+
margin-left: 0.5em;
192+
margin-right: 0.5em;
193+
font-size: large;
194+
}
195+
196+
div.doc {
197+
margin-left: 0%;
198+
margin-top: 0.2em;
199+
margin-bottom: 0.5em;
200+
font-family: serif;
201+
background-color: #f2f1f1;
202+
}
203+
204+
div.coq {
205+
margin-left: 1%;
206+
margin-right: 1%;
207+
font-family: monospace;
208+
}
209+
210+
}
211+
212+
.darkmode-toggle {
213+
z-index: 9999 !important;
214+
}

‎analysis/htmldoc_1_10_0/coq2html.js‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
2+
function renderMarkdowns()
3+
{
4+
const md = markdownit({html:true})
5+
.use(texmath, { engine: katex,
6+
delimiters: 'dollars'} );
7+
const elements = document.querySelectorAll('.markdown,.md');
8+
for (let elem of elements) {
9+
elem.innerHTML = md.render(elem.textContent);
10+
}
11+
}
12+
13+
function showDarkmodeWidget()
14+
{
15+
new Darkmode({
16+
time: '0.1s',
17+
label: '🌓',
18+
}).showWidget();
19+
}
20+
21+
function setUpSavingDetails() {
22+
$('details').on('toggle', function(event) {
23+
var id = $(this).attr('id')
24+
var isOpen = $(this).attr('open')
25+
window.localStorage.setItem('details-'+id, isOpen)
26+
})
27+
28+
function setDetailOpenStatus(item) {
29+
if (item.includes('details-')) {
30+
var id = item.split('details-')[1];
31+
var status = window.localStorage.getItem(item)
32+
if (status == 'open' || status == 'undefined'){
33+
$("#"+CSS.escape(id)).attr('open',true)
34+
}
35+
}
36+
}
37+
38+
$( document ).ready(function() {
39+
for (var i = 0; i < localStorage.length; i++) {
40+
setDetailOpenStatus(localStorage.key(i));
41+
}
42+
});
43+
}
44+
45+
function init()
46+
{
47+
renderMarkdowns();
48+
showDarkmodeWidget();
49+
setUpSavingDetails();
50+
}

‎analysis/htmldoc_1_10_0/dependency_graph.map‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
<map id="depend" name="depend">
2+
<area shape="rect" id="node1" href="mathcomp.analysis_stdlib.Rstruct_topology.html" title="Rstruct_topology" alt="" coords="693,1443,787,1467"/>
3+
<area shape="rect" id="node2" href="mathcomp.analysis_stdlib.showcase.uniform_bigO.html" title="uniform_bigO" alt="" coords="700,1491,780,1515"/>
4+
<area shape="rect" id="node3" href="mathcomp.classical.all_classical.html" title="all_classical" alt="" coords="735,435,805,459"/>
5+
<area shape="rect" id="node4" href="mathcomp.reals.prodnormedzmodule.html" title="prodnormedzmodule" alt="" coords="714,531,826,555"/>
6+
<area shape="rect" id="node5" href="mathcomp.analysis.topology_theory.topology_structure.html" title="topology_structure" alt="" coords="1098,483,1200,507"/>
7+
<area shape="rect" id="node28" href="mathcomp.reals.all_reals.html" title="all_reals" alt="" coords="476,627,528,651"/>
8+
<area shape="rect" id="node89" href="mathcomp.analysis.topology_theory.connected.html" title="connected" alt="" coords="1182,723,1243,747"/>
9+
<area shape="rect" id="node98" href="mathcomp.analysis.topology_theory.quotient_topology.html" title="quotient_topology" alt="" coords="1293,675,1392,699"/>
10+
<area shape="rect" id="node102" href="mathcomp.analysis.topology_theory.uniform_structure.html" title="uniform_structure" alt="" coords="1037,531,1135,555"/>
11+
<area shape="rect" id="node6" href="mathcomp.classical.boolp.html" title="boolp" alt="" coords="880,51,918,75"/>
12+
<area shape="rect" id="node7" href="mathcomp.classical.contra.html" title="contra" alt="" coords="881,99,922,123"/>
13+
<area shape="rect" id="node13" href="mathcomp.classical.wochoice.html" title="wochoice" alt="" coords="873,147,930,171"/>
14+
<area shape="rect" id="node8" href="mathcomp.classical.cardinality.html" title="cardinality" alt="" coords="736,291,799,315"/>
15+
<area shape="rect" id="node9" href="mathcomp.classical.fsbigop.html" title="fsbigop" alt="" coords="745,339,791,363"/>
16+
<area shape="rect" id="node14" href="mathcomp.classical.filter.html" title="filter" alt="" coords="752,387,788,411"/>
17+
<area shape="rect" id="node10" href="mathcomp.classical.classical_orders.html" title="classical_orders" alt="" coords="616,387,704,411"/>
18+
<area shape="rect" id="node11" href="mathcomp.classical.classical_sets.html" title="classical_sets" alt="" coords="777,195,853,219"/>
19+
<area shape="rect" id="node12" href="mathcomp.classical.functions.html" title="functions" alt="" coords="687,243,743,267"/>
20+
<area shape="rect" id="node15" href="mathcomp.classical.set_interval.html" title="set_interval" alt="" coords="627,339,695,363"/>
21+
<area shape="rect" id="node21" href="mathcomp.reals.reals.html" title="reals" alt="" coords="378,531,414,555"/>
22+
<area shape="rect" id="node16" href="mathcomp.classical.internal_Eqdep_dec.html" title="internal_Eqdep_dec" alt="" coords="845,3,953,27"/>
23+
<area shape="rect" id="node17" href="mathcomp.classical.mathcomp_extra.html" title="mathcomp_extra" alt="" coords="684,3,776,27"/>
24+
<area shape="rect" id="node18" href="mathcomp.classical.unstable.html" title="unstable" alt="" coords="683,51,734,75"/>
25+
<area shape="rect" id="node19" href="mathcomp.reals.interval_inference.html" title="interval_inference" alt="" coords="595,483,694,507"/>
26+
<area shape="rect" id="node20" href="mathcomp.analysis.forms.html" title="forms" alt="" coords="787,147,825,171"/>
27+
<area shape="rect" id="node22" href="mathcomp.reals.signed.html" title="signed" alt="" coords="692,99,734,123"/>
28+
<area shape="rect" id="node30" href="mathcomp.reals.constructive_ereal.html" title="constructive_ereal" alt="" coords="203,531,303,555"/>
29+
<area shape="rect" id="node33" href="mathcomp.analysis.topology_theory.pseudometric_structure.html" title="pseudometric_structure" alt="" coords="649,579,774,603"/>
30+
<area shape="rect" id="node41" href="mathcomp.analysis.derive.html" title="derive" alt="" coords="1325,1395,1366,1419"/>
31+
<area shape="rect" id="node23" href="mathcomp.experimental_reals.discrete.html" title="discrete" alt="" coords="52,579,100,603"/>
32+
<area shape="rect" id="node31" href="mathcomp.reals.real_interval.html" title="real_interval" alt="" coords="148,579,221,603"/>
33+
<area shape="rect" id="node32" href="mathcomp.reals_stdlib.nsatz_realtype.html" title="nsatz_realtype" alt="" coords="269,579,350,603"/>
34+
<area shape="rect" id="node34" href="mathcomp.reals_stdlib.Rstruct.html" title="Rstruct" alt="" coords="403,963,449,987"/>
35+
<area shape="rect" id="node24" href="mathcomp.experimental_reals.realseq.html" title="realseq" alt="" coords="5,627,50,651"/>
36+
<area shape="rect" id="node26" href="mathcomp.experimental_reals.realsum.html" title="realsum" alt="" coords="3,675,52,699"/>
37+
<area shape="rect" id="node25" href="mathcomp.experimental_reals.distr.html" title="distr" alt="" coords="9,723,45,747"/>
38+
<area shape="rect" id="node27" href="mathcomp.experimental_reals.xfinmap.html" title="xfinmap" alt="" coords="50,531,102,555"/>
39+
<area shape="rect" id="node29" href="mathcomp.analysis.topology_theory.discrete_topology.html" title="discrete_topology" alt="" coords="529,867,627,891"/>
40+
<area shape="rect" id="node85" href="mathcomp.analysis.topology_theory.bool_topology.html" title="bool_topology" alt="" coords="711,915,792,939"/>
41+
<area shape="rect" id="node91" href="mathcomp.analysis.topology_theory.nat_topology.html" title="nat_topology" alt="" coords="551,915,625,939"/>
42+
<area shape="rect" id="node92" href="mathcomp.analysis.topology_theory.separation_axioms.html" title="separation_axioms" alt="" coords="858,915,960,939"/>
43+
<area shape="rect" id="node87" href="mathcomp.analysis.topology_theory.compact.html" title="compact" alt="" coords="685,627,737,651"/>
44+
<area shape="rect" id="node93" href="mathcomp.analysis.topology_theory.matrix_topology.html" title="matrix_topology" alt="" coords="1115,819,1206,843"/>
45+
<area shape="rect" id="node35" href="mathcomp.analysis.all_analysis.html" title="all_analysis" alt="" coords="1329,2451,1397,2475"/>
46+
<area shape="rect" id="node36" href="mathcomp.analysis.cantor.html" title="cantor" alt="" coords="1116,1203,1157,1227"/>
47+
<area shape="rect" id="node37" href="mathcomp.analysis.charge.html" title="charge" alt="" coords="1493,2211,1536,2235"/>
48+
<area shape="rect" id="node38" href="mathcomp.analysis.ftc.html" title="ftc" alt="" coords="1501,2259,1537,2283"/>
49+
<area shape="rect" id="node48" href="mathcomp.analysis.trigo.html" title="trigo" alt="" coords="1504,2307,1540,2331"/>
50+
<area shape="rect" id="node39" href="mathcomp.analysis.convex.html" title="convex" alt="" coords="1418,1491,1463,1515"/>
51+
<area shape="rect" id="node40" href="mathcomp.analysis.exp.html" title="exp" alt="" coords="1426,1587,1462,1611"/>
52+
<area shape="rect" id="node47" href="mathcomp.analysis.measurable_realfun.html" title="measurable_realfun" alt="" coords="1391,1635,1497,1659"/>
53+
<area shape="rect" id="node42" href="mathcomp.analysis.realfun.html" title="realfun" alt="" coords="1322,1443,1367,1467"/>
54+
<area shape="rect" id="node72" href="mathcomp.analysis.lebesgue_stieltjes_measure.html" title="lebesgue_stieltjes_measure" alt="" coords="1235,1587,1378,1611"/>
55+
<area shape="rect" id="node43" href="mathcomp.analysis.ereal.html" title="ereal" alt="" coords="1008,1011,1044,1035"/>
56+
<area shape="rect" id="node44" href="mathcomp.analysis.tvs.html" title="tvs" alt="" coords="1008,1059,1044,1083"/>
57+
<area shape="rect" id="node81" href="mathcomp.analysis.normedtype_theory.num_normedtype.html" title="num_normedtype" alt="" coords="931,1107,1027,1131"/>
58+
<area shape="rect" id="node45" href="mathcomp.analysis.esum.html" title="esum" alt="" coords="1228,1491,1265,1515"/>
59+
<area shape="rect" id="node46" href="mathcomp.analysis.measure.html" title="measure" alt="" coords="1221,1539,1272,1563"/>
60+
<area shape="rect" id="node71" href="mathcomp.analysis.lebesgue_measure.html" title="lebesgue_measure" alt="" coords="1394,1683,1494,1707"/>
61+
<area shape="rect" id="node51" href="mathcomp.analysis.gauss_integral.html" title="gauss_integral" alt="" coords="1482,2355,1562,2379"/>
62+
<area shape="rect" id="node84" href="mathcomp.analysis.pi_irrational.html" title="pi_irrational" alt="" coords="1548,2403,1619,2427"/>
63+
<area shape="rect" id="node49" href="mathcomp.analysis.function_spaces.html" title="function_spaces" alt="" coords="1092,1011,1181,1035"/>
64+
<area shape="rect" id="node50" href="mathcomp.analysis.homotopy_theory.wedge_sigT.html" title="wedge_sigT" alt="" coords="1214,1059,1284,1083"/>
65+
<area shape="rect" id="node54" href="mathcomp.analysis.homotopy_theory.continuous_path.html" title="continuous_path" alt="" coords="1209,1107,1300,1131"/>
66+
<area shape="rect" id="node52" href="mathcomp.analysis.probability.html" title="probability" alt="" coords="1384,2403,1448,2427"/>
67+
<area shape="rect" id="node53" href="mathcomp.analysis.hoelder.html" title="hoelder" alt="" coords="1292,2259,1340,2283"/>
68+
<area shape="rect" id="node55" href="mathcomp.analysis.homotopy_theory.homotopy.html" title="homotopy" alt="" coords="1225,1155,1284,1179"/>
69+
<area shape="rect" id="node56" href="mathcomp.analysis.kernel.html" title="kernel" alt="" coords="1389,2307,1430,2331"/>
70+
<area shape="rect" id="node57" href="mathcomp.analysis.landau.html" title="landau" alt="" coords="1225,1347,1268,1371"/>
71+
<area shape="rect" id="node58" href="mathcomp.analysis.sequences.html" title="sequences" alt="" coords="1217,1395,1276,1419"/>
72+
<area shape="rect" id="node83" href="mathcomp.analysis.numfun.html" title="numfun" alt="" coords="1222,1443,1271,1467"/>
73+
<area shape="rect" id="node59" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral.html" title="lebesgue_Rintegral" alt="" coords="1396,2067,1501,2091"/>
74+
<area shape="rect" id="node60" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation.html" title="lebesgue_integral_differentiation" alt="" coords="1210,2115,1382,2139"/>
75+
<area shape="rect" id="node61" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under.html" title="lebesgue_integral_under" alt="" coords="1430,2115,1560,2139"/>
76+
<area shape="rect" id="node65" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral.html" title="lebesgue_integral" alt="" coords="1410,2163,1506,2187"/>
77+
<area shape="rect" id="node62" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable.html" title="lebesgue_integrable" alt="" coords="1394,1971,1503,1995"/>
78+
<area shape="rect" id="node63" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence.html" title="lebesgue_integral_dominated_convergence" alt="" coords="1338,2019,1559,2043"/>
79+
<area shape="rect" id="node64" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini.html" title="lebesgue_integral_fubini" alt="" coords="1567,2067,1698,2091"/>
80+
<area shape="rect" id="node66" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_approximation.html" title="lebesgue_integral_approximation" alt="" coords="1362,1827,1535,1851"/>
81+
<area shape="rect" id="node67" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence.html" title="lebesgue_integral_monotone_convergence" alt="" coords="1339,1875,1558,1899"/>
82+
<area shape="rect" id="node69" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg.html" title="lebesgue_integral_nonneg" alt="" coords="1380,1923,1518,1947"/>
83+
<area shape="rect" id="node68" href="mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition.html" title="lebesgue_integral_definition" alt="" coords="1370,1779,1520,1803"/>
84+
<area shape="rect" id="node70" href="mathcomp.analysis.lebesgue_integral_theory.simple_functions.html" title="simple_functions" alt="" coords="1397,1731,1491,1755"/>
85+
<area shape="rect" id="node73" href="mathcomp.analysis.normedtype_theory.complete_normed_module.html" title="complete_normed_module" alt="" coords="768,1251,909,1275"/>
86+
<area shape="rect" id="node74" href="mathcomp.analysis.normedtype_theory.normedtype.html" title="normedtype" alt="" coords="804,1299,873,1323"/>
87+
<area shape="rect" id="node80" href="mathcomp.analysis.showcase.summability.html" title="summability" alt="" coords="803,1347,874,1371"/>
88+
<area shape="rect" id="node75" href="mathcomp.analysis.normedtype_theory.ereal_normedtype.html" title="ereal_normedtype" alt="" coords="748,1155,847,1179"/>
89+
<area shape="rect" id="node76" href="mathcomp.analysis.normedtype_theory.normed_module.html" title="normed_module" alt="" coords="773,1203,863,1227"/>
90+
<area shape="rect" id="node77" href="mathcomp.analysis.normedtype_theory.matrix_normedtype.html" title="matrix_normedtype" alt="" coords="957,1251,1064,1275"/>
91+
<area shape="rect" id="node78" href="mathcomp.analysis.normedtype_theory.urysohn.html" title="urysohn" alt="" coords="547,1251,596,1275"/>
92+
<area shape="rect" id="node79" href="mathcomp.analysis.normedtype_theory.vitali_lemma.html" title="vitali_lemma" alt="" coords="644,1251,720,1275"/>
93+
<area shape="rect" id="node82" href="mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule.html" title="pseudometric_normed_Zmodule" alt="" coords="895,1155,1064,1179"/>
94+
<area shape="rect" id="node86" href="mathcomp.analysis.topology_theory.topology.html" title="topology" alt="" coords="1002,963,1055,987"/>
95+
<area shape="rect" id="node88" href="mathcomp.analysis.topology_theory.product_topology.html" title="product_topology" alt="" coords="663,675,760,699"/>
96+
<area shape="rect" id="node96" href="mathcomp.analysis.topology_theory.order_topology.html" title="order_topology" alt="" coords="669,723,754,747"/>
97+
<area shape="rect" id="node90" href="mathcomp.analysis.topology_theory.subspace_topology.html" title="subspace_topology" alt="" coords="964,819,1067,843"/>
98+
<area shape="rect" id="node99" href="mathcomp.analysis.topology_theory.sigT_topology.html" title="sigT_topology" alt="" coords="874,867,955,891"/>
99+
<area shape="rect" id="node100" href="mathcomp.analysis.topology_theory.subtype_topology.html" title="subtype_topology" alt="" coords="1003,867,1100,891"/>
100+
<area shape="rect" id="node94" href="mathcomp.analysis.topology_theory.num_topology.html" title="num_topology" alt="" coords="671,771,752,795"/>
101+
<area shape="rect" id="node95" href="mathcomp.analysis.topology_theory.one_point_compactification.html" title="one_point_compactification" alt="" coords="768,819,916,843"/>
102+
<area shape="rect" id="node97" href="mathcomp.analysis.topology_theory.weak_topology.html" title="weak_topology" alt="" coords="800,771,885,795"/>
103+
<area shape="rect" id="node101" href="mathcomp.analysis.topology_theory.supremum_topology.html" title="supremum_topology" alt="" coords="1031,771,1141,795"/>
104+
</map>

‎analysis/htmldoc_1_10_0/dependency_graph.png‎

214 KB
Loading

0 commit comments

Comments
 (0)