the next generation of the in-browser educational proof assistant
test for induction principles
+12
-1
+1
-1
index.html
+1
-1
index.html
···
331
331
--------------------------- E-ind
332
332
(P n) </hol-comp>
333
333
<hol-config id="index.html/myconfig">Gentzen</hol-config>
334
-
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz">
334
+
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
335
335
a.
336
336
(Nat a)
337
337
-------
+11
tests/HOTermTest.res
+11
tests/HOTermTest.res
···
312
312
t->Util.testNotUnify(a, b)
313
313
t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)")))
314
314
})
315
+
t->block("tests from induction examples", t => {
316
+
let r = ("((?0 \\0) (?1 \\0))")
317
+
let g = ("(f \\0)")
318
+
// what it's currently doing:
319
+
// 0 := (x. y. f x)
320
+
// 1 := doesn't matter
321
+
// what we want
322
+
// 0 := f
323
+
// 1 := (x. x)
324
+
//t->testUnify(r, g, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. f x)"))->substAdd(1,t->Util.parse("(x. x)")))
325
+
})
315
326
})