Checker "overfull" on the tests of "tutorial"
Checker: overfull · Version: b275736 · 📄 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: 298 ms · instructions: 5.6 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 301 ms · instructions: 5.8 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 384 ms · instructions: 7.7 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 325 ms · instructions: 6.3 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 492 ms · instructions: 10.1 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 724 ms · instructions: 15.4 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 753 ms · instructions: 16.4 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 709 ms · instructions: 15.1 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 776 ms · instructions: 15.8 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT 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: 549 ms · instructions: 11.7 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT 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: 539 ms · instructions: 11.2 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT 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: 306 ms · instructions: 6.0 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT theorem-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: 748 ms · instructions: 16.2 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 331 ms · instructions: 6.5 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT unknown-constant
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: 311 ms · instructions: 6.0 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 320 ms · instructions: 6.3 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 332 ms · instructions: 6.5 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 771 ms · instructions: 16.5 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 327 ms · instructions: 5.9 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-universe
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: 316 ms · instructions: 6.2 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 320 ms · instructions: 6.3 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 465 ms · instructions: 9.5 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 478 ms · instructions: 10.0 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 379 ms · instructions: 7.6 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 431 ms · instructions: 8.8 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 342 ms · instructions: 6.7 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 381 ms · instructions: 7.6 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 443 ms · instructions: 9.0 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 772 ms · instructions: 16.6 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.20 s · instructions: 49.4 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.48 s · instructions: 77.1 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
032_peano3
Test: tutorial/032_peano3 · Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 4.16 s · instructions: 94.4 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 343 ms · instructions: 6.8 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 669 ms · instructions: 14.2 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 403 ms · instructions: 8.0 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 606 ms · instructions: 12.8 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.21 s · instructions: 25.0 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.11 s · instructions: 46.9 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.85 s · instructions: 41.0 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.28 s · instructions: 50.7 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.29 s · instructions: 50.6 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 895 ms · instructions: 19.6 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.92 s · instructions: 43.4 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.77 s · instructions: 39.3 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 12.8 s · instructions: 285.0 G · max rss memory: 47.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 573 ms · instructions: 12.0 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT 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: 360 ms · instructions: 7.1 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT inductive-type
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: 327 ms · instructions: 6.3 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-universe
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: 347 ms · instructions: 6.7 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT inductive-type
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: 590 ms · instructions: 12.5 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT parameter-type
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: 659 ms · instructions: 14.0 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT constructor-return
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: 725 ms · instructions: 15.5 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT constructor-return
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: 546 ms · instructions: 11.3 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT constructor-return
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: 507 ms · instructions: 10.7 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT negative-occurrence
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: 2.49 s · instructions: 55.3 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 800 ms · instructions: 16.7 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT constructor-return
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: 924 ms · instructions: 20.1 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT negative-occurrence
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: 992 ms · instructions: 21.6 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.07 s · instructions: 22.8 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.12 s · instructions: 24.2 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 494 ms · instructions: 9.9 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT constructor-universe
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: 684 ms · instructions: 14.4 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.72 s · instructions: 38.1 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.67 s · instructions: 59.6 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.05 s · instructions: 45.8 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.59 s · instructions: 58.6 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.56 s · instructions: 58.0 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.18 s · instructions: 25.4 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.19 s · instructions: 49.2 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.89 s · instructions: 42.2 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 14.0 s · instructions: 317.1 G · max rss memory: 47.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.16 s · instructions: 25.4 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 846 ms · instructions: 18.3 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT recursor-metadata
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: 2.40 s · instructions: 54.3 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.79 s · instructions: 107.5 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
076_sortElimPropRec
Test: tutorial/076_sortElimPropRec · Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 3.43 s · instructions: 77.5 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.28 s · instructions: 96.7 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 7.84 s · instructions: 177.7 G · max rss memory: 46.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 8.16 s · instructions: 185.7 G · max rss memory: 46.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 9.52 s · instructions: 215.9 G · max rss memory: 47.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 16.9 s · instructions: 381.7 G · max rss memory: 47.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: ⌛ timeout · exit code -9 · wall time: 30.0 s · max rss memory: 0 B · run 2026-10-24 17:15:13 UTC
stderr:
Killed after exceeding the timeout of 30.0 s.
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: 2.82 s · instructions: 58.1 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.23 s · instructions: 66.1 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.23 s · instructions: 65.8 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.08 s · instructions: 83.0 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.39 s · instructions: 48.5 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-index
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: 2.05 s · instructions: 41.2 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-structure
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: 5.38 s · instructions: 111.2 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 5.43 s · instructions: 111.5 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-prop
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: 5.38 s · instructions: 111.5 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 5.45 s · instructions: 111.7 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-prop
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: 5.45 s · instructions: 115.4 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-prop
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: 5.28 s · instructions: 111.7 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-prop
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: 4.25 s · instructions: 83.8 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 9.23 s · instructions: 193.0 G · max rss memory: 47.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-type
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: 9.28 s · instructions: 193.2 G · max rss memory: 46.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT projection-type
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.06 s · instructions: 148.7 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.47 s · instructions: 94.4 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.43 s · instructions: 94.8 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 9.71 s · instructions: 216.6 G · max rss memory: 47.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 1.64 s · instructions: 36.2 G · max rss memory: 45.9 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.77 s · instructions: 84.8 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.25 s · instructions: 72.1 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.06 s · instructions: 68.8 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 3.60 s · instructions: 81.3 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 1.04 s · instructions: 22.3 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.90 s · instructions: 86.5 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
109_unitEta2
Test: tutorial/109_unitEta2 · Expected: 👍 accept · Size: 5.9 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 3.63 s · instructions: 82.0 G · max rss memory: 46.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
110_unitEta3
Test: tutorial/110_unitEta3 · Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 3.68 s · instructions: 82.8 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.20 s · instructions: 93.9 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 9.68 s · instructions: 218.5 G · max rss memory: 47.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 4.83 s · instructions: 109.3 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 3.47 s · instructions: 78.4 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
115_funEtaDep
Test: tutorial/115_funEtaDep · Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 3.59 s · instructions: 80.9 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
116_funEtaBad
Test: tutorial/116_funEtaBad · Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: ✋ rejected · exit code 1 · wall time: 3.28 s · instructions: 73.9 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 1.95 s · instructions: 43.6 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT negative-occurrence
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: 2.07 s · instructions: 46.2 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT argument-type
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: 2.84 s · instructions: 62.4 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 2.77 s · instructions: 62.2 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
121_rTreeRec
Test: tutorial/121_rTreeRec · Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 3.09 s · instructions: 69.1 G · max rss memory: 46.0 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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.17 s · instructions: 161.5 G · max rss memory: 46.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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.68 s · instructions: 128.7 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 11.8 s · instructions: 268.1 G · max rss memory: 47.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 9.73 s · instructions: 220.5 G · max rss memory: 47.1 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT declaration-type
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: 3.81 s · instructions: 86.2 G · max rss memory: 46.3 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 3.98 s · instructions: 89.6 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
128_quotLiftType
Test: tutorial/128_quotLiftType · Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 4.05 s · instructions: 91.4 G · max rss memory: 46.2 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
129_quotSoundType
Test: tutorial/129_quotSoundType · Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial
Result: 👍 accepted · exit code 0 · wall time: 4.69 s · instructions: 106.4 G · max rss memory: 46.4 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 6.17 s · instructions: 140.2 G · max rss memory: 46.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 5.86 s · instructions: 132.7 G · max rss memory: 46.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
ACCEPT
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: 314 ms · instructions: 6.1 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 725 ms · instructions: 15.4 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 733 ms · instructions: 15.7 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 754 ms · instructions: 16.2 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 952 ms · instructions: 20.2 G · max rss memory: 45.7 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT missing-recursor
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: 834 ms · instructions: 18.0 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT missing-recursor
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: 698 ms · instructions: 14.9 G · max rss memory: 45.6 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 940 ms · instructions: 20.3 G · max rss memory: 45.8 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT duplicate-declaration
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: 647 ms · instructions: 13.8 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT unknown-constant
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: 650 ms · instructions: 13.8 G · max rss memory: 45.5 MB · run 2026-10-24 17:15:13 UTC
stdout:
REJECT unknown-constant