kefir on tutorial - Lean Kernel Arena

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: 3.57 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.85 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.76 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.85 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.31 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.63 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.82 ms · instructions: 2.5 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.31 ms · instructions: 2.5 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.96 ms · instructions: 2.5 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.01 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.42 ms · instructions: 2.4 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.89 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.21 ms · instructions: 2.4 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.70 ms · instructions: 2.4 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.84 ms · instructions: 2.4 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.19 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.41 ms · instructions: 2.4 M · max rss memory: 5.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.94 ms · instructions: 2.5 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.28 ms · instructions: 2.4 M · max rss memory: 5.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.70 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.95 ms · instructions: 2.4 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.86 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.85 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.22 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.66 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.07 ms · instructions: 2.4 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.82 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.01 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.77 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.33 ms · instructions: 2.7 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.36 ms · instructions: 2.9 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.15 ms · instructions: 3.1 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.68 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.62 ms · instructions: 2.5 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.07 ms · instructions: 2.4 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.60 ms · instructions: 2.5 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.89 ms · instructions: 3.0 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.48 ms · instructions: 3.5 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.49 ms · instructions: 3.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.25 ms · instructions: 3.6 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.94 ms · instructions: 3.9 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.29 ms · instructions: 2.9 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.09 ms · instructions: 3.5 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.59 ms · instructions: 3.1 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.73 ms · instructions: 9.2 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.80 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.76 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.00 ms · instructions: 2.4 M · max rss memory: 5.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.24 ms · instructions: 2.4 M · max rss memory: 5.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 40.4 ms · instructions: 2.4 M · max rss memory: 5.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.86 ms · instructions: 2.4 M · max rss memory: 5.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.75 ms · instructions: 2.4 M · max rss memory: 5.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.52 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.71 ms · instructions: 2.4 M · max rss memory: 5.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.93 ms · instructions: 3.5 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.22 ms · instructions: 2.5 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.87 ms · instructions: 2.5 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.50 ms · instructions: 2.8 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.87 ms · instructions: 2.8 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.09 ms · instructions: 2.9 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.51 ms · instructions: 2.4 M · max rss memory: 5.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.06 ms · instructions: 2.5 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.47 ms · instructions: 3.1 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.41 ms · instructions: 3.6 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.46 ms · instructions: 3.3 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.00 ms · instructions: 3.7 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.78 ms · instructions: 4.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.78 ms · instructions: 3.0 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.06 ms · instructions: 3.5 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.92 ms · instructions: 3.1 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.75 ms · instructions: 9.6 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.40 ms · instructions: 2.8 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.42 ms · instructions: 2.6 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.87 ms · instructions: 3.7 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.94 ms · instructions: 4.5 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.81 ms · instructions: 4.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.50 ms · instructions: 4.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.92 ms · instructions: 5.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.46 ms · instructions: 4.9 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.53 ms · instructions: 5.3 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.13 ms · instructions: 6.7 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 5.47 ms · instructions: 14.2 M · max rss memory: 6.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.81 ms · instructions: 3.3 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.11 ms · instructions: 3.7 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.27 ms · instructions: 4.0 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.96 ms · instructions: 4.0 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.54 ms · instructions: 3.3 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.35 ms · instructions: 3.1 M · max rss memory: 5.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.47 ms · instructions: 5.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.50 ms · instructions: 5.2 M · max rss memory: 6.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.78 ms · instructions: 5.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.55 ms · instructions: 5.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.98 ms · instructions: 5.2 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.81 ms · instructions: 5.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.82 ms · instructions: 4.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.95 ms · instructions: 6.8 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.37 ms · instructions: 6.8 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.92 ms · instructions: 5.4 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.72 ms · instructions: 4.2 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.90 ms · instructions: 4.6 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 35.9 ms · instructions: 7.4 M · max rss memory: 6.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.43 ms · instructions: 3.4 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.40 ms · instructions: 4.4 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.05 ms · instructions: 3.6 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.04 ms · instructions: 3.7 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.15 ms · instructions: 3.7 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.90 ms · instructions: 2.5 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.34 ms · instructions: 4.1 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.74 ms · instructions: 4.1 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.59 ms · instructions: 4.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.79 ms · instructions: 4.7 M · max rss memory: 6.5 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.87 ms · instructions: 5.8 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 5.14 ms · instructions: 5.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.00 ms · instructions: 3.6 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.89 ms · instructions: 3.6 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.58 ms · instructions: 3.9 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.37 ms · instructions: 3.4 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.66 ms · instructions: 3.4 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.08 ms · instructions: 3.6 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.97 ms · instructions: 3.6 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.62 ms · instructions: 3.9 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.75 ms · instructions: 5.1 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.64 ms · instructions: 4.9 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.05 ms · instructions: 6.5 M · max rss memory: 6.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.58 ms · instructions: 7.3 M · max rss memory: 6.7 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.23 ms · instructions: 4.1 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.11 ms · instructions: 4.1 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.27 ms · instructions: 4.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.42 ms · instructions: 4.3 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.10 ms · instructions: 4.3 M · max rss memory: 6.3 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.19 ms · instructions: 4.2 M · max rss memory: 6.4 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"accept","code":"checked","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.49 ms · instructions: 2.4 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.91 ms · instructions: 2.4 M · max rss memory: 5.6 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.48 ms · instructions: 2.5 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.86 ms · instructions: 2.5 M · max rss memory: 5.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.00 ms · instructions: 2.4 M · max rss memory: 5.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.56 ms · instructions: 2.5 M · max rss memory: 5.9 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.31 ms · instructions: 2.4 M · max rss memory: 5.0 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.44 ms · instructions: 2.4 M · max rss memory: 4.8 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 3.83 ms · instructions: 2.6 M · max rss memory: 6.1 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}

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: 4.42 ms · instructions: 2.5 M · max rss memory: 6.2 MB · run 2026-11-06 00:56:04 UTC

stdout:

{"protocol":"kefir-result-1","outcome":"reject","code":"checking.failed","specification":"sha256:7f42cc89b7243a63abe901f7f27b063e7e4deb261dc9fa06be28ac10a0a9d800","build":"sha256:3091a6d93a28822901c54a736017002bbf18d865c4dbde21488dba857d779ee2","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"}