Checker "kefir-wasm" on the tests of "tutorial"
Checker: kefir-wasm · Version: e00bbd5 · 📄 Declaration · 🔗 Source
These tests are explained on the 📖 tutorial page.
001_basicDef
Test: tutorial/001_basicDef · Expected: 👍 accept · Size: 367 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 62.1 ms · instructions: 565.6 M · max rss memory: 81.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"367","records":"6","work_charged":"1119236","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61882) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61882) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
002_badDef
Test: tutorial/002_badDef · Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 68.5 ms · instructions: 607.3 M · max rss memory: 82.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"def","location":{"record":"6","declaration":"1"},"accounting":{"input_bytes":"365","records":"6","work_charged":"1118914","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61897) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61897) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
003_arrowType
Test: tutorial/003_arrowType · Expected: 👍 accept · Size: 622 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 59.9 ms · instructions: 567.1 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"622","records":"12","work_charged":"1119635","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61912) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61912) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
004_dependentType
Test: tutorial/004_dependentType · Expected: 👍 accept · Size: 460 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 66.2 ms · instructions: 568.0 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"460","records":"7","work_charged":"1119608","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61927) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61927) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
005_constType
Test: tutorial/005_constType · Expected: 👍 accept · Size: 897 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 63.6 ms · instructions: 572.4 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"897","records":"17","work_charged":"1120154","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61942) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61942) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
006_betaReduction
Test: tutorial/006_betaReduction · Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 59.9 ms · instructions: 581.3 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1363","records":"27","work_charged":"1121740","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61957) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61957) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
007_betaReduction2
Test: tutorial/007_betaReduction2 · Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 67.9 ms · instructions: 579.4 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1434","records":"28","work_charged":"1121889","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61972) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61972) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
008_forallSortWhnf
Test: tutorial/008_forallSortWhnf · Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 64.4 ms · instructions: 584.8 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1201","records":"25","work_charged":"1122425","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:61987) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:61987) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
009_forallSortBad
Test: tutorial/009_forallSortBad · Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 71.0 ms · instructions: 643.0 M · max rss memory: 83.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"26","declaration":"2"},"accounting":{"input_bytes":"1273","records":"26","work_charged":"1122546","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62002) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62002) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
010_nonTypeType
Test: tutorial/010_nonTypeType · Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 62.3 ms · instructions: 597.8 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"21","declaration":"2"},"accounting":{"input_bytes":"1094","records":"21","work_charged":"1120505","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62017) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62017) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
011_nonTypeAxiom
Test: tutorial/011_nonTypeAxiom · Expected: ✋ reject · Size: 1.0 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 68.3 ms · instructions: 605.4 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"axiom","location":{"record":"20","declaration":"2"},"accounting":{"input_bytes":"1043","records":"20","work_charged":"1120454","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62032) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62032) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
012_nonPropThm
Test: tutorial/012_nonPropThm · Expected: ✋ reject · Size: 424 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 66.2 ms · instructions: 583.3 M · max rss memory: 81.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"thm","location":{"record":"7","declaration":"1"},"accounting":{"input_bytes":"424","records":"7","work_charged":"1118975","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62047) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62047) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
013_thmProof
Test: tutorial/013_thmProof · Expected: 👍 accept · Size: 1.3 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 67.1 ms · instructions: 576.8 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1345","records":"26","work_charged":"1120975","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62062) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62062) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
014_selfProof
Test: tutorial/014_selfProof · Expected: ✋ reject · Size: 459 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 72.6 ms · instructions: 614.2 M · max rss memory: 82.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"thm","location":{"record":"8","declaration":"1"},"accounting":{"input_bytes":"459","records":"8","work_charged":"1119373","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62077) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62077) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
015_levelComp1
Test: tutorial/015_levelComp1 · Expected: 👍 accept · Size: 391 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 65.6 ms · instructions: 565.5 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"391","records":"7","work_charged":"1119462","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62092) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62092) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
016_levelComp2
Test: tutorial/016_levelComp2 · Expected: 👍 accept · Size: 409 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 64.1 ms · instructions: 572.9 M · max rss memory: 81.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"409","records":"8","work_charged":"1119498","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62107) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62107) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
017_levelComp3
Test: tutorial/017_levelComp3 · Expected: 👍 accept · Size: 427 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 66.2 ms · instructions: 569.4 M · max rss memory: 80.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"427","records":"9","work_charged":"1119518","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62122) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62122) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
018_levelParams
Test: tutorial/018_levelParams · Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 63.3 ms · instructions: 586.2 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1429","records":"29","work_charged":"1121973","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62137) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62137) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
019_tut06_bad01
Test: tutorial/019_tut06_bad01 · Expected: ✋ reject · Size: 427 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 63.6 ms · instructions: 540.1 M · max rss memory: 80.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"def","location":{"record":"8","declaration":"1"},"accounting":{"input_bytes":"427","records":"8","work_charged":"1118815","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62152) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62152) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
020_levelComp4
Test: tutorial/020_levelComp4 · Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 62.4 ms · instructions: 564.5 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"424","records":"8","work_charged":"1119432","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62167) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62167) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
021_levelComp5
Test: tutorial/021_levelComp5 · Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 72.6 ms · instructions: 564.9 M · max rss memory: 81.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"424","records":"8","work_charged":"1119485","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62182) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62182) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
022_imax1
Test: tutorial/022_imax1 · Expected: 👍 accept · Size: 809 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 65.6 ms · instructions: 574.0 M · max rss memory: 81.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"809","records":"16","work_charged":"1119635","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62197) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62197) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
023_imax2
Test: tutorial/023_imax2 · Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 61.9 ms · instructions: 566.2 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"828","records":"17","work_charged":"1119700","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62212) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62212) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
024_levelMaxComm
Test: tutorial/024_levelMaxComm · Expected: 👍 accept · Size: 524 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 62.5 ms · instructions: 568.5 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"524","records":"12","work_charged":"1120269","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62227) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62227) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
025_levelMaxAssoc
Test: tutorial/025_levelMaxAssoc · Expected: 👍 accept · Size: 623 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 65.8 ms · instructions: 569.6 M · max rss memory: 81.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"623","records":"16","work_charged":"1121032","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62242) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62242) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
026_levelMaxIdem
Test: tutorial/026_levelMaxIdem · Expected: 👍 accept · Size: 447 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 62.6 ms · instructions: 570.9 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"447","records":"9","work_charged":"1119777","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62257) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62257) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
027_levelMaxAbsorb
Test: tutorial/027_levelMaxAbsorb · Expected: 👍 accept · Size: 526 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 60.8 ms · instructions: 579.3 M · max rss memory: 81.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"526","records":"12","work_charged":"1120381","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62272) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62272) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
028_inferVar
Test: tutorial/028_inferVar · Expected: 👍 accept · Size: 713 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 58.3 ms · instructions: 565.4 M · max rss memory: 81.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"713","records":"12","work_charged":"1119629","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62287) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62287) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
029_defEqLambda
Test: tutorial/029_defEqLambda · Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 60.2 ms · instructions: 579.6 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"1391","records":"26","work_charged":"1121001","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62302) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62302) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
030_peano1
Test: tutorial/030_peano1 · Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 67.7 ms · instructions: 585.8 M · max rss memory: 81.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[],"accounting":{"input_bytes":"3692","records":"73","work_charged":"1128991","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62317) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62317) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
031_peano2
Test: tutorial/031_peano2 · Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.5 ms · instructions: 602.8 M · max rss memory: 81.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"8","assumed_axioms":[],"accounting":{"input_bytes":"4566","records":"90","work_charged":"1131377","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62332) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62332) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
032_peano3
Test: tutorial/032_peano3 · Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.9 ms · instructions: 600.7 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"10","assumed_axioms":[],"accounting":{"input_bytes":"5006","records":"98","work_charged":"1134210","peak_live_capacity_bytes":"1163144"},"detail":"not_requested"}
stderr:
(node:62347) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62347) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
033_letType
Test: tutorial/033_letType · Expected: 👍 accept · Size: 489 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 66.7 ms · instructions: 566.7 M · max rss memory: 81.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","assumed_axioms":[],"accounting":{"input_bytes":"489","records":"9","work_charged":"1119319","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62362) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62362) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
034_letTypeDep
Test: tutorial/034_letTypeDep · Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 67.0 ms · instructions: 576.0 M · max rss memory: 81.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[{"declaration":"1","name":[{"string":"aDepProp"}]},{"declaration":"2","name":[{"string":"mkADepProp"}]}],"accounting":{"input_bytes":"1238","records":"26","work_charged":"1121341","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62377) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62377) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
035_letRed
Test: tutorial/035_letRed · Expected: 👍 accept · Size: 627 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 63.4 ms · instructions: 577.8 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[{"declaration":"1","name":[{"string":"aProp"}]}],"accounting":{"input_bytes":"627","records":"12","work_charged":"1119604","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:62392) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62392) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
036_empty
Test: tutorial/036_empty · Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 65.9 ms · instructions: 619.5 M · max rss memory: 82.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1228","records":"20","work_charged":"1121869","peak_live_capacity_bytes":"1207757"},"detail":"not_requested"}
stderr:
(node:62407) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62407) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
037_boolType
Test: tutorial/037_boolType · Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 67.7 ms · instructions: 645.1 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2377","records":"37","work_charged":"1141804","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:62422) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62422) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
038_twoBool
Test: tutorial/038_twoBool · Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 74.4 ms · instructions: 662.5 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4266","records":"65","work_charged":"1150769","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:62437) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62437) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
039_andType
Test: tutorial/039_andType · Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 76.8 ms · instructions: 654.9 M · max rss memory: 82.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3273","records":"57","work_charged":"1141299","peak_live_capacity_bytes":"1244032"},"detail":"not_requested"}
stderr:
(node:62452) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62452) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
040_prodType
Test: tutorial/040_prodType · Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 76.2 ms · instructions: 655.4 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3919","records":"76","work_charged":"1141713","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:62467) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62467) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
041_pprodType
Test: tutorial/041_pprodType · Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 78.0 ms · instructions: 672.6 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3906","records":"75","work_charged":"1162739","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:62482) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62482) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
042_pUnitType
Test: tutorial/042_pUnitType · Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.3 ms · instructions: 643.3 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1843","records":"31","work_charged":"1138685","peak_live_capacity_bytes":"1243875"},"detail":"not_requested"}
stderr:
(node:62497) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62497) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
043_eqType
Test: tutorial/043_eqType · Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 77.4 ms · instructions: 666.6 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3324","records":"62","work_charged":"1147906","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:62512) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62512) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
044_natDef
Test: tutorial/044_natDef · Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 76.9 ms · instructions: 659.6 M · max rss memory: 82.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3392","records":"61","work_charged":"1131893","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:62527) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62527) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
045_rbTreeDef
Test: tutorial/045_rbTreeDef · Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 87.6 ms · instructions: 1.1 G · max rss memory: 104.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"16090","records":"296","work_charged":"1246199","peak_live_capacity_bytes":"1333603"},"detail":"not_requested"}
stderr:
(node:62542) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62542) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
046_inductBadNonSort
Test: tutorial/046_inductBadNonSort · Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 71.7 ms · instructions: 583.2 M · max rss memory: 81.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"20","declaration":"2"},"accounting":{"input_bytes":"1182","records":"20","work_charged":"1120703","peak_live_capacity_bytes":"1171365"},"detail":"not_requested"}
stderr:
(node:62557) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62557) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
047_inductBadNonSort2
Test: tutorial/047_inductBadNonSort2 · Expected: ✋ reject · Size: 598 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 62.1 ms · instructions: 575.6 M · max rss memory: 81.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"8","declaration":"2"},"accounting":{"input_bytes":"598","records":"8","work_charged":"1119329","peak_live_capacity_bytes":"1171106"},"detail":"not_requested"}
stderr:
(node:62572) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62572) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
048_inductLevelParam
Test: tutorial/048_inductLevelParam · Expected: ✋ reject · Size: 515 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 62.1 ms · instructions: 546.6 M · max rss memory: 81.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"7","declaration":"1"},"accounting":{"input_bytes":"515","records":"7","work_charged":"1119076","peak_live_capacity_bytes":"1171357"},"detail":"not_requested"}
stderr:
(node:62587) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62587) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
049_inductTooFewParams
Test: tutorial/049_inductTooFewParams · Expected: ✋ reject · Size: 548 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 56.1 ms · instructions: 546.4 M · max rss memory: 80.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"6","declaration":"1"},"accounting":{"input_bytes":"548","records":"6","work_charged":"1119112","peak_live_capacity_bytes":"1170593"},"detail":"not_requested"}
stderr:
(node:62602) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62602) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
050_inductWrongCtorParams
Test: tutorial/050_inductWrongCtorParams · Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 59.4 ms · instructions: 571.8 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"16","declaration":"2"},"accounting":{"input_bytes":"1182","records":"16","work_charged":"1120032","peak_live_capacity_bytes":"1234401"},"detail":"not_requested"}
stderr:
(node:62617) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62617) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
051_inductWrongCtorResParams
Test: tutorial/051_inductWrongCtorResParams · Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 64.9 ms · instructions: 557.1 M · max rss memory: 80.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"19","declaration":"1"},"accounting":{"input_bytes":"1293","records":"19","work_charged":"1120148","peak_live_capacity_bytes":"1234287"},"detail":"not_requested"}
stderr:
(node:62632) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62632) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
052_inductWrongCtorResLevel
Test: tutorial/052_inductWrongCtorResLevel · Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 85.2 ms · instructions: 551.8 M · max rss memory: 81.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"23","declaration":"1"},"accounting":{"input_bytes":"1411","records":"23","work_charged":"1120397","peak_live_capacity_bytes":"1235891"},"detail":"not_requested"}
stderr:
(node:62647) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62647) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
053_inductInIndex
Test: tutorial/053_inductInIndex · Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 75.3 ms · instructions: 573.0 M · max rss memory: 81.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"14","declaration":"2"},"accounting":{"input_bytes":"1099","records":"14","work_charged":"1119913","peak_live_capacity_bytes":"1234385"},"detail":"not_requested"}
stderr:
(node:62662) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62662) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
054_indNeg
Test: tutorial/054_indNeg · Expected: ✋ reject · Size: 996 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 62.0 ms · instructions: 584.6 M · max rss memory: 81.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"12","declaration":"1"},"accounting":{"input_bytes":"996","records":"12","work_charged":"1119714","peak_live_capacity_bytes":"1233838"},"detail":"not_requested"}
stderr:
(node:62677) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62677) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
055_reduceCtorParam.mk
Test: tutorial/055_reduceCtorParam.mk · Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 76.3 ms · instructions: 677.2 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4179","records":"80","work_charged":"1137996","peak_live_capacity_bytes":"1247223"},"detail":"not_requested"}
stderr:
(node:62692) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62692) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
056_reduceCtorType.mk
Test: tutorial/056_reduceCtorType.mk · Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 67.4 ms · instructions: 590.0 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"26","declaration":"2"},"accounting":{"input_bytes":"1549","records":"26","work_charged":"1122096","peak_live_capacity_bytes":"1235192"},"detail":"not_requested"}
stderr:
(node:62707) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62707) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
057_indNegReducible
Test: tutorial/057_indNegReducible · Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 67.3 ms · instructions: 608.1 M · max rss memory: 81.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","declaration_kind":"inductive","location":{"record":"31","declaration":"3"},"accounting":{"input_bytes":"1918","records":"31","work_charged":"1122048","peak_live_capacity_bytes":"1237182"},"detail":"not_requested"}
stderr:
(node:62722) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62722) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
058_predWithTypeField
Test: tutorial/058_predWithTypeField · Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 73.8 ms · instructions: 646.0 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2023","records":"32","work_charged":"1127079","peak_live_capacity_bytes":"1242656"},"detail":"not_requested"}
stderr:
(node:62737) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62737) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
059_typeWithTypeField
Test: tutorial/059_typeWithTypeField · Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 68.0 ms · instructions: 649.2 M · max rss memory: 82.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2116","records":"36","work_charged":"1127994","peak_live_capacity_bytes":"1243105"},"detail":"not_requested"}
stderr:
(node:62752) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62752) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
060_typeWithTypeFieldPoly
Test: tutorial/060_typeWithTypeFieldPoly · Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 65.0 ms · instructions: 650.2 M · max rss memory: 82.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2190","records":"38","work_charged":"1131470","peak_live_capacity_bytes":"1244205"},"detail":"not_requested"}
stderr:
(node:62767) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62767) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
061_typeWithTooHighTypeField.mk
Test: tutorial/061_typeWithTooHighTypeField.mk · Expected: ✋ reject · Size: 943 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 71.4 ms · instructions: 593.3 M · max rss memory: 81.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"11","declaration":"1"},"accounting":{"input_bytes":"943","records":"11","work_charged":"1119663","peak_live_capacity_bytes":"1233870"},"detail":"not_requested"}
stderr:
(node:62782) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62782) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
062_emptyRec
Test: tutorial/062_emptyRec · Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 78.8 ms · instructions: 624.3 M · max rss memory: 82.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"1269","records":"21","work_charged":"1122274","peak_live_capacity_bytes":"1207757"},"detail":"not_requested"}
stderr:
(node:62797) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62797) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
063_boolRec
Test: tutorial/063_boolRec · Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 82.3 ms · instructions: 651.0 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3092","records":"53","work_charged":"1143564","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:62812) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62812) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
064_twoBoolRec
Test: tutorial/064_twoBoolRec · Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 70.4 ms · instructions: 659.6 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4866","records":"78","work_charged":"1152171","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:62827) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62827) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
065_andRec
Test: tutorial/065_andRec · Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 69.8 ms · instructions: 665.9 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3313","records":"58","work_charged":"1141801","peak_live_capacity_bytes":"1244032"},"detail":"not_requested"}
stderr:
(node:62842) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62842) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
066_prodRec
Test: tutorial/066_prodRec · Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 70.5 ms · instructions: 662.7 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"4111","records":"79","work_charged":"1143312","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:62857) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62857) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
067_pprodRec
Test: tutorial/067_pprodRec · Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 73.3 ms · instructions: 672.2 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"4096","records":"78","work_charged":"1164084","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:62872) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62872) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
068_punitRec
Test: tutorial/068_punitRec · Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 70.3 ms · instructions: 652.9 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2227","records":"39","work_charged":"1139719","peak_live_capacity_bytes":"1243875"},"detail":"not_requested"}
stderr:
(node:62887) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62887) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
069_eqRec
Test: tutorial/069_eqRec · Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 70.2 ms · instructions: 657.8 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3369","records":"63","work_charged":"1148684","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:62902) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62902) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
070_nRec
Test: tutorial/070_nRec · Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 68.4 ms · instructions: 652.6 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3394","records":"61","work_charged":"1132291","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:62917) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62917) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
071_rbTreeRef
Test: tutorial/071_rbTreeRef · Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 84.5 ms · instructions: 1.0 G · max rss memory: 103.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"16556","records":"303","work_charged":"1250318","peak_live_capacity_bytes":"1333603"},"detail":"not_requested"}
stderr:
(node:62932) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62932) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
072_boolPropRec
Test: tutorial/072_boolPropRec · Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 69.0 ms · instructions: 634.1 M · max rss memory: 82.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"2313","records":"34","work_charged":"1126107","peak_live_capacity_bytes":"1277798"},"detail":"not_requested"}
stderr:
(node:62947) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62947) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
073_BogusRecursor
Test: tutorial/073_BogusRecursor · Expected: ✋ reject · Size: 1.8 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 64.9 ms · instructions: 623.6 M · max rss memory: 81.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"24","declaration":"2"},"accounting":{"input_bytes":"1710","records":"24","work_charged":"1129180","peak_live_capacity_bytes":"1235927"},"detail":"not_requested"}
stderr:
(node:62962) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62962) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
074_existsRec
Test: tutorial/074_existsRec · Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 70.8 ms · instructions: 661.1 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3665","records":"66","work_charged":"1144906","peak_live_capacity_bytes":"1246310"},"detail":"not_requested"}
stderr:
(node:62977) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62977) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
075_typeSingletonRecReduction
Test: tutorial/075_typeSingletonRecReduction · Expected: 👍 accept · Size: 7.9 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 72.6 ms · instructions: 752.7 M · max rss memory: 87.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"5","assumed_axioms":[],"accounting":{"input_bytes":"8095","records":"138","work_charged":"1180820","peak_live_capacity_bytes":"1286075"},"detail":"not_requested"}
stderr:
(node:62992) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:62992) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
076_sortElimPropRec
Test: tutorial/076_sortElimPropRec · Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 77.3 ms · instructions: 736.3 M · max rss memory: 85.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5773","records":"97","work_charged":"1161322","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:63007) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63007) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
077_sortElimProp2Rec
Test: tutorial/077_sortElimProp2Rec · Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 74.9 ms · instructions: 738.0 M · max rss memory: 85.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"6794","records":"114","work_charged":"1164138","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:63022) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63022) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
078_boolRecEqns
Test: tutorial/078_boolRecEqns · Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 90.0 ms · instructions: 928.5 M · max rss memory: 91.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"11058","records":"199","work_charged":"1197891","peak_live_capacity_bytes":"1285917"},"detail":"not_requested"}
stderr:
(node:63037) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63037) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
079_prodRecEqns
Test: tutorial/079_prodRecEqns · Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 89.4 ms · instructions: 923.8 M · max rss memory: 92.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"10305","records":"205","work_charged":"1179313","peak_live_capacity_bytes":"1252147"},"detail":"not_requested"}
stderr:
(node:63052) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63052) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
080_nRecReduction
Test: tutorial/080_nRecReduction · Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 84.0 ms · instructions: 926.3 M · max rss memory: 93.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"13051","records":"238","work_charged":"1188885","peak_live_capacity_bytes":"1286301"},"detail":"not_requested"}
stderr:
(node:63067) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63067) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
081_listRecReduction
Test: tutorial/081_listRecReduction · Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 89.2 ms · instructions: 1.1 G · max rss memory: 108.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[],"accounting":{"input_bytes":"17898","records":"335","work_charged":"1220536","peak_live_capacity_bytes":"1280428"},"detail":"not_requested"}
stderr:
(node:63082) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63082) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
082_RBTree.id_spec
Test: tutorial/082_RBTree.id_spec · Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 83.7 ms · instructions: 1.2 G · max rss memory: 106.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[],"accounting":{"input_bytes":"49017","records":"1006","work_charged":"1336451","peak_live_capacity_bytes":"1687347"},"detail":"not_requested"}
stderr:
(node:63097) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63097) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
083_And.right
Test: tutorial/083_And.right · Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 73.7 ms · instructions: 671.1 M · max rss memory: 82.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4353","records":"74","work_charged":"1145194","peak_live_capacity_bytes":"1244032"},"detail":"not_requested"}
stderr:
(node:63112) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63112) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
084_Prod.snd
Test: tutorial/084_Prod.snd · Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 72.3 ms · instructions: 657.4 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4646","records":"83","work_charged":"1143370","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:63127) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63127) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
085_PProd.snd
Test: tutorial/085_PProd.snd · Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 69.1 ms · instructions: 670.8 M · max rss memory: 82.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4650","records":"83","work_charged":"1164154","peak_live_capacity_bytes":"1247243"},"detail":"not_requested"}
stderr:
(node:63142) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63142) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
086_PSigma.snd
Test: tutorial/086_PSigma.snd · Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.5 ms · instructions: 668.8 M · max rss memory: 83.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5177","records":"96","work_charged":"1156068","peak_live_capacity_bytes":"1248655"},"detail":"not_requested"}
stderr:
(node:63157) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63157) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
087_projOutOfRange
Test: tutorial/087_projOutOfRange · Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 83.4 ms · instructions: 686.7 M · max rss memory: 83.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"67","declaration":"2"},"accounting":{"input_bytes":"3875","records":"67","work_charged":"1142905","peak_live_capacity_bytes":"1244032"},"detail":"not_requested"}
stderr:
(node:63172) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63172) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
088_projNotStruct
Test: tutorial/088_projNotStruct · Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 74.7 ms · instructions: 669.6 M · max rss memory: 83.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"64","declaration":"2"},"accounting":{"input_bytes":"3557","records":"64","work_charged":"1131968","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:63187) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63187) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
089_projProp1
Test: tutorial/089_projProp1 · Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 93.6 ms · instructions: 924.2 M · max rss memory: 91.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"8390","records":"143","work_charged":"1191479","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63202) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63202) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
090_projProp2
Test: tutorial/090_projProp2 · Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 86.9 ms · instructions: 943.3 M · max rss memory: 95.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"def","location":{"record":"143","declaration":"4"},"accounting":{"input_bytes":"8390","records":"143","work_charged":"1191983","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63217) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63217) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
091_projProp3
Test: tutorial/091_projProp3 · Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 86.7 ms · instructions: 949.6 M · max rss memory: 98.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"8390","records":"143","work_charged":"1192528","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63232) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63232) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
092_projProp4
Test: tutorial/092_projProp4 · Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 89.7 ms · instructions: 937.2 M · max rss memory: 95.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"def","location":{"record":"143","declaration":"4"},"accounting":{"input_bytes":"8390","records":"143","work_charged":"1192024","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63247) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63247) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
093_projProp5
Test: tutorial/093_projProp5 · Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 88.0 ms · instructions: 950.1 M · max rss memory: 100.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"def","location":{"record":"148","declaration":"4"},"accounting":{"input_bytes":"8596","records":"148","work_charged":"1192542","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63262) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63262) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
094_projProp6
Test: tutorial/094_projProp6 · Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 93.2 ms · instructions: 936.8 M · max rss memory: 95.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"def","location":{"record":"143","declaration":"4"},"accounting":{"input_bytes":"8390","records":"143","work_charged":"1191978","peak_live_capacity_bytes":"1253827"},"detail":"not_requested"}
stderr:
(node:63277) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63277) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
095_projDataIndexRec
Test: tutorial/095_projDataIndexRec · Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 81.4 ms · instructions: 732.1 M · max rss memory: 85.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"6921","records":"111","work_charged":"1157561","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:63292) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63292) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
096_projIndexData
Test: tutorial/096_projIndexData · Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 88.0 ms · instructions: 991.4 M · max rss memory: 97.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","declaration_kind":"def","location":{"record":"226","declaration":"7"},"accounting":{"input_bytes":"14395","records":"226","work_charged":"1226512","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:63307) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63307) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
097_projIndexData2
Test: tutorial/097_projIndexData2 · Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 87.0 ms · instructions: 992.1 M · max rss memory: 101.0 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","declaration_kind":"def","location":{"record":"226","declaration":"7"},"accounting":{"input_bytes":"14397","records":"226","work_charged":"1226430","peak_live_capacity_bytes":"1279495"},"detail":"not_requested"}
stderr:
(node:63322) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63322) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
098_projRed
Test: tutorial/098_projRed · Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 89.7 ms · instructions: 929.5 M · max rss memory: 91.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"10151","records":"177","work_charged":"1197591","peak_live_capacity_bytes":"1286535"},"detail":"not_requested"}
stderr:
(node:63337) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63337) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
099_ruleK
Test: tutorial/099_ruleK · Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 77.9 ms · instructions: 667.2 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"6624","records":"121","work_charged":"1171460","peak_live_capacity_bytes":"1286535"},"detail":"not_requested"}
stderr:
(node:63352) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63352) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
100_ruleKbad
Test: tutorial/100_ruleKbad · Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 75.0 ms · instructions: 717.3 M · max rss memory: 83.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","declaration_kind":"thm","location":{"record":"121","declaration":"3"},"accounting":{"input_bytes":"6628","records":"121","work_charged":"1182506","peak_live_capacity_bytes":"1286535"},"detail":"not_requested"}
stderr:
(node:63367) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63367) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
101_ruleKAcc
Test: tutorial/101_ruleKAcc · Expected: ✋ reject · Size: 12.5 KB · Lines: 229 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 93.7 ms · instructions: 1.2 G · max rss memory: 106.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"thm","location":{"record":"229","declaration":"4"},"accounting":{"input_bytes":"12750","records":"229","work_charged":"1244110","peak_live_capacity_bytes":"1295723"},"detail":"not_requested"}
stderr:
(node:63382) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63382) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
102_aNatLit
Test: tutorial/102_aNatLit · Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.4 ms · instructions: 661.3 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"3101","records":"54","work_charged":"1151126","peak_live_capacity_bytes":"1278534"},"detail":"not_requested"}
stderr:
(node:63397) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63397) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
103_natLitEq
Test: tutorial/103_natLitEq · Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 73.6 ms · instructions: 739.5 M · max rss memory: 85.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"6274","records":"114","work_charged":"1180703","peak_live_capacity_bytes":"1286279"},"detail":"not_requested"}
stderr:
(node:63412) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63412) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
104_proofIrrelevance
Test: tutorial/104_proofIrrelevance · Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 72.3 ms · instructions: 659.5 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5154","records":"100","work_charged":"1153432","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63427) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63427) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
105_proofIrrelevanceBad
Test: tutorial/105_proofIrrelevanceBad · Expected: ✋ reject · Size: 4.7 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 81.4 ms · instructions: 708.4 M · max rss memory: 83.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","declaration_kind":"def","location":{"record":"93","declaration":"3"},"accounting":{"input_bytes":"4851","records":"93","work_charged":"1155008","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63442) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63442) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
106_proofIrrelevanceWhnf
Test: tutorial/106_proofIrrelevanceWhnf · Expected: 👍 accept · Size: 5.6 KB · Lines: 112 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 71.4 ms · instructions: 659.7 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"5757","records":"112","work_charged":"1156038","peak_live_capacity_bytes":"1247032"},"detail":"not_requested"}
stderr:
(node:63457) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63457) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
107_proofIrrelevanceUnderBinder
Test: tutorial/107_proofIrrelevanceUnderBinder · Expected: 👍 accept · Size: 1.9 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 62.1 ms · instructions: 592.0 M · max rss memory: 81.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[{"declaration":"1","name":[{"string":"aType"}]},{"declaration":"2","name":[{"string":"aProp"}]},{"declaration":"3","name":[{"string":"aPropFamily"}]},{"declaration":"4","name":[{"string":"anElem"}]},{"declaration":"5","name":[{"string":"anotherElem"}]},{"declaration":"6","name":[{"string":"aPropFamilyProof"}]}],"accounting":{"input_bytes":"1918","records":"39","work_charged":"1124691","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:63472) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63472) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
108_unitEta1
Test: tutorial/108_unitEta1 · Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 77.0 ms · instructions: 666.5 M · max rss memory: 82.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"5","assumed_axioms":[],"accounting":{"input_bytes":"6395","records":"116","work_charged":"1173487","peak_live_capacity_bytes":"1249635"},"detail":"not_requested"}
stderr:
(node:63487) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63487) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
109_unitEta2
Test: tutorial/109_unitEta2 · Expected: 👍 accept · Size: 5.9 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 80.6 ms · instructions: 667.7 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"6092","records":"109","work_charged":"1171314","peak_live_capacity_bytes":"1248547"},"detail":"not_requested"}
stderr:
(node:63502) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63502) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
110_unitEta3
Test: tutorial/110_unitEta3 · Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 76.0 ms · instructions: 663.5 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"6173","records":"111","work_charged":"1171137","peak_live_capacity_bytes":"1248547"},"detail":"not_requested"}
stderr:
(node:63517) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63517) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
111_indexedUnitEta
Test: tutorial/111_indexedUnitEta · Expected: ✋ reject · Size: 7.2 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 90.4 ms · instructions: 797.9 M · max rss memory: 89.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"def","location":{"record":"121","declaration":"4"},"accounting":{"input_bytes":"7372","records":"121","work_charged":"1181405","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:63532) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63532) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
112_structEta
Test: tutorial/112_structEta · Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 90.9 ms · instructions: 928.4 M · max rss memory: 92.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[],"accounting":{"input_bytes":"12836","records":"230","work_charged":"1200511","peak_live_capacity_bytes":"1255891"},"detail":"not_requested"}
stderr:
(node:63547) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63547) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
113_indexedStructEta
Test: tutorial/113_indexedStructEta · Expected: ✋ reject · Size: 8.5 KB · Lines: 138 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 79.5 ms · instructions: 802.4 M · max rss memory: 89.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","declaration_kind":"def","location":{"record":"138","declaration":"5"},"accounting":{"input_bytes":"8713","records":"138","work_charged":"1198559","peak_live_capacity_bytes":"1278087"},"detail":"not_requested"}
stderr:
(node:63562) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63562) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
114_funEta
Test: tutorial/114_funEta · Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 79.2 ms · instructions: 665.0 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5335","records":"104","work_charged":"1153165","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63577) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63577) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
115_funEtaDep
Test: tutorial/115_funEtaDep · Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 73.0 ms · instructions: 664.9 M · max rss memory: 82.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5443","records":"106","work_charged":"1153394","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63592) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63592) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
116_funEtaBad
Test: tutorial/116_funEtaBad · Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 80.4 ms · instructions: 705.2 M · max rss memory: 83.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"thm","location":{"record":"97","declaration":"2"},"accounting":{"input_bytes":"4979","records":"97","work_charged":"1161632","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63607) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63607) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
117_reflOccLeft
Test: tutorial/117_reflOccLeft · Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 70.1 ms · instructions: 655.0 M · max rss memory: 82.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"61","declaration":"2"},"accounting":{"input_bytes":"3826","records":"61","work_charged":"1151597","peak_live_capacity_bytes":"1278534"},"detail":"not_requested"}
stderr:
(node:63622) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63622) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
118_reflOccInIndex
Test: tutorial/118_reflOccInIndex · Expected: ✋ reject · Size: 3.9 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 81.3 ms · instructions: 653.5 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"66","declaration":"2"},"accounting":{"input_bytes":"4044","records":"66","work_charged":"1152161","peak_live_capacity_bytes":"1278534"},"detail":"not_requested"}
stderr:
(node:63637) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63637) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
119_reduceCtorParamRefl.mk
Test: tutorial/119_reduceCtorParamRefl.mk · Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 89.6 ms · instructions: 674.8 M · max rss memory: 82.7 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4642","records":"88","work_charged":"1143633","peak_live_capacity_bytes":"1246966"},"detail":"not_requested"}
stderr:
(node:63652) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63652) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
120_reduceCtorParamRefl2.mk
Test: tutorial/120_reduceCtorParamRefl2.mk · Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 84.6 ms · instructions: 673.8 M · max rss memory: 82.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"4642","records":"88","work_charged":"1143743","peak_live_capacity_bytes":"1246966"},"detail":"not_requested"}
stderr:
(node:63667) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63667) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
121_rTreeRec
Test: tutorial/121_rTreeRec · Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 88.4 ms · instructions: 729.6 M · max rss memory: 85.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","assumed_axioms":[],"accounting":{"input_bytes":"5639","records":"91","work_charged":"1159525","peak_live_capacity_bytes":"1284267"},"detail":"not_requested"}
stderr:
(node:63682) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63682) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
122_rtreeRecReduction
Test: tutorial/122_rtreeRecReduction · Expected: 👍 accept · Size: 10.7 KB · Lines: 191 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 102 ms · instructions: 931.1 M · max rss memory: 92.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"10986","records":"191","work_charged":"1191759","peak_live_capacity_bytes":"1284267"},"detail":"not_requested"}
stderr:
(node:63697) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63697) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
123_accRecType
Test: tutorial/123_accRecType · Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 91.7 ms · instructions: 939.6 M · max rss memory: 93.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","assumed_axioms":[],"accounting":{"input_bytes":"7649","records":"151","work_charged":"1173881","peak_live_capacity_bytes":"1247815"},"detail":"not_requested"}
stderr:
(node:63712) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63712) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
124_accRecReduction
Test: tutorial/124_accRecReduction · Expected: 👍 accept · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 86.2 ms · instructions: 976.1 M · max rss memory: 96.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"4","assumed_axioms":[],"accounting":{"input_bytes":"13363","records":"243","work_charged":"1221971","peak_live_capacity_bytes":"1295723"},"detail":"not_requested"}
stderr:
(node:63727) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63727) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
125_accRecNoEta
Test: tutorial/125_accRecNoEta · Expected: ✋ reject · Size: 12.7 KB · Lines: 235 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 93.8 ms · instructions: 1.2 G · max rss memory: 106.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"3","declaration_kind":"thm","location":{"record":"235","declaration":"4"},"accounting":{"input_bytes":"12978","records":"235","work_charged":"1242612","peak_live_capacity_bytes":"1295723"},"detail":"not_requested"}
stderr:
(node:63742) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63742) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
126_quotMkType
Test: tutorial/126_quotMkType · Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 83.5 ms · instructions: 781.5 M · max rss memory: 87.5 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"6450","records":"123","work_charged":"1166926","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63757) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63757) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
127_quotIndType
Test: tutorial/127_quotIndType · Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 88.8 ms · instructions: 773.5 M · max rss memory: 87.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"6490","records":"124","work_charged":"1167524","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63772) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63772) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
128_quotLiftType
Test: tutorial/128_quotLiftType · Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 91.8 ms · instructions: 835.1 M · max rss memory: 89.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"6496","records":"124","work_charged":"1168002","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63787) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63787) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
129_quotSoundType
Test: tutorial/129_quotSoundType · Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 93.1 ms · instructions: 850.7 M · max rss memory: 89.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"7","assumed_axioms":[{"declaration":"6","name":[{"string":"Quot"},{"string":"sound"}]}],"accounting":{"input_bytes":"7332","records":"141","work_charged":"1170574","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63802) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63802) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
130_quotLiftReduction
Test: tutorial/130_quotLiftReduction · Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 108 ms · instructions: 1.0 G · max rss memory: 94.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"7957","records":"153","work_charged":"1170099","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63817) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63817) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
131_quotIndReduction
Test: tutorial/131_quotIndReduction · Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 117 ms · instructions: 1.0 G · max rss memory: 94.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"6","assumed_axioms":[],"accounting":{"input_bytes":"7817","records":"151","work_charged":"1169534","peak_live_capacity_bytes":"1245669"},"detail":"not_requested"}
stderr:
(node:63832) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63832) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
132_dup_defs
Test: tutorial/132_dup_defs · Expected: ✋ reject · Size: 475 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 69.7 ms · instructions: 577.5 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"7","declaration":"2"},"accounting":{"input_bytes":"475","records":"7","work_charged":"1119353","peak_live_capacity_bytes":"1162864"},"detail":"not_requested"}
stderr:
(node:63847) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63847) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
133_dup_ind_def
Test: tutorial/133_dup_ind_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 66.2 ms · instructions: 586.1 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"27","declaration":"2"},"accounting":{"input_bytes":"1706","records":"27","work_charged":"1121192","peak_live_capacity_bytes":"1243163"},"detail":"not_requested"}
stderr:
(node:63862) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63862) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
134_dup_ctor_def
Test: tutorial/134_dup_ctor_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 76.7 ms · instructions: 586.4 M · max rss memory: 81.2 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"27","declaration":"2"},"accounting":{"input_bytes":"1707","records":"27","work_charged":"1122698","peak_live_capacity_bytes":"1243167"},"detail":"not_requested"}
stderr:
(node:63877) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63877) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
135_dup_rec_def
Test: tutorial/135_dup_rec_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 72.1 ms · instructions: 582.3 M · max rss memory: 81.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"27","declaration":"2"},"accounting":{"input_bytes":"1706","records":"27","work_charged":"1124939","peak_live_capacity_bytes":"1243163"},"detail":"not_requested"}
stderr:
(node:63892) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63892) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
136_misnamed_rec_user
Test: tutorial/136_misnamed_rec_user · Expected: ✋ reject · Size: 2.0 KB · Lines: 33 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 66.4 ms · instructions: 550.1 M · max rss memory: 80.8 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"25","declaration":"1"},"accounting":{"input_bytes":"1588","records":"25","work_charged":"1120807","peak_live_capacity_bytes":"1242607"},"detail":"not_requested"}
stderr:
(node:63907) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63907) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
137_dup_rec_def2
Test: tutorial/137_dup_rec_def2 · Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 61.8 ms · instructions: 583.2 M · max rss memory: 80.9 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"inductive","location":{"record":"28","declaration":"2"},"accounting":{"input_bytes":"1748","records":"28","work_charged":"1125325","peak_live_capacity_bytes":"1243359"},"detail":"not_requested"}
stderr:
(node:63922) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63922) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
138_dup_ctor_rec
Test: tutorial/138_dup_ctor_rec · Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 65.7 ms · instructions: 544.2 M · max rss memory: 81.4 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"24","declaration":"1"},"accounting":{"input_bytes":"1548","records":"24","work_charged":"1120328","peak_live_capacity_bytes":"1242607"},"detail":"not_requested"}
stderr:
(node:63937) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63937) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
139_DupConCon
Test: tutorial/139_DupConCon · Expected: ✋ reject · Size: 2.2 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 62.9 ms · instructions: 549.2 M · max rss memory: 81.1 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"0","declaration_kind":"inductive","location":{"record":"34","declaration":"1"},"accounting":{"input_bytes":"2206","records":"34","work_charged":"1121534","peak_live_capacity_bytes":"1278071"},"detail":"not_requested"}
stderr:
(node:63952) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63952) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
140_falseFromUnsafe
Test: tutorial/140_falseFromUnsafe · Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 75.8 ms · instructions: 658.1 M · max rss memory: 83.3 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"2","declaration_kind":"thm","location":{"record":"22","declaration":"3"},"accounting":{"input_bytes":"1367","records":"22","work_charged":"1128692","peak_live_capacity_bytes":"1207757"},"detail":"not_requested"}
stderr:
(node:63967) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63967) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)
141_falseFromPartial
Test: tutorial/141_falseFromPartial · Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 69.8 ms · instructions: 633.9 M · max rss memory: 82.6 MB · run 2026-11-06 01:01:34 UTC
stdout:
{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:671bc7a685c1af51be4470de0c2c44eddf2923809707b35ad3088ea7b54a1bf9","resource_profile":"sha256:56c449b1a2cdcc498bc0aecf7fbcd221f62f1c314b18adf1438068380b533dcf","checked_declarations":"1","declaration_kind":"def","location":{"record":"20","declaration":"2"},"accounting":{"input_bytes":"1255","records":"20","work_charged":"1128073","peak_live_capacity_bytes":"1207757"},"detail":"not_requested"}
stderr:
(node:63982) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created) (node:63982) ExperimentalWarning: WASI is an experimental feature and might change at any time (Use `node --trace-warnings ...` to show where the warning was created)