the next generation of the in-browser educational proof assistant
run npm install and npm run res:format
+27
-5
+22
-1
package-lock.json
+22
-1
package-lock.json
···
8
8
"name": "holbert-ng",
9
9
"version": "0.0.0",
10
10
"dependencies": {
11
+
"@jmagaram/rescript-seq": "^4.4.1",
11
12
"@rescript/react": "^0.13.1",
12
13
"react": "^19.1.0",
13
14
"react-dom": "^19.1.0",
···
724
725
"url": "https://github.com/sponsors/nzakas"
725
726
}
726
727
},
728
+
"node_modules/@jmagaram/rescript-seq": {
729
+
"version": "4.4.1",
730
+
"resolved": "https://registry.npmjs.org/@jmagaram/rescript-seq/-/rescript-seq-4.4.1.tgz",
731
+
"integrity": "sha512-+OdQX3csszdwMAqiVDiSkqGauq564KaxyvXH21oHPMCwD+Z8VdBxsH9t+XkpQ4wS14YbnEd13R4+Z/fg8pkawQ==",
732
+
"license": "ISC",
733
+
"dependencies": {
734
+
"@rescript/core": "^1.1.0",
735
+
"rescript": "^11.0.1"
736
+
}
737
+
},
727
738
"node_modules/@nodelib/fs.scandir": {
728
739
"version": "2.1.5",
729
740
"resolved": "https://registry.npmjs.org/@nodelib/fs.scandir/-/fs.scandir-2.1.5.tgz",
···
766
777
"version": "1.6.1",
767
778
"resolved": "https://registry.npmjs.org/@rescript/core/-/core-1.6.1.tgz",
768
779
"integrity": "sha512-vyb5k90ck+65Fgui+5vCja/mUfzKaK3kOPT4Z6aAJdHLH1eljEi1zKhXroCiCtpNLSWp8k4ulh1bdB5WS0hvqA==",
769
-
"dev": true,
770
780
"license": "MIT",
771
781
"peerDependencies": {
772
782
"rescript": ">=11.1.0"
···
1335
1345
"integrity": "sha512-AwAfQ2Wa5bCx9WP8nZL2uMZWod7J7/JSplxbTmBQ5ms6QpqNYm672H0Vu9ZVKVngQ+ii4R/byguVEUZQyeg44g==",
1336
1346
"dev": true,
1337
1347
"license": "MIT",
1348
+
"peer": true,
1338
1349
"dependencies": {
1339
1350
"csstype": "^3.0.2"
1340
1351
}
···
1395
1406
"integrity": "sha512-vxXJV1hVFx3IXz/oy2sICsJukaBrtDEQSBiV48/YIV5KWjX1dO+bcIr/kCPrW6weKXvsaGKFNlwH0v2eYdRRbA==",
1396
1407
"dev": true,
1397
1408
"license": "MIT",
1409
+
"peer": true,
1398
1410
"dependencies": {
1399
1411
"@typescript-eslint/scope-manager": "8.34.0",
1400
1412
"@typescript-eslint/types": "8.34.0",
···
1626
1638
"integrity": "sha512-NZyJarBfL7nWwIq+FDL6Zp/yHEhePMNnnJ0y3qfieCrmNvYct8uvtiV41UvlSe6apAfk0fY1FbWx+NwfmpvtTg==",
1627
1639
"dev": true,
1628
1640
"license": "MIT",
1641
+
"peer": true,
1629
1642
"bin": {
1630
1643
"acorn": "bin/acorn"
1631
1644
},
···
2056
2069
"integrity": "sha512-ocgh41VhRlf9+fVpe7QKzwLj9c92fDiqOj8Y3Sd4/ZmVA4Btx4PlUYPq4pp9JDyupkf1upbEXecxL2mwNV7jPQ==",
2057
2070
"dev": true,
2058
2071
"license": "MIT",
2072
+
"peer": true,
2059
2073
"dependencies": {
2060
2074
"@eslint-community/eslint-utils": "^4.2.0",
2061
2075
"@eslint-community/regexpp": "^4.12.1",
···
3098
3112
"resolved": "https://registry.npmjs.org/react/-/react-19.1.0.tgz",
3099
3113
"integrity": "sha512-FS+XFBNvn3GTAWq26joslQgWNoFu08F4kl0J4CgdNKADkdSGXQyTCnKteIAJy96Br6YbpEU1LSzV5dYtjMkMDg==",
3100
3114
"license": "MIT",
3115
+
"peer": true,
3101
3116
"engines": {
3102
3117
"node": ">=0.10.0"
3103
3118
}
···
3107
3122
"resolved": "https://registry.npmjs.org/react-dom/-/react-dom-19.1.0.tgz",
3108
3123
"integrity": "sha512-Xs1hdnE+DyKgeHJeJznQmYMIBG3TKIHJJT95Q58nHLSrElKlGQqDTR2HQ9fx5CN/Gk6Vh/kupBTDLU11/nDk/g==",
3109
3124
"license": "MIT",
3125
+
"peer": true,
3110
3126
"dependencies": {
3111
3127
"scheduler": "^0.26.0"
3112
3128
},
···
3133
3149
"integrity": "sha512-0bGU0bocihjSC6MsE3TMjHjY0EUpchyrREquLS8VsZ3ohSMD+VHUEwimEfB3kpBI1vYkw3UFZ3WD8R28guz/Vw==",
3134
3150
"hasInstallScript": true,
3135
3151
"license": "SEE LICENSE IN LICENSE",
3152
+
"peer": true,
3136
3153
"bin": {
3137
3154
"bsc": "bsc",
3138
3155
"bstracing": "lib/bstracing",
···
3473
3490
"integrity": "sha512-M7BAV6Rlcy5u+m6oPhAPFgJTzAioX/6B0DxyvDlo9l8+T3nLKbrczg2WLUyzd45L8RqfUMyGPzekbMvX2Ldkwg==",
3474
3491
"dev": true,
3475
3492
"license": "MIT",
3493
+
"peer": true,
3476
3494
"engines": {
3477
3495
"node": ">=12"
3478
3496
},
···
3535
3553
"integrity": "sha512-p1diW6TqL9L07nNxvRMM7hMMw4c5XOo/1ibL4aAIGmSAt9slTE1Xgw5KWuof2uTOvCg9BY7ZRi+GaF+7sfgPeQ==",
3536
3554
"dev": true,
3537
3555
"license": "Apache-2.0",
3556
+
"peer": true,
3538
3557
"bin": {
3539
3558
"tsc": "bin/tsc",
3540
3559
"tsserver": "bin/tsserver"
···
3595
3614
"integrity": "sha512-0msEVHJEScQbhkbVTb/4iHZdJ6SXp/AvxL2sjwYQFfBqleHtnCqv1J3sa9zbWz/6kW1m9Tfzn92vW+kZ1WV6QA==",
3596
3615
"dev": true,
3597
3616
"license": "MIT",
3617
+
"peer": true,
3598
3618
"dependencies": {
3599
3619
"esbuild": "^0.25.0",
3600
3620
"fdir": "^6.4.4",
···
3685
3705
"integrity": "sha512-M7BAV6Rlcy5u+m6oPhAPFgJTzAioX/6B0DxyvDlo9l8+T3nLKbrczg2WLUyzd45L8RqfUMyGPzekbMvX2Ldkwg==",
3686
3706
"dev": true,
3687
3707
"license": "MIT",
3708
+
"peer": true,
3688
3709
"engines": {
3689
3710
"node": ">=12"
3690
3711
},
+1
-1
src/Method.res
+1
-1
src/Method.res
+2
-1
src/Rule.res
+2
-1
src/Rule.res
···
6
6
module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
7
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
8
8
let rec substitute = (rule: t, subst: Judgment.subst) => {
9
-
let subst' = subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars)))
9
+
let subst' =
10
+
subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars)))
10
11
{
11
12
vars: rule.vars,
12
13
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
+2
-2
tests/HOTermTest.res
+2
-2
tests/HOTermTest.res
···
313
313
t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)")))
314
314
})
315
315
t->block("tests from induction examples", t => {
316
-
let r = ("((?0 \\0) (?1 \\0))")
317
-
let g = ("(f \\0)")
316
+
let r = "((?0 \\0) (?1 \\0))"
317
+
let g = "(f \\0)"
318
318
// what it's currently doing:
319
319
// 0 := (x. y. f x)
320
320
// 1 := doesn't matter