Checker "nano-lean" on the tests of "tutorial"
Checker: nano-lean · Version: v0.3.2 (54ce971) · 📄 Declaration · 🔗 Source
These tests are explained on the 📖 tutorial page.
001_basicDef
Test: tutorial/001_basicDef · Expected: 👍 accept · Size: 367 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 6.47 ms · instructions: 2.6 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 410.00µs
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: 5.68 ms · instructions: 2.7 M · max rss memory: 8.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
badDef rejected: declaration type mismatch
stderr:
FAIL 1 declarations, 0 cached, 1 failed in 459.38µs
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: 6.64 ms · instructions: 2.7 M · max rss memory: 11.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 567.61µs
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: 7.84 ms · instructions: 2.7 M · max rss memory: 9.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 592.89µs
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: 6.82 ms · instructions: 2.7 M · max rss memory: 11.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 478.01µs
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: 6.10 ms · instructions: 2.8 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 593.77µs
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: 5.86 ms · instructions: 2.8 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 641.29µs
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: 5.75 ms · instructions: 2.8 M · max rss memory: 12.4 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 480.15µs
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: 4.76 ms · instructions: 2.8 M · max rss memory: 12.3 MB · run 2026-11-06 07:57:01 UTC
stdout:
forallSortBad rejected: expected a sort
stderr:
FAIL 2 declarations, 0 cached, 1 failed in 599.15µs
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: 5.46 ms · instructions: 2.7 M · max rss memory: 12.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
nonTypeType rejected: expected a sort
stderr:
FAIL 2 declarations, 0 cached, 1 failed in 517.95µs
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.43 ms · instructions: 2.7 M · max rss memory: 12.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
nonTypeAxiom rejected: expected a sort
stderr:
FAIL 2 declarations, 0 cached, 1 failed in 430.35µs
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: 4.15 ms · instructions: 2.7 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stdout:
nonPropThm rejected: theorem type is not a proposition
stderr:
FAIL 1 declarations, 0 cached, 1 failed in 519.97µs
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: 5.07 ms · instructions: 2.8 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 552.90µs
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.05 ms · instructions: 2.7 M · max rss memory: 9.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
selfProof rejected: unknown constant selfProof
stderr:
FAIL 1 declarations, 0 cached, 1 failed in 369.66µs
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: 4.14 ms · instructions: 2.7 M · max rss memory: 8.4 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 506.47µs
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: 6.50 ms · instructions: 2.7 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 467.49µs
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: 5.44 ms · instructions: 2.7 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 494.98µs
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: 6.17 ms · instructions: 2.8 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 712.60µs
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: 5.09 ms · instructions: 2.5 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 8: duplicate universe parameter
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: 5.19 ms · instructions: 2.7 M · max rss memory: 8.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 533.12µs
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: 7.38 ms · instructions: 2.7 M · max rss memory: 8.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 386.64µs
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: 6.62 ms · instructions: 2.7 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 516.46µs
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: 6.58 ms · instructions: 2.7 M · max rss memory: 11.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 531.53µs
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: 5.46 ms · instructions: 2.7 M · max rss memory: 10.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 382.43µs
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.50 ms · instructions: 2.7 M · max rss memory: 10.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 369.75µs
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: 5.00 ms · instructions: 2.7 M · max rss memory: 8.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 341.34µs
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: 4.62 ms · instructions: 2.7 M · max rss memory: 10.4 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 311.78µs
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: 4.27 ms · instructions: 2.7 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 406.71µs
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: 4.78 ms · instructions: 2.7 M · max rss memory: 11.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 413.88µs
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: 5.25 ms · instructions: 3.1 M · max rss memory: 17.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 7 declarations, 0 cached, 0 failed in 977.05µs
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: 7.56 ms · instructions: 3.2 M · max rss memory: 17.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.27ms
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: 44.1 ms · instructions: 3.2 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 10 declarations, 0 cached, 0 failed in 1.35ms
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: 5.00 ms · instructions: 2.7 M · max rss memory: 9.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 1 declarations, 0 cached, 0 failed in 457.06µs
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: 6.29 ms · instructions: 2.9 M · max rss memory: 15.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 3 declarations, 0 cached, 0 failed in 837.16µs
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.90 ms · instructions: 2.7 M · max rss memory: 11.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 2 declarations, 0 cached, 0 failed in 455.61µs
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: 4.38 ms · instructions: 2.8 M · max rss memory: 12.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 3 declarations, 0 cached, 0 failed in 413.03µs
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: 4.08 ms · instructions: 2.9 M · max rss memory: 12.4 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 466.03µs
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.81 ms · instructions: 3.0 M · max rss memory: 17.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 882.24µs
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: 5.06 ms · instructions: 2.9 M · max rss memory: 15.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 894.35µs
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: 7.43 ms · instructions: 3.0 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 990.99µs
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: 6.06 ms · instructions: 3.0 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 1.13ms
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: 5.94 ms · instructions: 2.9 M · max rss memory: 11.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 687.75µs
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: 5.25 ms · instructions: 3.0 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 875.81µs
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: 5.04 ms · instructions: 2.9 M · max rss memory: 13.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 622.02µs
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: 7.13 ms · instructions: 3.5 M · max rss memory: 21.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 14 declarations, 0 cached, 0 failed in 1.45ms
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: 5.91 ms · instructions: 2.8 M · max rss memory: 13.9 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductBadNonSort rejected: expected a sort
stderr:
FAIL 2 declarations, 0 cached, 1 failed in 785.80µs
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: 5.09 ms · instructions: 2.7 M · max rss memory: 9.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductBadNonSort2 rejected: inductive type does not end in a sort
stderr:
FAIL 2 declarations, 0 cached, 1 failed in 445.69µs
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.87 ms · instructions: 2.6 M · max rss memory: 8.2 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 7: duplicate universe parameter
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.97 ms · instructions: 2.7 M · max rss memory: 11.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductTooFewParams rejected: missing inductive parameter
stderr:
FAIL 1 declarations, 0 cached, 1 failed in 619.51µs
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: 5.90 ms · instructions: 2.8 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductWrongCtorParams rejected: inductive parameter type mismatch
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 744.66µs
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: 5.66 ms · instructions: 2.8 M · max rss memory: 13.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductWrongCtorResParams rejected: invalid constructor return type
stderr:
FAIL 3 declarations, 0 cached, 1 failed in 675.48µs
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: 5.09 ms · instructions: 2.8 M · max rss memory: 13.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductWrongCtorResLevel rejected: invalid constructor return type
stderr:
FAIL 3 declarations, 0 cached, 1 failed in 658.84µs
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: 5.88 ms · instructions: 2.8 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
inductInIndex rejected: invalid constructor return type
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 610.78µs
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: 6.58 ms · instructions: 2.8 M · max rss memory: 13.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
indNeg rejected: negative inductive occurrence
stderr:
FAIL 3 declarations, 0 cached, 1 failed in 789.45µs
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: 5.68 ms · instructions: 3.0 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 983.23µs
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: 6.20 ms · instructions: 2.9 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
reduceCtorType rejected: incorrect recursor universe parameters
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 896.78µs
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: 7.30 ms · instructions: 2.9 M · max rss memory: 13.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
indNegReducible rejected: negative inductive occurrence
stderr:
FAIL 5 declarations, 0 cached, 1 failed in 719.04µs
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: 5.61 ms · instructions: 2.9 M · max rss memory: 13.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 692.12µs
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: 5.10 ms · instructions: 2.9 M · max rss memory: 13.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 793.39µs
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: 7.18 ms · instructions: 2.9 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 1.02ms
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: 4.36 ms · instructions: 2.8 M · max rss memory: 10.5 MB · run 2026-11-06 07:57:01 UTC
stdout:
typeWithTooHighTypeField rejected: constructor field universe exceeds inductive universe
stderr:
FAIL 3 declarations, 0 cached, 1 failed in 513.82µs
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: 6.80 ms · instructions: 2.8 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 3 declarations, 0 cached, 0 failed in 733.16µs
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: 5.48 ms · instructions: 2.9 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 772.31µs
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: 6.52 ms · instructions: 3.1 M · max rss memory: 19.4 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.18ms
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: 29.7 ms · instructions: 3.0 M · max rss memory: 17.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 1.12ms
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: 7.08 ms · instructions: 3.1 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 976.43µs
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: 6.04 ms · instructions: 3.0 M · max rss memory: 15.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 841.88µs
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: 6.25 ms · instructions: 2.9 M · max rss memory: 16.0 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 1.01ms
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: 5.90 ms · instructions: 3.0 M · max rss memory: 13.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 883.50µs
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: 5.97 ms · instructions: 3.0 M · max rss memory: 13.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 950.61µs
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: 8.78 ms · instructions: 3.7 M · max rss memory: 24.1 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 14 declarations, 0 cached, 0 failed in 1.73ms
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: 7.47 ms · instructions: 2.9 M · max rss memory: 13.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 928.02µs
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: 7.07 ms · instructions: 2.9 M · max rss memory: 13.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
BogusRecursor rejected: incorrect recursor universe parameters
stderr:
FAIL 6 declarations, 0 cached, 1 failed in 798.25µs
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: 5.81 ms · instructions: 3.0 M · max rss memory: 15.5 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 861.12µs
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: 7.14 ms · instructions: 3.4 M · max rss memory: 23.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 12 declarations, 0 cached, 0 failed in 1.80ms
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: 6.32 ms · instructions: 3.1 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.10ms
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: 8.38 ms · instructions: 3.2 M · max rss memory: 19.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 9 declarations, 0 cached, 0 failed in 1.14ms
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: 8.73 ms · instructions: 3.5 M · max rss memory: 21.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 11 declarations, 0 cached, 0 failed in 1.12ms
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: 5.67 ms · instructions: 3.3 M · max rss memory: 22.1 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 7 declarations, 0 cached, 0 failed in 970.72µs
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: 6.45 ms · instructions: 3.6 M · max rss memory: 20.1 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 13 declarations, 0 cached, 0 failed in 1.38ms
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: 7.79 ms · instructions: 3.8 M · max rss memory: 23.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 14 declarations, 0 cached, 0 failed in 1.31ms
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: 7.03 ms · instructions: 5.1 M · max rss memory: 27.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 19 declarations, 0 cached, 0 failed in 1.65ms
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: 6.29 ms · instructions: 3.1 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.05ms
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: 8.26 ms · instructions: 3.1 M · max rss memory: 17.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.41ms
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: 7.73 ms · instructions: 3.1 M · max rss memory: 18.0 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.54ms
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: 8.62 ms · instructions: 3.1 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.10ms
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: 6.81 ms · instructions: 3.0 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
projOutOfRange rejected: invalid projection
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 1.07ms
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: 6.79 ms · instructions: 2.9 M · max rss memory: 15.9 MB · run 2026-11-06 07:57:01 UTC
stdout:
projNotStruct rejected: projection of a non-structure
stderr:
FAIL 5 declarations, 0 cached, 1 failed in 771.30µs
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: 6.46 ms · instructions: 3.3 M · max rss memory: 17.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 10 declarations, 0 cached, 0 failed in 1.08ms
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: 8.34 ms · instructions: 3.2 M · max rss memory: 17.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
projProp2 rejected: invalid projection
stderr:
FAIL 10 declarations, 0 cached, 1 failed in 1.30ms
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: 8.78 ms · instructions: 3.3 M · max rss memory: 19.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 10 declarations, 0 cached, 0 failed in 1.24ms
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: 7.05 ms · instructions: 3.3 M · max rss memory: 20.1 MB · run 2026-11-06 07:57:01 UTC
stdout:
projProp4 rejected: invalid projection
stderr:
FAIL 10 declarations, 0 cached, 1 failed in 1.15ms
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: 7.23 ms · instructions: 3.3 M · max rss memory: 20.0 MB · run 2026-11-06 07:57:01 UTC
stdout:
projProp5 rejected: invalid projection
stderr:
FAIL 10 declarations, 0 cached, 1 failed in 1.70ms
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: 6.83 ms · instructions: 3.3 M · max rss memory: 18.1 MB · run 2026-11-06 07:57:01 UTC
stdout:
projProp6 rejected: invalid projection
stderr:
FAIL 10 declarations, 0 cached, 1 failed in 1.28ms
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: 7.09 ms · instructions: 3.3 M · max rss memory: 20.0 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 11 declarations, 0 cached, 0 failed in 1.34ms
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: 6.07 ms · instructions: 3.6 M · max rss memory: 21.9 MB · run 2026-11-06 07:57:01 UTC
stdout:
projIndexData rejected: projection type mismatch
stderr:
FAIL 20 declarations, 0 cached, 1 failed in 1.13ms
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: 6.68 ms · instructions: 3.6 M · max rss memory: 21.7 MB · run 2026-11-06 07:57:01 UTC
stdout:
projIndexData2 rejected: projection type mismatch
stderr:
FAIL 20 declarations, 0 cached, 1 failed in 935.80µs
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: 7.91 ms · instructions: 3.5 M · max rss memory: 25.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 13 declarations, 0 cached, 0 failed in 1.68ms
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: 6.78 ms · instructions: 3.2 M · max rss memory: 17.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.07ms
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: 6.73 ms · instructions: 3.2 M · max rss memory: 17.9 MB · run 2026-11-06 07:57:01 UTC
stdout:
ruleKbad rejected: declaration type mismatch
stderr:
FAIL 8 declarations, 0 cached, 1 failed in 1.11ms
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: 7.04 ms · instructions: 3.6 M · max rss memory: 22.0 MB · run 2026-11-06 07:57:01 UTC
stdout:
ruleKAcc rejected: declaration type mismatch
stderr:
FAIL 11 declarations, 0 cached, 1 failed in 1.75ms
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: 6.41 ms · instructions: 2.9 M · max rss memory: 16.0 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 885.83µs
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: 7.08 ms · instructions: 3.2 M · max rss memory: 19.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.32ms
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: 6.03 ms · instructions: 3.1 M · max rss memory: 17.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.14ms
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: 5.41 ms · instructions: 3.0 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
proofIrrelevanceBad rejected: declaration type mismatch
stderr:
FAIL 5 declarations, 0 cached, 1 failed in 1.17ms
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: 6.98 ms · instructions: 3.1 M · max rss memory: 17.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 6 declarations, 0 cached, 0 failed in 1.20ms
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: 6.19 ms · instructions: 2.9 M · max rss memory: 13.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 7 declarations, 0 cached, 0 failed in 773.71µs
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: 6.55 ms · instructions: 3.3 M · max rss memory: 21.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 9 declarations, 0 cached, 0 failed in 1.42ms
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: 7.26 ms · instructions: 3.2 M · max rss memory: 21.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.79ms
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: 7.23 ms · instructions: 3.2 M · max rss memory: 19.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.40ms
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: 7.41 ms · instructions: 3.3 M · max rss memory: 20.3 MB · run 2026-11-06 07:57:01 UTC
stdout:
indexedUnitEta rejected: declaration type mismatch
stderr:
FAIL 11 declarations, 0 cached, 1 failed in 1.65ms
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: 6.37 ms · instructions: 3.6 M · max rss memory: 21.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 13 declarations, 0 cached, 0 failed in 1.49ms
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: 7.63 ms · instructions: 3.4 M · max rss memory: 20.0 MB · run 2026-11-06 07:57:01 UTC
stdout:
indexedStructEta rejected: declaration type mismatch
stderr:
FAIL 14 declarations, 0 cached, 1 failed in 1.60ms
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: 7.31 ms · instructions: 3.1 M · max rss memory: 18.1 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.17ms
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: 7.77 ms · instructions: 3.1 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.50ms
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: 6.48 ms · instructions: 3.1 M · max rss memory: 18.0 MB · run 2026-11-06 07:57:01 UTC
stdout:
funEtaBad rejected: declaration type mismatch
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 1.06ms
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: 7.40 ms · instructions: 3.0 M · max rss memory: 19.9 MB · run 2026-11-06 07:57:01 UTC
stdout:
reflOccLeft rejected: negative inductive occurrence
stderr:
FAIL 7 declarations, 0 cached, 1 failed in 1.21ms
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: 6.13 ms · instructions: 3.0 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
reflOccInIndex rejected: application type mismatch
stderr:
FAIL 7 declarations, 0 cached, 1 failed in 919.14µs
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: 6.80 ms · instructions: 3.0 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 1.07ms
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: 5.84 ms · instructions: 3.0 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 5 declarations, 0 cached, 0 failed in 966.27µs
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: 5.70 ms · instructions: 3.2 M · max rss memory: 19.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 9 declarations, 0 cached, 0 failed in 1.35ms
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: 7.30 ms · instructions: 3.5 M · max rss memory: 25.9 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 14 declarations, 0 cached, 0 failed in 1.86ms
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: 5.86 ms · instructions: 3.2 M · max rss memory: 17.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 4 declarations, 0 cached, 0 failed in 1.13ms
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: 7.09 ms · instructions: 3.7 M · max rss memory: 22.3 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 11 declarations, 0 cached, 0 failed in 1.55ms
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: 39.2 ms · instructions: 3.6 M · max rss memory: 20.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
accRecNoEta rejected: declaration type mismatch
stderr:
FAIL 11 declarations, 0 cached, 1 failed in 1.56ms
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: 7.93 ms · instructions: 3.7 M · max rss memory: 17.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.46ms
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: 7.03 ms · instructions: 3.7 M · max rss memory: 15.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.05ms
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: 6.22 ms · instructions: 3.7 M · max rss memory: 17.6 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.21ms
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: 6.01 ms · instructions: 3.8 M · max rss memory: 22.1 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 9 declarations, 0 cached, 0 failed in 1.48ms
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: 5.44 ms · instructions: 3.7 M · max rss memory: 17.7 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.05ms
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: 7.20 ms · instructions: 3.7 M · max rss memory: 19.8 MB · run 2026-11-06 07:57:01 UTC
stderr:
ok 8 declarations, 0 cached, 0 failed in 1.28ms
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: 4.13 ms · instructions: 2.5 M · max rss memory: 8.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 7: duplicate declaration dup_defs
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: 6.81 ms · instructions: 2.6 M · max rss memory: 10.5 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 27: duplicate declaration dup_ind_def
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: 6.69 ms · instructions: 2.6 M · max rss memory: 10.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 27: duplicate declaration dup_ctor_def.mk
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: 5.59 ms · instructions: 2.6 M · max rss memory: 10.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 27: duplicate declaration dup_rec_def.rec
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: 7.30 ms · instructions: 2.9 M · max rss memory: 15.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
misnamed_rec rejected: missing recursor
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 838.91µs
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: 6.23 ms · instructions: 2.8 M · max rss memory: 11.8 MB · run 2026-11-06 07:57:01 UTC
stdout:
dup_rec_def2 rejected: missing recursor
stderr:
FAIL 4 declarations, 0 cached, 1 failed in 658.00µs
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: 5.69 ms · instructions: 2.6 M · max rss memory: 10.5 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 24: duplicate declaration dup_ctor_rec.rec
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: 6.22 ms · instructions: 2.6 M · max rss memory: 10.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 34: duplicate declaration dup_ind_con_con.mk
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: 6.05 ms · instructions: 2.6 M · max rss memory: 10.6 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 20: unsafe or partial definition is not permitted in a safe proof export
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: 5.90 ms · instructions: 2.6 M · max rss memory: 10.4 MB · run 2026-11-06 07:57:01 UTC
stdout:
invalid export: line 20: unsafe or partial definition is not permitted in a safe proof export