Lean Kernel Arena / lean4cobol / tutorial

Checker "lean4cobol" on the tests of "tutorial"

Checker: lean4cobol · Version: d2e7b79 · 📄 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: 8.60 ms · instructions: 7.6 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=6 names=2 levels=3 exprs=2 longest=172
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: 9.02 ms · instructions: 7.6 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=6 names=2 levels=3 exprs=3 longest=172
stderr:
rejected at record 00000000000000000006

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: 8.71 ms · instructions: 8.3 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=7 levels=3 exprs=3 longest=172
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: 9.81 ms · instructions: 7.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=7 names=3 levels=2 exprs=3 longest=172
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: 9.49 ms · instructions: 8.9 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=17 names=9 levels=3 exprs=6 longest=172
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: 8.81 ms · instructions: 10.3 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=27 names=11 levels=3 exprs=13 longest=172
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: 7.49 ms · instructions: 10.5 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=28 names=11 levels=3 exprs=14 longest=172
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: 8.93 ms · instructions: 10.1 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=25 names=7 levels=6 exprs=13 longest=172
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: 12.4 ms · instructions: 10.2 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=26 names=7 levels=6 exprs=22 longest=172
stderr:
rejected at record 00000000000000000026

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: 7.99 ms · instructions: 9.4 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=21 names=10 levels=3 exprs=8 longest=172
stderr:
rejected at record 00000000000000000021

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: 7.05 ms · instructions: 9.3 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=20 names=10 levels=3 exprs=7 longest=172
stderr:
rejected at record 00000000000000000020

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: 8.76 ms · instructions: 7.7 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=7 names=3 levels=2 exprs=4 longest=172
stderr:
rejected at record 00000000000000000007

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: 7.46 ms · instructions: 10.4 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=26 names=10 levels=2 exprs=14 longest=172
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: 9.14 ms · instructions: 7.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=3 levels=2 exprs=6 longest=172
stderr:
rejected at record 00000000000000000008

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: 7.24 ms · instructions: 7.7 M · max rss memory: 13.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=7 names=2 levels=5 exprs=2 longest=172
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: 7.37 ms · instructions: 7.8 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=2 levels=7 exprs=2 longest=172
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: 8.57 ms · instructions: 7.9 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=9 names=2 levels=8 exprs=2 longest=172
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: 7.42 ms · instructions: 10.6 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=29 names=12 levels=5 exprs=13 longest=172
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: 8.11 ms · instructions: 7.7 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=3 levels=3 exprs=2 longest=172
stderr:
rejected at record 00000000000000000008

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: 7.68 ms · instructions: 7.8 M · max rss memory: 13.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=3 levels=4 exprs=2 longest=172
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: 7.57 ms · instructions: 7.8 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=3 levels=4 exprs=2 longest=172
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: 8.75 ms · instructions: 8.8 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=16 names=8 levels=3 exprs=6 longest=172
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: 8.91 ms · instructions: 8.8 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=17 names=8 levels=4 exprs=6 longest=172
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: 11.0 ms · instructions: 8.2 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=4 levels=11 exprs=2 longest=172
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: 12.1 ms · instructions: 8.6 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=16 names=5 levels=16 exprs=2 longest=172
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: 8.39 ms · instructions: 7.9 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=9 names=3 levels=6 exprs=2 longest=172
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: 8.26 ms · instructions: 8.2 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=4 levels=11 exprs=2 longest=172
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: 8.93 ms · instructions: 8.5 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=4 levels=2 exprs=7 longest=172
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: 7.34 ms · instructions: 10.5 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=26 names=10 levels=2 exprs=15 longest=172
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: 7.59 ms · instructions: 18.0 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=73 names=21 levels=10 exprs=41 longest=172
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: 21.3 ms · instructions: 23.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=90 names=23 levels=10 exprs=55 longest=172
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: 8.62 ms · instructions: 27.4 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=98 names=25 levels=10 exprs=59 longest=172
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: 7.94 ms · instructions: 8.0 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=9 names=3 levels=3 exprs=4 longest=172
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: 10.3 ms · instructions: 10.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=26 names=11 levels=3 exprs=11 longest=172
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: 8.62 ms · instructions: 8.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=4 levels=3 exprs=5 longest=172
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: 8.39 ms · instructions: 9.7 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=20 names=7 levels=4 exprs=15 longest=341
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: 9.35 ms · instructions: 12.5 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=37 names=11 levels=4 exprs=39 longest=611
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: 7.64 ms · instructions: 17.0 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=65 names=17 levels=4 exprs=91 longest=611
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: 8.05 ms · instructions: 17.0 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=57 names=13 levels=3 exprs=144 longest=476
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: 7.87 ms · instructions: 18.9 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=76 names=20 levels=16 exprs=142 longest=487
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: 8.33 ms · instructions: 18.7 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=75 names=20 levels=16 exprs=142 longest=487
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: 7.67 ms · instructions: 11.3 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=31 names=10 levels=6 exprs=26 longest=479
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: 8.70 ms · instructions: 17.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=62 names=16 levels=7 exprs=133 longest=481
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: 9.04 ms · instructions: 15.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=61 names=21 levels=4 exprs=83 longest=611
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: 17.0 ms · instructions: 72.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=296 names=40 levels=7 exprs=947 longest=777
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: 8.28 ms · instructions: 9.6 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=20 names=10 levels=3 exprs=8 longest=198
stderr:
rejected at record 00000000000000000020

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: 7.08 ms · instructions: 8.2 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=8 names=3 levels=3 exprs=3 longest=198
stderr:
rejected at record 00000000000000000008

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: 6.95 ms · instructions: 7.9 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=7 names=3 levels=3 exprs=1 longest=201
stderr:
rejected at record 00000000000000000007

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: 7.22 ms · instructions: 7.9 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=6 names=3 levels=1 exprs=3 longest=198
stderr:
rejected at record 00000000000000000006

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: 7.43 ms · instructions: 9.7 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=16 names=6 levels=3 exprs=13 longest=442
stderr:
rejected at record 00000000000000000016

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: 10.4 ms · instructions: 10.2 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=19 names=6 levels=3 exprs=32 longest=443
stderr:
rejected at record 00000000000000000019

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: 9.00 ms · instructions: 10.7 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=23 names=8 levels=5 exprs=33 longest=449
stderr:
rejected at record 00000000000000000023

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: 9.24 ms · instructions: 9.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=14 names=6 levels=2 exprs=9 longest=442
stderr:
rejected at record 00000000000000000014

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: 9.11 ms · instructions: 9.1 M · max rss memory: 13.3 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=12 names=5 levels=3 exprs=8 longest=442
stderr:
rejected at record 00000000000000000012

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: 9.70 ms · instructions: 19.3 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=80 names=19 levels=7 exprs=127 longest=483
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: 9.23 ms · instructions: 10.6 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=26 names=8 levels=6 exprs=16 longest=444
stderr:
rejected at record 00000000000000000026

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: 8.68 ms · instructions: 11.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=31 names=13 levels=3 exprs=17 longest=451
stderr:
rejected at record 00000000000000000031

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: 9.00 ms · instructions: 11.8 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=32 names=9 levels=3 exprs=40 longest=474
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: 8.79 ms · instructions: 12.0 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=36 names=10 levels=5 exprs=40 longest=475
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: 8.67 ms · instructions: 12.5 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=38 names=11 levels=6 exprs=40 longest=479
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: 13.6 ms · instructions: 9.0 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=11 names=5 levels=3 exprs=6 longest=442
stderr:
rejected at record 00000000000000000011

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: 9.53 ms · instructions: 10.1 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=21 names=7 levels=7 exprs=16 longest=341
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: 10.4 ms · instructions: 15.3 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=53 names=17 levels=9 exprs=49 longest=611
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: 10.4 ms · instructions: 19.7 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=78 names=23 levels=9 exprs=98 longest=611
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: 14.7 ms · instructions: 18.2 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=58 names=13 levels=7 exprs=145 longest=476
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: 20.9 ms · instructions: 20.9 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=79 names=21 levels=22 exprs=144 longest=487
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: 13.3 ms · instructions: 20.8 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=78 names=21 levels=24 exprs=143 longest=487
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: 8.29 ms · instructions: 12.7 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=39 names=16 levels=10 exprs=28 longest=479
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: 8.69 ms · instructions: 18.7 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=63 names=16 levels=14 exprs=134 longest=481
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: 7.96 ms · instructions: 16.3 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=61 names=21 levels=8 exprs=83 longest=611
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: 14.7 ms · instructions: 80.8 M · max rss memory: 14.0 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=303 names=41 levels=20 exprs=953 longest=777
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: 9.62 ms · instructions: 12.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=34 names=10 levels=2 exprs=39 longest=610
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: 9.50 ms · instructions: 11.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=27 names=10 levels=4 exprs=37 longest=443
stderr:
rejected at record 00000000000000000027

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: 9.68 ms · instructions: 20.6 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=66 names=18 levels=6 exprs=172 longest=482
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: 9.71 ms · instructions: 30.1 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=138 names=35 levels=9 exprs=211 longest=625
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: 9.18 ms · instructions: 24.3 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=97 names=23 levels=9 exprs=202 longest=611
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: 9.11 ms · instructions: 28.0 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=114 names=25 levels=6 exprs=222 longest=611
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: 10.3 ms · instructions: 44.2 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=199 names=59 levels=9 exprs=342 longest=626
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: 10.4 ms · instructions: 45.1 M · max rss memory: 13.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=205 names=68 levels=21 exprs=312 longest=491
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: 10.9 ms · instructions: 50.7 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=238 names=59 levels=10 exprs=409 longest=625
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: 13.4 ms · instructions: 81.1 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=335 names=68 levels=19 exprs=556 longest=616
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: 25.1 ms · instructions: 257.0 M · max rss memory: 14.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=1006 names=117 levels=11 exprs=1667 longest=777
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: 8.02 ms · instructions: 20.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=74 names=15 levels=3 exprs=158 longest=476
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: 12.5 ms · instructions: 22.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=83 names=17 levels=14 exprs=152 longest=487
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: 10.0 ms · instructions: 22.5 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=83 names=17 levels=21 exprs=152 longest=487
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: 9.33 ms · instructions: 26.6 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=96 names=22 levels=22 exprs=178 longest=491
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: 8.56 ms · instructions: 18.8 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=67 names=16 levels=3 exprs=168 longest=476
stderr:
rejected at record 00000000000000000067

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: 8.08 ms · instructions: 16.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=64 names=22 levels=4 exprs=88 longest=611
stderr:
rejected at record 00000000000000000064

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: 8.91 ms · instructions: 31.9 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=143 names=32 levels=9 exprs=348 longest=496
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: 9.09 ms · instructions: 31.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=143 names=32 levels=9 exprs=362 longest=496
stderr:
rejected at record 00000000000000000143

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: 9.16 ms · instructions: 31.9 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=143 names=32 levels=9 exprs=348 longest=496
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: 9.09 ms · instructions: 31.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=143 names=32 levels=9 exprs=362 longest=496
stderr:
rejected at record 00000000000000000143

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: 9.18 ms · instructions: 32.5 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=148 names=32 levels=9 exprs=369 longest=496
stderr:
rejected at record 00000000000000000148

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: 11.2 ms · instructions: 31.9 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=143 names=32 levels=9 exprs=362 longest=496
stderr:
rejected at record 00000000000000000143

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: 9.99 ms · instructions: 25.0 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=111 names=32 levels=8 exprs=170 longest=611
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: 10.3 ms · instructions: 46.4 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=226 names=52 levels=10 exprs=512 longest=611
stderr:
rejected at record 00000000000000000226

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: 10.8 ms · instructions: 46.4 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=226 names=52 levels=10 exprs=512 longest=611
stderr:
rejected at record 00000000000000000226

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: 10.3 ms · instructions: 38.7 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=177 names=33 levels=19 exprs=333 longest=627
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: 9.26 ms · instructions: 27.5 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=121 names=32 levels=8 exprs=190 longest=627
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: 8.88 ms · instructions: 27.9 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=121 names=32 levels=8 exprs=278 longest=627
stderr:
rejected at record 00000000000000000121

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: 10.7 ms · instructions: 54.1 M · max rss memory: 13.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=229 names=42 levels=11 exprs=824 longest=629
stderr:
rejected at record 00000000000000000229

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: 8.18 ms · instructions: 14.8 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=54 names=13 levels=4 exprs=84 longest=610
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: 8.76 ms · instructions: 25.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=114 names=24 levels=8 exprs=221 longest=626
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: 10.3 ms · instructions: 23.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=100 names=29 levels=8 exprs=157 longest=481
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: 8.01 ms · instructions: 22.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=93 names=20 levels=9 exprs=199 longest=481
stderr:
rejected at record 00000000000000000093

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: 8.32 ms · instructions: 25.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=112 names=30 levels=10 exprs=164 longest=484
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: 7.67 ms · instructions: 12.1 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=39 names=14 levels=3 exprs=17 longest=172
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: 9.65 ms · instructions: 25.9 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=116 names=31 levels=9 exprs=177 longest=488
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: 7.94 ms · instructions: 25.2 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=109 names=30 levels=8 exprs=174 longest=484
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: 8.25 ms · instructions: 25.3 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=111 names=30 levels=8 exprs=176 longest=484
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: 8.36 ms · instructions: 27.3 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=121 names=28 levels=8 exprs=242 longest=611
stderr:
rejected at record 00000000000000000121

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: 11.2 ms · instructions: 54.0 M · max rss memory: 13.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=230 names=44 levels=18 exprs=461 longest=493
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: 9.12 ms · instructions: 30.4 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=138 names=31 levels=8 exprs=265 longest=611
stderr:
rejected at record 00000000000000000138

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: 8.36 ms · instructions: 24.2 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=104 names=27 levels=9 exprs=161 longest=481
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: 8.40 ms · instructions: 24.9 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=106 names=27 levels=9 exprs=163 longest=481
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: 8.41 ms · instructions: 23.1 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=97 names=28 levels=8 exprs=232 longest=481
stderr:
rejected at record 00000000000000000097

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: 8.05 ms · instructions: 16.3 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=61 names=16 levels=4 exprs=92 longest=610
stderr:
rejected at record 00000000000000000061

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: 8.06 ms · instructions: 17.1 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=66 names=17 levels=5 exprs=99 longest=610
stderr:
rejected at record 00000000000000000066

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: 7.89 ms · instructions: 20.8 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=88 names=19 levels=7 exprs=157 longest=482
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: 9.78 ms · instructions: 20.9 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=88 names=19 levels=7 exprs=157 longest=482
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: 14.6 ms · instructions: 21.8 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=91 names=25 levels=12 exprs=140 longest=623
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: 11.0 ms · instructions: 40.2 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=191 names=48 levels=9 exprs=304 longest=623
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: 11.0 ms · instructions: 37.3 M · max rss memory: 13.5 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=151 names=22 levels=19 exprs=441 longest=483
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: 12.3 ms · instructions: 64.3 M · max rss memory: 13.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=243 names=43 levels=11 exprs=616 longest=629
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: 13.3 ms · instructions: 54.3 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=235 names=42 levels=11 exprs=849 longest=629
stderr:
rejected at record 00000000000000000235

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: 13.5 ms · instructions: 26.3 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=123 names=27 levels=12 exprs=281 longest=481
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: 10.6 ms · instructions: 27.3 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=124 names=27 levels=10 exprs=282 longest=481
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: 9.53 ms · instructions: 27.5 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=124 names=27 levels=15 exprs=282 longest=481
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: 11.8 ms · instructions: 30.4 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=141 names=28 levels=10 exprs=297 longest=481
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: 36.1 ms · instructions: 36.9 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=153 names=28 levels=12 exprs=310 longest=481
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: 10.4 ms · instructions: 35.5 M · max rss memory: 13.7 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=151 names=27 levels=10 exprs=309 longest=481
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: 7.80 ms · instructions: 7.6 M · max rss memory: 12.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=7 names=2 levels=2 exprs=2 longest=172
stderr:
rejected at record 00000000000000000007

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: 17.4 ms · instructions: 9.7 M · max rss memory: 13.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=27 names=8 levels=3 exprs=15 longest=475
stderr:
rejected at record 00000000000000000027

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: 8.05 ms · instructions: 9.8 M · max rss memory: 13.2 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=27 names=8 levels=3 exprs=15 longest=475
stderr:
rejected at record 00000000000000000027

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: 9.57 ms · instructions: 9.9 M · max rss memory: 12.9 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=27 names=8 levels=3 exprs=15 longest=475
stderr:
rejected at record 00000000000000000027

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: 8.38 ms · instructions: 11.8 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=33 names=11 levels=9 exprs=36 longest=475
stderr:
rejected at record 00000000000000000033

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: 9.11 ms · instructions: 11.0 M · max rss memory: 13.6 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=28 names=9 levels=4 exprs=25 longest=475
stderr:
rejected at record 00000000000000000028

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: 8.07 ms · instructions: 9.6 M · max rss memory: 13.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=24 names=7 levels=3 exprs=14 longest=475
stderr:
rejected at record 00000000000000000024

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: 12.6 ms · instructions: 10.7 M · max rss memory: 13.1 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=34 names=10 levels=3 exprs=21 longest=611
stderr:
rejected at record 00000000000000000034

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: 8.83 ms · instructions: 10.0 M · max rss memory: 13.8 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=22 names=8 levels=3 exprs=16 longest=341
stderr:
rejected at record 00000000000000000022

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: 7.53 ms · instructions: 10.0 M · max rss memory: 13.4 MB · run 2026-10-24 17:06:14 UTC

stdout:
records=22 names=8 levels=3 exprs=16 longest=341
stderr:
rejected at record 00000000000000000022