-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
0d3db1c
commit 6960467
Showing
231 changed files
with
141,599 additions
and
6 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,202 @@ | ||
|
|
||
| /* Classes: | ||
| h1.title the title of the page | ||
| div.coq encloses all generated body | ||
| div.doc contents of (** *) comments | ||
| div.footer footer | ||
| summary.toggleproof "Proof." line | ||
| div.proofscript contents of proof script | ||
| span.docright contents of (**r *) comments | ||
| span.bracket contents of [ ] within comments | ||
| span.comment contents of (* *) comments | ||
| span.string string literals "..." | ||
| span.kwd Coq keyword | ||
| span.id any other identifier | ||
| */ | ||
|
|
||
| * { | ||
| box-sizing: border-box; | ||
| } | ||
|
|
||
| body { | ||
| font-family: Arial, Helvetica; | ||
| margin: 8px; | ||
| font-size: large; | ||
| } | ||
|
|
||
| main { | ||
| margin-top: 0em; | ||
| } | ||
|
|
||
| div.sidebar { | ||
| left: 8px; | ||
| height: calc(100vh); | ||
| width: 200px; | ||
| position: fixed; | ||
| overflow-y: scroll; | ||
| } | ||
| div.sidebar li { | ||
| list-style: none; | ||
| } | ||
| div.sidebar ul { | ||
| padding-inline-start: 10px; | ||
| } | ||
|
|
||
| h1 { | ||
| font-size: 1.5em; | ||
| font-weight: bold; | ||
| align-items: center; | ||
| } | ||
| h2 { | ||
| margin-left: 0em; | ||
| padding: 0px; | ||
| color: #580909 | ||
| } | ||
|
|
||
| h3 { | ||
| margin-left: 0em; | ||
| padding: 0px; | ||
| color: #C05001; | ||
| } | ||
|
|
||
| h1, h2, h3 { | ||
| font-family: sans-serif; | ||
|
|
||
| } | ||
|
|
||
| div.coq { | ||
| margin-left: 0%; | ||
| margin-right: 0%; | ||
| font-family: monospace; | ||
| } | ||
|
|
||
| div.doc { | ||
| margin-left: 0%; | ||
| margin-top: 0.2em; | ||
| margin-bottom: 0.5em; | ||
| font-family: serif; | ||
| background-color: #f2f1f1; | ||
| } | ||
|
|
||
| summary.toggleproof { | ||
| list-style-position: outside; | ||
| font-size: 0.8em; | ||
| text-decoration: underline; | ||
| } | ||
|
|
||
| div.proofscript { | ||
| font-size: 0.8em; | ||
| } | ||
|
|
||
| div.footer { | ||
| margin-top: 1em; | ||
| margin-bottom: 1em; | ||
| font-size: 0.8em; | ||
| font-style: italic; | ||
| } | ||
|
|
||
| span.docright { | ||
| position: absolute; | ||
| left: 60%; | ||
| width: 40%; | ||
| font-family: serif; | ||
| } | ||
|
|
||
| span.bracket { | ||
| font-family: monospace; | ||
| color: #008000; | ||
| } | ||
|
|
||
| span.vernacular { | ||
| color: #9400d3; | ||
| } | ||
|
|
||
| span.gallina-kwd { | ||
| color: #228b22; | ||
| } | ||
|
|
||
| .hierarchy-builder { | ||
| color: #ff4500; | ||
| margin: 2em 0; | ||
| border: solid 1px #cd0000; | ||
| } | ||
|
|
||
| span.comment { | ||
| color: #008000; | ||
| } | ||
|
|
||
| span.string { | ||
| color: Maroon; | ||
| } | ||
|
|
||
| a:visited {color : #0000BF; text-decoration : none; } | ||
| a:link {color : #0000BF; text-decoration : none; } | ||
| a:hover {text-decoration : none; } | ||
| a:active {text-decoration : none; } | ||
|
|
||
| .coq :target { | ||
| background-color: yellow; | ||
| transition: background-color 0.5s; | ||
| } | ||
|
|
||
| pre.ssrdoc { | ||
| border: solid 2px; | ||
| padding-left: 1em; | ||
| padding-right: 1em; | ||
| } | ||
|
|
||
| div.ssrdoc { | ||
| border: solid 2px; | ||
| padding-left: 1em; | ||
| padding-right: 1em; | ||
| } | ||
|
|
||
| div.content { | ||
| margin-left: 200px; | ||
| padding-left: 12px; | ||
| } | ||
|
|
||
| .warning { | ||
| color: #cd0000; | ||
| } | ||
|
|
||
| .darkmode--activated .sidebar { | ||
| color: white; | ||
| } | ||
|
|
||
| .darkmode--activated .sidebar h2 { | ||
| color: #a7f6f6; | ||
| } | ||
|
|
||
| .darkmode--activated span.katex { | ||
| color: white; | ||
| } | ||
|
|
||
| .darkmode--activated span.docright { | ||
| color: white; | ||
| } | ||
|
|
||
| @media screen and (max-width:960px) { | ||
|
|
||
| body { | ||
| font-family: Arial, Helvetica; | ||
| margin-left: 0.5em; | ||
| margin-right: 0.5em; | ||
| font-size: large; | ||
| } | ||
|
|
||
| div.doc { | ||
| margin-left: 0%; | ||
| margin-top: 0.2em; | ||
| margin-bottom: 0.5em; | ||
| font-family: serif; | ||
| background-color: #f2f1f1; | ||
| } | ||
|
|
||
| div.coq { | ||
| margin-left: 1%; | ||
| margin-right: 1%; | ||
| font-family: monospace; | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,50 @@ | ||
|
|
||
| function renderMarkdowns() | ||
| { | ||
| const md = markdownit({html:true}) | ||
| .use(texmath, { engine: katex, | ||
| delimiters: 'dollars'} ); | ||
| const elements = document.querySelectorAll('.markdown,.md'); | ||
| for (let elem of elements) { | ||
| elem.innerHTML = md.render(elem.textContent); | ||
| } | ||
| } | ||
|
|
||
| function showDarkmodeWidget() | ||
| { | ||
| new Darkmode({ | ||
| time: '0.1s', | ||
| label: '🌓', | ||
| }).showWidget(); | ||
| } | ||
|
|
||
| function setUpSavingDetails() { | ||
| $('details').on('toggle', function(event) { | ||
| var id = $(this).attr('id') | ||
| var isOpen = $(this).attr('open') | ||
| window.localStorage.setItem('details-'+id, isOpen) | ||
| }) | ||
|
|
||
| function setDetailOpenStatus(item) { | ||
| if (item.includes('details-')) { | ||
| var id = item.split('details-')[1]; | ||
| var status = window.localStorage.getItem(item) | ||
| if (status == 'open' || status == 'undefined'){ | ||
| $("#"+CSS.escape(id)).attr('open',true) | ||
| } | ||
| } | ||
| } | ||
|
|
||
| $( document ).ready(function() { | ||
| for (var i = 0; i < localStorage.length; i++) { | ||
| setDetailOpenStatus(localStorage.key(i)); | ||
| } | ||
| }); | ||
| } | ||
|
|
||
| function init() | ||
| { | ||
| renderMarkdowns(); | ||
| showDarkmodeWidget(); | ||
| setUpSavingDetails(); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,83 @@ | ||
| <map id="depend" name="depend"> | ||
| <area shape="rect" id="node1" href="mathcomp.analysis_stdlib.Rstruct_topology.html" title="Rstruct_topology" alt="" coords="480,963,574,987"/> | ||
| <area shape="rect" id="node2" href="mathcomp.analysis_stdlib.showcase.uniform_bigO.html" title="uniform_bigO" alt="" coords="487,1203,567,1227"/> | ||
| <area shape="rect" id="node3" href="mathcomp.classical.all_classical.html" title="all_classical" alt="" coords="580,435,650,459"/> | ||
| <area shape="rect" id="node4" href="mathcomp.reals.prodnormedzmodule.html" title="prodnormedzmodule" alt="" coords="436,531,548,555"/> | ||
| <area shape="rect" id="node5" href="mathcomp.analysis.topology_theory.topology_structure.html" title="topology_structure" alt="" coords="1005,483,1107,507"/> | ||
| <area shape="rect" id="node26" href="mathcomp.reals.all_reals.html" title="all_reals" alt="" coords="145,627,197,651"/> | ||
| <area shape="rect" id="node69" href="mathcomp.analysis.topology_theory.connected.html" title="connected" alt="" coords="1088,675,1148,699"/> | ||
| <area shape="rect" id="node77" href="mathcomp.analysis.topology_theory.quotient_topology.html" title="quotient_topology" alt="" coords="1185,723,1285,747"/> | ||
| <area shape="rect" id="node81" href="mathcomp.analysis.topology_theory.uniform_structure.html" title="uniform_structure" alt="" coords="947,531,1045,555"/> | ||
| <area shape="rect" id="node6" href="mathcomp.classical.boolp.html" title="boolp" alt="" coords="541,51,579,75"/> | ||
| <area shape="rect" id="node7" href="mathcomp.classical.contra.html" title="contra" alt="" coords="539,99,580,123"/> | ||
| <area shape="rect" id="node13" href="mathcomp.classical.wochoice.html" title="wochoice" alt="" coords="531,147,588,171"/> | ||
| <area shape="rect" id="node8" href="mathcomp.classical.cardinality.html" title="cardinality" alt="" coords="579,291,643,315"/> | ||
| <area shape="rect" id="node9" href="mathcomp.classical.fsbigop.html" title="fsbigop" alt="" coords="590,339,637,363"/> | ||
| <area shape="rect" id="node14" href="mathcomp.classical.filter.html" title="filter" alt="" coords="597,387,633,411"/> | ||
| <area shape="rect" id="node10" href="mathcomp.classical.classical_orders.html" title="classical_orders" alt="" coords="461,387,549,411"/> | ||
| <area shape="rect" id="node11" href="mathcomp.classical.classical_sets.html" title="classical_sets" alt="" coords="522,195,598,219"/> | ||
| <area shape="rect" id="node12" href="mathcomp.classical.functions.html" title="functions" alt="" coords="532,243,588,267"/> | ||
| <area shape="rect" id="node15" href="mathcomp.classical.set_interval.html" title="set_interval" alt="" coords="472,339,540,363"/> | ||
| <area shape="rect" id="node20" href="mathcomp.reals.reals.html" title="reals" alt="" coords="352,531,388,555"/> | ||
| <area shape="rect" id="node16" href="mathcomp.classical.mathcomp_extra.html" title="mathcomp_extra" alt="" coords="557,3,650,27"/> | ||
| <area shape="rect" id="node17" href="mathcomp.reals.interval_inference.html" title="interval_inference" alt="" coords="442,483,542,507"/> | ||
| <area shape="rect" id="node18" href="mathcomp.reals.signed.html" title="signed" alt="" coords="627,51,669,75"/> | ||
| <area shape="rect" id="node19" href="mathcomp.analysis.forms.html" title="forms" alt="" coords="1159,99,1198,123"/> | ||
| <area shape="rect" id="node28" href="mathcomp.reals.constructive_ereal.html" title="constructive_ereal" alt="" coords="166,531,266,555"/> | ||
| <area shape="rect" id="node31" href="mathcomp.analysis.topology_theory.pseudometric_structure.html" title="pseudometric_structure" alt="" coords="657,579,781,603"/> | ||
| <area shape="rect" id="node39" href="mathcomp.analysis.derive.html" title="derive" alt="" coords="1004,1203,1046,1227"/> | ||
| <area shape="rect" id="node21" href="mathcomp.experimental_reals.discrete.html" title="discrete" alt="" coords="545,579,593,603"/> | ||
| <area shape="rect" id="node29" href="mathcomp.reals.nsatz_realtype.html" title="nsatz_realtype" alt="" coords="123,579,204,603"/> | ||
| <area shape="rect" id="node30" href="mathcomp.reals.real_interval.html" title="real_interval" alt="" coords="3,579,75,603"/> | ||
| <area shape="rect" id="node32" href="mathcomp.reals_stdlib.Rstruct.html" title="Rstruct" alt="" coords="292,915,338,939"/> | ||
| <area shape="rect" id="node22" href="mathcomp.experimental_reals.realseq.html" title="realseq" alt="" coords="456,627,501,651"/> | ||
| <area shape="rect" id="node24" href="mathcomp.experimental_reals.realsum.html" title="realsum" alt="" coords="454,675,503,699"/> | ||
| <area shape="rect" id="node23" href="mathcomp.experimental_reals.distr.html" title="distr" alt="" coords="460,723,496,747"/> | ||
| <area shape="rect" id="node25" href="mathcomp.experimental_reals.xfinmap.html" title="xfinmap" alt="" coords="595,531,647,555"/> | ||
| <area shape="rect" id="node27" href="mathcomp.analysis.topology_theory.discrete_topology.html" title="discrete_topology" alt="" coords="216,771,314,795"/> | ||
| <area shape="rect" id="node65" href="mathcomp.analysis.topology_theory.bool_topology.html" title="bool_topology" alt="" coords="314,819,396,843"/> | ||
| <area shape="rect" id="node71" href="mathcomp.analysis.topology_theory.nat_topology.html" title="nat_topology" alt="" coords="192,819,266,843"/> | ||
| <area shape="rect" id="node67" href="mathcomp.analysis.topology_theory.compact.html" title="compact" alt="" coords="642,627,694,651"/> | ||
| <area shape="rect" id="node72" href="mathcomp.analysis.topology_theory.matrix_topology.html" title="matrix_topology" alt="" coords="790,675,882,699"/> | ||
| <area shape="rect" id="node33" href="mathcomp.analysis.all_analysis.html" title="all_analysis" alt="" coords="787,1779,855,1803"/> | ||
| <area shape="rect" id="node34" href="mathcomp.analysis.cantor.html" title="cantor" alt="" coords="630,1251,671,1275"/> | ||
| <area shape="rect" id="node35" href="mathcomp.analysis.charge.html" title="charge" alt="" coords="946,1587,989,1611"/> | ||
| <area shape="rect" id="node36" href="mathcomp.analysis.ftc.html" title="ftc" alt="" coords="962,1635,998,1659"/> | ||
| <area shape="rect" id="node47" href="mathcomp.analysis.gauss_integral.html" title="gauss_integral" alt="" coords="939,1683,1020,1707"/> | ||
| <area shape="rect" id="node48" href="mathcomp.analysis.pi_irrational.html" title="pi_irrational" alt="" coords="1068,1683,1139,1707"/> | ||
| <area shape="rect" id="node37" href="mathcomp.analysis.convex.html" title="convex" alt="" coords="1044,1299,1089,1323"/> | ||
| <area shape="rect" id="node38" href="mathcomp.analysis.exp.html" title="exp" alt="" coords="1047,1395,1083,1419"/> | ||
| <area shape="rect" id="node45" href="mathcomp.analysis.measurable_realfun.html" title="measurable_realfun" alt="" coords="851,1443,958,1467"/> | ||
| <area shape="rect" id="node46" href="mathcomp.analysis.trigo.html" title="trigo" alt="" coords="1047,1635,1083,1659"/> | ||
| <area shape="rect" id="node40" href="mathcomp.analysis.realfun.html" title="realfun" alt="" coords="953,1251,998,1275"/> | ||
| <area shape="rect" id="node60" href="mathcomp.analysis.lebesgue_stieltjes_measure.html" title="lebesgue_stieltjes_measure" alt="" coords="833,1395,976,1419"/> | ||
| <area shape="rect" id="node41" href="mathcomp.analysis.ereal.html" title="ereal" alt="" coords="846,1011,882,1035"/> | ||
| <area shape="rect" id="node42" href="mathcomp.analysis.tvs.html" title="tvs" alt="" coords="846,1059,882,1083"/> | ||
| <area shape="rect" id="node61" href="mathcomp.analysis.normedtype.html" title="normedtype" alt="" coords="851,1107,920,1131"/> | ||
| <area shape="rect" id="node43" href="mathcomp.analysis.esum.html" title="esum" alt="" coords="856,1299,892,1323"/> | ||
| <area shape="rect" id="node44" href="mathcomp.analysis.measure.html" title="measure" alt="" coords="847,1347,898,1371"/> | ||
| <area shape="rect" id="node59" href="mathcomp.analysis.lebesgue_measure.html" title="lebesgue_measure" alt="" coords="843,1491,943,1515"/> | ||
| <area shape="rect" id="node51" href="mathcomp.analysis.probability.html" title="probability" alt="" coords="841,1731,905,1755"/> | ||
| <area shape="rect" id="node49" href="mathcomp.analysis.function_spaces.html" title="function_spaces" alt="" coords="702,1011,791,1035"/> | ||
| <area shape="rect" id="node50" href="mathcomp.analysis.homotopy_theory.wedge_sigT.html" title="wedge_sigT" alt="" coords="718,1059,787,1083"/> | ||
| <area shape="rect" id="node53" href="mathcomp.analysis.homotopy_theory.continuous_path.html" title="continuous_path" alt="" coords="712,1107,803,1131"/> | ||
| <area shape="rect" id="node52" href="mathcomp.analysis.hoelder.html" title="hoelder" alt="" coords="745,1731,793,1755"/> | ||
| <area shape="rect" id="node54" href="mathcomp.analysis.homotopy_theory.homotopy.html" title="homotopy" alt="" coords="727,1155,787,1179"/> | ||
| <area shape="rect" id="node55" href="mathcomp.analysis.kernel.html" title="kernel" alt="" coords="850,1587,892,1611"/> | ||
| <area shape="rect" id="node56" href="mathcomp.analysis.landau.html" title="landau" alt="" coords="955,1155,998,1179"/> | ||
| <area shape="rect" id="node57" href="mathcomp.analysis.sequences.html" title="sequences" alt="" coords="896,1203,956,1227"/> | ||
| <area shape="rect" id="node63" href="mathcomp.analysis.numfun.html" title="numfun" alt="" coords="852,1251,900,1275"/> | ||
| <area shape="rect" id="node58" href="mathcomp.analysis.lebesgue_integral.html" title="lebesgue_integral" alt="" coords="839,1539,935,1563"/> | ||
| <area shape="rect" id="node62" href="mathcomp.analysis.showcase.summability.html" title="summability" alt="" coords="835,1155,907,1179"/> | ||
| <area shape="rect" id="node64" href="mathcomp.analysis.separation_axioms.html" title="separation_axioms" alt="" coords="690,963,792,987"/> | ||
| <area shape="rect" id="node66" href="mathcomp.analysis.topology_theory.topology.html" title="topology" alt="" coords="714,915,768,939"/> | ||
| <area shape="rect" id="node68" href="mathcomp.analysis.topology_theory.product_topology.html" title="product_topology" alt="" coords="565,675,661,699"/> | ||
| <area shape="rect" id="node75" href="mathcomp.analysis.topology_theory.order_topology.html" title="order_topology" alt="" coords="550,723,636,747"/> | ||
| <area shape="rect" id="node70" href="mathcomp.analysis.topology_theory.subspace_topology.html" title="subspace_topology" alt="" coords="721,819,825,843"/> | ||
| <area shape="rect" id="node78" href="mathcomp.analysis.topology_theory.sigT_topology.html" title="sigT_topology" alt="" coords="838,867,919,891"/> | ||
| <area shape="rect" id="node79" href="mathcomp.analysis.topology_theory.subtype_topology.html" title="subtype_topology" alt="" coords="692,867,790,891"/> | ||
| <area shape="rect" id="node73" href="mathcomp.analysis.topology_theory.num_topology.html" title="num_topology" alt="" coords="428,771,509,795"/> | ||
| <area shape="rect" id="node74" href="mathcomp.analysis.topology_theory.one_point_compactification.html" title="one_point_compactification" alt="" coords="496,867,644,891"/> | ||
| <area shape="rect" id="node76" href="mathcomp.analysis.topology_theory.weak_topology.html" title="weak_topology" alt="" coords="557,771,642,795"/> | ||
| <area shape="rect" id="node80" href="mathcomp.analysis.topology_theory.supremum_topology.html" title="supremum_topology" alt="" coords="1064,867,1175,891"/> | ||
| </map> |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Oops, something went wrong.