-
Notifications
You must be signed in to change notification settings - Fork 14
/
template.html
69 lines (69 loc) · 3.47 KB
/
template.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="description" content="A list of 100 famous math theorems, some of which have been formalized in the Coq proof assistant. This page keeps track of those.">
<title>Famous theorems proven in Coq</title>
<link rel="stylesheet" href="def.css" type="text/css" media="screen,print">
<script>
var show = function(i){document.getElementById('send'+i).setAttribute('style','block'); return false;};
var _gaq = _gaq || [];
_gaq.push(['_setAccount', 'UA-17038604-1']);
_gaq.push(['_trackPageview']);
(function() {
var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true;
ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js';
var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s);
})();
</script>
</head>
<body>
<div class="middle">
<h1>Formalizing 100 theorems in Coq</h1>
<p>
This is an appendix to Freek
Wiedijk's <a href="http://www.cs.ru.nl/~freek/100/">webpage</a> webpage
on the "top 100" mathematical theorems, to keep track of the statements
of the {{{nb_formalized_in_coq}}} theorems that are formalised in Coq.
</p>
<p>
Drop me or Freek an email or
<a href="https://github.com/coq-community/coq-100-theorems">
make a pull request
</a> if you have updates. Preferably edit
<a href="https://github.com/coq-community/coq-100-theorems/blob/master/statements.yml">this file</a>,
from which this page has been generated.
</p>
<p>
Options:<br>
<label><input type="checkbox" checked="checked" onclick="javascript:toggle(this, 'solved');"> Show theorems that have been formalized in Coq</label><br>
<label><input type="checkbox" checked="checked" onclick="javascript:toggle(this, 'unsolved');"> Show theorems that have not been formalized in Coq</label><br>
<label><input type="checkbox" onclick="javascript:toggle(this, 'existing');"> Show existing formalizations</label><br>
<label><input type="checkbox" onclick="javascript:toggle(this, 'axioms');"> Show axioms used</label><br>
<label><input type="checkbox" onclick="javascript:toggle(this, 'repro');"> Show some reproducibility information</label><br>
</p>
{{{main}}}
</div>
<script>
function sheet(rules, options) {
let style = document.createElement("style");
style.appendChild(document.createTextNode(""));
document.head.appendChild(style);
rules.forEach(r => style.sheet.insertRule(r, 0));
style.sheet.disabled = options?.disabled || false;
return style.sheet;
};
let sheets = {
solved: sheet(['.formalized,.formalized+div{ display:none; }'], { disabled: true }),
unsolved: sheet(['.notformalizedyet,.notformalizedyet+div{ display:none; }'], { disabled: true }),
existing: sheet(['.existing { display:none; }'], { disabled: false }),
axioms: sheet(['.axioms { display:none; }'], { disabled: false }),
repro: sheet(['.repro { display:none; }'], { disabled: false }),
};
function toggle(checkbox, field) {
sheets[field].disabled = checkbox.checked
}
var stats = {};
</script>
</body>
</html>