the next generation of the in-browser educational proof assistant
switch to higher order terms to aid debugging
+50
-26
+43
-19
index.html
+43
-19
index.html
···
261
261
</head>
262
262
<body>
263
263
<hol-comp id="index.html/baz" deps="index.html/myconfig">
264
-
x.y.
264
+
x.y.
265
265
(/\ x y)
266
-
---- AE1
266
+
-------- AE1
267
267
x
268
268
269
-
x.y.
269
+
x.y.
270
270
(/\ x y)
271
-
---- AE2
271
+
-------- AE2
272
272
y
273
273
274
-
x.y.
275
-
x y
274
+
x.y.
275
+
x
276
+
y
276
277
---- AI
277
278
(/\ x y)
278
-
</hol-comp>
279
+
280
+
---- Z
281
+
(Nat 0)
282
+
283
+
n.
284
+
(Nat n)
285
+
------- S
286
+
(Nat (S n))
287
+
288
+
P.n.
289
+
(Nat n)
290
+
(P 0)
291
+
[k. (P k) |- (P (S k))]
292
+
----------------------- ind
293
+
(P n)
294
+
295
+
---- e-z
296
+
(Even 0)
297
+
298
+
n.
299
+
(Even n)
300
+
-------- e-SS
301
+
(Even (S (S n)))
302
+
303
+
P.n.
304
+
(Even n)
305
+
(P 0)
306
+
[k. (P k) |- (P (S (S k)))]
307
+
--------------------------- E-ind
308
+
(P n) </hol-comp>
279
309
<hol-config id="index.html/myconfig">Gentzen</hol-config>
280
310
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz">
281
-
a.b.
282
-
(/\ b a)
283
-
-------- theorem
284
-
(/\ a b)
285
-
x.y. ayx |- have x
286
-
|- by (AE2 y x) {
287
-
|- by (ayx) {} }
288
-
asm |- by (AI x y) {
289
-
|- by (asm) {}
290
-
|- by (AE1 y x) {
291
-
|- by (ayx) {} }
292
-
}
311
+
a.
312
+
(Nat a)
313
+
-------
314
+
(Nat (S (S a)))
315
+
316
+
a. asm |- ?
293
317
</hol-proof>
294
318
<script type="module" src="./src/testcomponent.tsx"></script>
295
319
</body>
+7
-7
src/Scratch.res
+7
-7
src/Scratch.res
···
1
-
module AxiomS = Editable.TextArea(AxiomSet.Make(SExp, SExp, SExpJView))
1
+
module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView))
2
2
module DerivationsOrLemmasView = MethodView.CombineMethodView(
3
-
SExp,
4
-
SExp,
5
-
MethodView.DerivationView(SExp, SExp),
6
-
MethodView.LemmaView(SExp, SExp, SExpJView),
3
+
HOTerm,
4
+
HOTerm,
5
+
MethodView.DerivationView(HOTerm, HOTerm),
6
+
MethodView.LemmaView(HOTerm, HOTerm, HOTermJView),
7
7
)
8
-
module TheoremS = Editable.TextArea(Theorem.Make(SExp, SExp, SExpJView, DerivationsOrLemmasView))
9
-
module ConfS = ConfigBlock.Make(SExp, SExp)
8
+
module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DerivationsOrLemmasView))
9
+
module ConfS = ConfigBlock.Make(HOTerm, HOTerm)