-
Notifications
You must be signed in to change notification settings - Fork 42
/
index.html
141 lines (126 loc) · 5.57 KB
/
index.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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>jsCoq – Use Coq in Your Browser</title>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<!-- Move to copy with the bundle -->
<link rel="icon" href="frontend/classic/images/favicon.png">
<style>body { visibility: hidden; } /* FOUC avoidance */</style>
<link rel="stylesheet" type="text/css" href="./dist/frontend/index.css">
<link rel="stylesheet" type="text/css" href="./frontend/classic/css/landing-page.css">
<!-- These may be bundled as part of landing-page, but anyway should not be in the main bundle -->
<link rel="stylesheet" type="text/css" href="node_modules/bootstrap/dist/css/bootstrap.min.css">
<script src="node_modules/bootstrap/dist/js/bootstrap.bundle.min.js"></script>
</head>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled split">
<div id="code-wrapper">
<div id="document-wrapper">
<!------------------------------->
<!-- N A V B A R -->
<!------------------------------->
<nav class="navbar sticky-top navbar-expand-lg navbar-light bg-light">
<div class="container-fluid">
<a class="navbar-brand"><img src="frontend/classic/images/favicon.png"></a>
<button class="navbar-toggler" type="button" data-bs-toggle="collapse" data-bs-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarSupportedContent">
<ul class="navbar-nav me-auto mb-2 mb-lg-0">
<li class="nav-item dropdown">
<a class="nav-link dropdown-toggle" id="navbarAbout" role="button" data-bs-toggle="dropdown" aria-expanded="false">
About
</a>
<ul class="dropdown-menu" aria-labelledby="navbarDropdown">
<li><a class="dropdown-item" href="#team">jsCoq Dev Team</a></li>
<li><hr class="dropdown-divider"></li>
<li><a class="dropdown-item" href="https://coq.inria.fr">Coq Proof Assistant</a></li>
<li><a class="dropdown-item" href="https://github.com/cpitclaudel/company-coq">company-coq</a></li>
</ul>
</li>
<li class="nav-item dropdown">
<a class="nav-link dropdown-toggle" id="navbarExamples" role="button" data-bs-toggle="dropdown" aria-expanded="false">
Examples
</a>
<ul class="dropdown-menu" aria-labelledby="navbarDropdown">
<li><a class="dropdown-item" href="examples/inf-primes.html">Infinitude of Primes</a></li>
<li><a class="dropdown-item" href="examples/sqrt_2.html">Irrationality of <span class="math"><img class="symbol-sqrt" src="frontend/classic/images/sqrt.svg">2</span></a></li>
<!-- these are only available from the full website -->
<li><a class="dropdown-item" href="/fun/coqoban.html">🎡 Çoqoban</a></li>
<li><hr class="dropdown-divider"></li>
<li><a class="dropdown-item" href="/ext/sf"><img class="symbol-book" src="frontend/classic/images/book.svg">Software Foundations</a></li>
</ul>
</li>
</ul>
</div>
</div>
<a id="scratchpad" href="examples/scratchpad.html" title="Open scratchpad">
<span class="newcomer scratchpad-tip">open the scratchpad<br/>to start editing</span>
</a>
</nav>
<!------------------------------->
<div id="document">
<div>
<h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
<textarea id="coqCode" class="snippet">
### Welcome to JsCoq
- You can edit this document as you please
- Coq will recognize the code snippets as Coq
- You will be able to save the document and link to other documents soon
```coq
From Coq Require Import List.
Import ListNotations.
```
```coq
Lemma rev_snoc_cons A :
forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
Proof.
induction l.
- reflexivity.
- simpl. rewrite IHl. simpl. reflexivity.
Qed.
```
Try to update _above_ and **below**:
```coq
Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
Proof.
induction l.
- reflexivity.
- simpl. rewrite rev_snoc_cons. rewrite IHl.
reflexivity.
Qed.
```
Please edit your code here!
</textarea>
</div> <!-- /#subdiv -->
</div> <!-- /#document -->
</div> <!-- /#document-wrapper -->
</div> <!-- /#code-wrapper -->
</div> <!-- /#ide-wrapper -->
<script type="module">
import { JsCoq } from './jscoq.js';
var sp = new URLSearchParams(location.search),
ifHas = x => sp.has(x) ? x : undefined;
if (!localStorage['scratchpad.last_filename'])
setTimeout(() => document.body.classList.add('welcome'), 1500);
document.querySelector('#scratchpad').href += location.search;
var jscoq_ids = ['coqCode'];
var jscoq_opts = {
backend: sp.get('backend') ?? ifHas('wa'),
frontend: sp.get('frontend'),
content_type: sp.get('content_type'),
implicit_libs: false,
focus: false,
debug: true,
editor: { mode: { 'company-coq': false } },
init_pkgs: ['init', 'coq-base', 'coq-collections', 'coq-arith'],
all_pkgs: ['coq', 'mathcomp']
};
JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
/* Global reference */
window.coq = res;
});
</script>
</body>
</html>