Checker "pestka-wasm" on the tests of "tutorial"
Checker: pestka-wasm · Version: 7caa557 · 📄 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: 118 ms · instructions: 444.1 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 2, levels 2, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 123 ms · instructions: 446.4 M · max rss memory: 91.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 2, levels 2, expressions 2 rejected: badDef: declaration type mismatch
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: 115 ms · instructions: 449.5 M · max rss memory: 91.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 7, levels 2, expressions 3 checked 1, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 453.2 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 1, expressions 3 checked 1, admitted unchecked 0, skipped 0 accepted
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: 112 ms · instructions: 450.5 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 9, levels 2, expressions 6 checked 1, admitted unchecked 0, skipped 0 accepted
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: 111 ms · instructions: 457.6 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 11, levels 2, expressions 13 checked 2, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 460.9 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 11, levels 2, expressions 14 checked 2, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 456.8 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 7, levels 4, expressions 13 checked 2, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 457.7 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 7, levels 4, expressions 14 rejected: forallSortBad: type expected
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: 112 ms · instructions: 451.0 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 10, levels 2, expressions 8 rejected: nonTypeType: type expected
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: 110 ms · instructions: 453.4 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 10, levels 2, expressions 7 rejected: nonTypeAxiom: type expected
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: 117 ms · instructions: 439.7 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 1, expressions 3 rejected: nonPropThm: theorem type is not Prop
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: 111 ms · instructions: 454.4 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 10, levels 1, expressions 14 checked 2, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 457.5 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 1, expressions 4 rejected: selfProof: unknown constant 'selfProof'
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: 112 ms · instructions: 455.1 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 2, levels 3, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 441.9 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 2, levels 4, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 115 ms · instructions: 440.5 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 2, levels 5, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 464.0 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 12, levels 3, expressions 13 checked 2, admitted unchecked 0, skipped 0 accepted
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: 111 ms · instructions: 432.7 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 3, expressions 2 rejected: tut06_bad01: duplicate universe level 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: 118 ms · instructions: 439.5 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 3, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 440.4 M · max rss memory: 90.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 3, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 452.1 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 8, levels 2, expressions 6 checked 1, admitted unchecked 0, skipped 0 accepted
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: 108 ms · instructions: 451.9 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 8, levels 3, expressions 6 checked 1, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 448.1 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 4, levels 6, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 449.5 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 5, levels 9, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 446.6 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 4, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 446.9 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 4, levels 6, expressions 2 checked 1, admitted unchecked 0, skipped 0 accepted
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: 115 ms · instructions: 449.9 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 4, levels 1, expressions 7 checked 1, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 453.5 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 10, levels 1, expressions 15 checked 1, admitted unchecked 0, skipped 0 accepted
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: 121 ms · instructions: 468.9 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 7, declarations 7, names 21, levels 5, expressions 41 checked 7, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 471.4 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 8, names 23, levels 5, expressions 55 checked 8, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 479.4 M · max rss memory: 92.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 10, names 25, levels 5, expressions 59 checked 10, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 454.1 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 2, expressions 4 checked 1, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 467.5 M · max rss memory: 91.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 3, names 11, levels 2, expressions 11 checked 3, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 460.1 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 4, levels 2, expressions 5 checked 2, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 467.6 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 2, names 7, levels 3, expressions 9 checked 2, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 478.8 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 11, levels 3, expressions 22 checked 2, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 480.4 M · max rss memory: 91.8 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 17, levels 3, expressions 43 checked 3, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 481.5 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 13, levels 2, expressions 41 checked 2, admitted unchecked 0, skipped 0 accepted
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: 115 ms · instructions: 480.9 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 20, levels 8, expressions 47 checked 2, admitted unchecked 0, skipped 0 accepted
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: 115 ms · instructions: 483.7 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 20, levels 7, expressions 47 checked 2, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 476.0 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 10, levels 4, expressions 16 checked 2, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 478.8 M · max rss memory: 91.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 16, levels 3, expressions 42 checked 2, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 487.9 M · max rss memory: 91.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 21, levels 3, expressions 36 checked 2, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 554.4 M · max rss memory: 100.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 14, declarations 4, names 40, levels 5, expressions 248 checked 4, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 464.2 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 10, levels 2, expressions 7 rejected: inductBadNonSort: type expected
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: 112 ms · instructions: 447.0 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 3, levels 2, expressions 2 rejected: inductBadNonSort2: type expected
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: 109 ms · instructions: 435.9 M · max rss memory: 91.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 3, expressions 1 rejected: inductLevelParam: duplicate universe level 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: 108 ms · instructions: 446.0 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 1, declarations 1, names 3, levels 1, expressions 2 rejected: inductTooFewParams: number of parameters mismatch in inductive datatype declaration
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: 112 ms · instructions: 453.6 M · max rss memory: 91.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 6, levels 2, expressions 7 rejected: inductWrongCtorParams: invalid occurrence of a datatype being declared in 'inductWrongCtorParams.mk': it must be applied to the parameters and universe levels of the mutual declaration
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: 113 ms · instructions: 452.9 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 1, names 6, levels 2, expressions 11 rejected: inductWrongCtorResParams: invalid occurrence of a datatype being declared in 'inductWrongCtorResParams.mk': it must be applied to the parameters and universe levels of the mutual declaration
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: 112 ms · instructions: 446.4 M · max rss memory: 91.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 1, names 8, levels 4, expressions 11 rejected: inductWrongCtorResLevel: invalid occurrence of a datatype being declared in 'inductWrongCtorResLevel.mk': it must be applied to the parameters and universe levels of the mutual declaration
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: 114 ms · instructions: 463.3 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 6, levels 1, expressions 6 rejected: inductInIndex: invalid return type for 'inductInIndex.mk'
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: 121 ms · instructions: 455.1 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 1, names 5, levels 2, expressions 5 rejected: indNeg: arg #1 of 'indNeg.mk' has a non positive occurrence of the datatypes being declared
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: 125 ms · instructions: 500.7 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 19, levels 5, expressions 54 checked 3, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 462.5 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 8, levels 4, expressions 13 rejected: reduceCtorType: invalid return type for 'reduceCtorType.mk'
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: 115 ms · instructions: 469.1 M · max rss memory: 91.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 13, levels 2, expressions 14 rejected: indNegReducible: arg #1 of 'indNegReducible.mk' has a non positive occurrence of the datatypes being declared
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: 115 ms · instructions: 476.3 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 9, levels 2, expressions 20 checked 2, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 480.9 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 10, levels 4, expressions 21 checked 2, admitted unchecked 0, skipped 0 accepted
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: 119 ms · instructions: 484.4 M · max rss memory: 91.8 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 11, levels 5, expressions 21 checked 2, admitted unchecked 0, skipped 0 accepted
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: 111 ms · instructions: 460.7 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 1, names 5, levels 2, expressions 4 rejected: typeWithTooHighTypeField: universe level of type_of(arg #1) of 'typeWithTooHighTypeField.mk' is too big for the corresponding inductive datatype
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: 115 ms · instructions: 474.5 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 2, names 7, levels 3, expressions 10 checked 2, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 482.2 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 17, levels 3, expressions 32 checked 2, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 483.3 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 23, levels 3, expressions 50 checked 3, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 485.2 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 13, levels 2, expressions 42 checked 2, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 486.8 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 21, levels 8, expressions 49 checked 2, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 489.9 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 21, levels 8, expressions 48 checked 2, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 477.6 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 16, levels 4, expressions 18 checked 2, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 478.7 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 16, levels 3, expressions 43 checked 2, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 478.3 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 21, levels 3, expressions 36 checked 2, admitted unchecked 0, skipped 0 accepted
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: 120 ms · instructions: 554.6 M · max rss memory: 100.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 14, declarations 4, names 41, levels 5, expressions 254 checked 4, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 472.9 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 10, levels 1, expressions 22 checked 2, admitted unchecked 0, skipped 0 accepted
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: 119 ms · instructions: 476.1 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 6, declarations 3, names 10, levels 3, expressions 12 rejected: BogusRecursor: invalid recursor 'BogusRecursor.rec'
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: 127 ms · instructions: 488.5 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 18, levels 2, expressions 45 checked 2, admitted unchecked 0, skipped 0 accepted
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: 126 ms · instructions: 556.2 M · max rss memory: 99.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 12, declarations 5, names 35, levels 4, expressions 95 checked 5, admitted unchecked 0, skipped 0 accepted
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: 129 ms · instructions: 484.7 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 23, levels 3, expressions 69 checked 3, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 489.6 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 9, declarations 4, names 25, levels 3, expressions 83 checked 4, admitted unchecked 0, skipped 0 accepted
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: 121 ms · instructions: 554.2 M · max rss memory: 100.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 59, levels 4, expressions 133 checked 4, admitted unchecked 0, skipped 0 accepted
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: 120 ms · instructions: 553.2 M · max rss memory: 100.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 7, declarations 3, names 68, levels 8, expressions 127 checked 3, admitted unchecked 0, skipped 0 accepted
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: 156 ms · instructions: 564.0 M · max rss memory: 100.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 13, declarations 6, names 59, levels 4, expressions 170 checked 6, admitted unchecked 0, skipped 0 accepted
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: 122 ms · instructions: 569.2 M · max rss memory: 99.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 14, declarations 7, names 68, levels 5, expressions 256 checked 7, admitted unchecked 0, skipped 0 accepted
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: 125 ms · instructions: 674.0 M · max rss memory: 105.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 19, declarations 7, names 117, levels 5, expressions 878 checked 7, admitted unchecked 0, skipped 0 accepted
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: 120 ms · instructions: 483.1 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 15, levels 2, expressions 55 checked 3, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 485.5 M · max rss memory: 91.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 17, levels 7, expressions 57 checked 3, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 491.4 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 17, levels 7, expressions 57 checked 3, admitted unchecked 0, skipped 0 accepted
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: 119 ms · instructions: 498.2 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 22, levels 7, expressions 65 checked 3, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 479.7 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 16, levels 2, expressions 48 rejected: projOutOfRange: invalid projection
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: 126 ms · instructions: 484.0 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 22, levels 3, expressions 38 rejected: projNotStruct: invalid projection
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: 125 ms · instructions: 559.6 M · max rss memory: 100.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 103 checked 4, admitted unchecked 0, skipped 0 accepted
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: 127 ms · instructions: 559.0 M · max rss memory: 99.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 103 rejected: projProp2: invalid projection
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: 120 ms · instructions: 551.4 M · max rss memory: 100.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 103 checked 4, admitted unchecked 0, skipped 0 accepted
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: 120 ms · instructions: 546.6 M · max rss memory: 99.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 103 rejected: projProp4: invalid projection
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: 121 ms · instructions: 551.5 M · max rss memory: 99.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 108 rejected: projProp5: invalid projection
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: 126 ms · instructions: 550.5 M · max rss memory: 100.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 10, declarations 4, names 32, levels 5, expressions 103 rejected: projProp6: invalid projection
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: 121 ms · instructions: 485.9 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 32, levels 4, expressions 72 checked 4, admitted unchecked 0, skipped 0 accepted
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: 154 ms · instructions: 557.0 M · max rss memory: 99.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 20, declarations 7, names 52, levels 5, expressions 163 rejected: projIndexData: invalid projection
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: 125 ms · instructions: 566.1 M · max rss memory: 100.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 20, declarations 7, names 52, levels 5, expressions 163 rejected: projIndexData2: invalid projection
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: 125 ms · instructions: 566.6 M · max rss memory: 100.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 13, declarations 6, names 33, levels 8, expressions 131 checked 6, admitted unchecked 0, skipped 0 accepted
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: 123 ms · instructions: 488.2 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 32, levels 4, expressions 83 checked 3, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 495.4 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 32, levels 4, expressions 83 rejected: ruleKbad: declaration type mismatch
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: 119 ms · instructions: 556.3 M · max rss memory: 100.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 42, levels 4, expressions 180 rejected: ruleKAcc: declaration type mismatch
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: 114 ms · instructions: 485.4 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 2, names 13, levels 3, expressions 37 checked 2, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 492.8 M · max rss memory: 92.8 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 3, names 24, levels 4, expressions 84 checked 3, admitted unchecked 0, skipped 0 accepted
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: 139 ms · instructions: 487.5 M · max rss memory: 91.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 29, levels 3, expressions 66 checked 3, admitted unchecked 0, skipped 0 accepted
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: 114 ms · instructions: 487.3 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 20, levels 4, expressions 67 rejected: proofIrrelevanceBad: declaration type mismatch
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: 119 ms · instructions: 492.9 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 6, declarations 4, names 30, levels 5, expressions 74 checked 4, admitted unchecked 0, skipped 0 accepted
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: 110 ms · instructions: 461.7 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 7, declarations 7, names 14, levels 2, expressions 17 checked 7, admitted unchecked 0, skipped 0 accepted
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: 121 ms · instructions: 490.6 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 9, declarations 5, names 31, levels 4, expressions 77 checked 5, admitted unchecked 0, skipped 0 accepted
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: 122 ms · instructions: 490.5 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 4, names 30, levels 3, expressions 73 checked 4, admitted unchecked 0, skipped 0 accepted
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: 112 ms · instructions: 487.1 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 4, names 30, levels 3, expressions 75 checked 4, admitted unchecked 0, skipped 0 accepted
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: 123 ms · instructions: 493.8 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 28, levels 4, expressions 86 rejected: indexedUnitEta: declaration type mismatch
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: 118 ms · instructions: 562.3 M · max rss memory: 99.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 13, declarations 7, names 44, levels 7, expressions 173 checked 7, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 551.8 M · max rss memory: 99.9 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 14, declarations 5, names 31, levels 4, expressions 99 rejected: indexedStructEta: declaration type mismatch
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: 116 ms · instructions: 487.1 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 27, levels 4, expressions 71 checked 3, admitted unchecked 0, skipped 0 accepted
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: 113 ms · instructions: 493.4 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 27, levels 4, expressions 73 checked 3, admitted unchecked 0, skipped 0 accepted
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: 115 ms · instructions: 491.5 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 28, levels 4, expressions 64 rejected: funEtaBad: declaration type mismatch
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: 114 ms · instructions: 477.5 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 7, declarations 2, names 16, levels 3, expressions 41 rejected: reflOccLeft: arg #1 of 'reflOccLeft.mk' has a non positive occurrence of the datatypes being declared
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: 112 ms · instructions: 482.1 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 7, declarations 2, names 17, levels 3, expressions 45 rejected: reflOccInIndex: application type mismatch
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: 123 ms · instructions: 494.9 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 19, levels 5, expressions 62 checked 3, admitted unchecked 0, skipped 0 accepted
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: 126 ms · instructions: 494.5 M · max rss memory: 92.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 5, declarations 3, names 19, levels 5, expressions 62 checked 3, admitted unchecked 0, skipped 0 accepted
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: 123 ms · instructions: 485.5 M · max rss memory: 92.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 9, declarations 3, names 25, levels 4, expressions 60 checked 3, admitted unchecked 0, skipped 0 accepted
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: 125 ms · instructions: 559.5 M · max rss memory: 100.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 14, declarations 6, names 48, levels 4, expressions 134 checked 6, admitted unchecked 0, skipped 0 accepted
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: 122 ms · instructions: 552.7 M · max rss memory: 99.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 22, levels 4, expressions 124 checked 2, admitted unchecked 0, skipped 0 accepted
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: 121 ms · instructions: 558.2 M · max rss memory: 100.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 43, levels 4, expressions 193 checked 4, admitted unchecked 0, skipped 0 accepted
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: 130 ms · instructions: 563.6 M · max rss memory: 100.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 11, declarations 4, names 42, levels 4, expressions 186 rejected: accRecNoEta: declaration type mismatch
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: 125 ms · instructions: 486.4 M · max rss memory: 92.0 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 6, names 27, levels 4, expressions 87 checked 6, admitted unchecked 0, skipped 0 accepted
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: 117 ms · instructions: 482.9 M · max rss memory: 92.1 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 6, names 27, levels 4, expressions 88 checked 6, admitted unchecked 0, skipped 0 accepted
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: 118 ms · instructions: 488.3 M · max rss memory: 92.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 6, names 27, levels 4, expressions 88 checked 6, admitted unchecked 0, skipped 0 accepted
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: 130 ms · instructions: 550.3 M · max rss memory: 99.2 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 9, declarations 7, names 28, levels 4, expressions 103 checked 7, admitted unchecked 0, skipped 0 accepted
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: 120 ms · instructions: 549.7 M · max rss memory: 99.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 6, names 28, levels 4, expressions 116 checked 6, admitted unchecked 0, skipped 0 accepted
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: 116 ms · instructions: 552.3 M · max rss memory: 99.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 8, declarations 6, names 27, levels 4, expressions 115 checked 6, admitted unchecked 0, skipped 0 accepted
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: 108 ms · instructions: 440.2 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 2, declarations 2, names 2, levels 2, expressions 2 rejected: dup_defs: already declared
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: 118 ms · instructions: 451.9 M · max rss memory: 91.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 8, levels 3, expressions 15 rejected: dup_ind_def: 'dup_ind_def' or its recursor has already been declared
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: 112 ms · instructions: 455.2 M · max rss memory: 91.5 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 8, levels 3, expressions 15 rejected: dup_ctor_def: duplicate or already declared constructor '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: 143 ms · instructions: 454.0 M · max rss memory: 91.3 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 8, levels 3, expressions 15 rejected: dup_rec_def: 'dup_rec_def' or its recursor has already been declared
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: 113 ms · instructions: 472.7 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 10, levels 4, expressions 18 rejected: misnamed_rec: invalid recursor 'misnamed_rec.not_rec'
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: 113 ms · instructions: 458.9 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 2, names 9, levels 3, expressions 15 rejected: dup_rec_def2: 'dup_rec_def2' or its recursor has already been declared
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: 112 ms · instructions: 469.0 M · max rss memory: 91.4 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 3, declarations 1, names 7, levels 3, expressions 14 rejected: dup_ctor_rec: incorrect number of universe levels for '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: 111 ms · instructions: 456.7 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 1, names 10, levels 3, expressions 21 rejected: DupConCon: duplicate or already declared constructor '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: 115 ms · instructions: 464.2 M · max rss memory: 91.7 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 3, names 8, levels 2, expressions 10 rejected: falseFromUnsafe: unknown constant 'unsafeLoop'
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: 113 ms · instructions: 471.4 M · max rss memory: 91.6 MB · run 2026-11-08 19:19:35 UTC
stdout:
constants 4, declarations 3, names 8, levels 2, expressions 10 rejected: falseFromPartial: unknown constant 'partialLoop'