Lean Kernel Arena / logos-kernel / tutorial

Checker "logos-kernel" on the tests of "tutorial"

Checker: logos-kernel · Version: 1e6ad5b · 📄 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: 3.13 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 6 records; native primitives:

002_badDef

Test: tutorial/002_badDef · Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 3.71 ms · instructions: 2.4 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'badDef': declaration type mismatch
  the value has type
    Sort LevelId(2)
  but is declared with type
    Sort LevelId(0)

003_arrowType

Test: tutorial/003_arrowType · Expected: 👍 accept · Size: 622 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.16 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 12 records; native primitives:

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: 2.98 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 7 records; native primitives:

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: 2.77 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 17 records; native primitives:

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: 2.73 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 27 records; native primitives:

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: 2.78 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 28 records; native primitives:

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: 2.74 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 25 records; native primitives:

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: 8.94 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'forallSortBad': type expected, a binder type has type x0
  at export line 26

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: 2.89 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'nonTypeType': type expected, found constType
  at export line 21

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: 2.60 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'nonTypeAxiom': type expected, found constType
  at export line 20

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: 2.75 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'nonPropThm': theorem type is not a proposition
  its type is 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: 3.09 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 26 records; native primitives:

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: 2.70 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'selfProof': unknown constant 'selfProof'
  at export line 8

015_levelComp1

Test: tutorial/015_levelComp1 · Expected: 👍 accept · Size: 391 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.36 ms · instructions: 2.4 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 7 records; native primitives:

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: 2.73 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 8 records; native primitives:

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: 2.70 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 9 records; native primitives:

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: 2.68 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 29 records; native primitives:

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: 2.95 ms · instructions: 2.3 M · max rss memory: 3.0 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'tut06_bad01': duplicate universe level parameter 'u'
  at export line 8

020_levelComp4

Test: tutorial/020_levelComp4 · Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.29 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 8 records; native primitives:

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: 2.57 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 8 records; native primitives:

022_imax1

Test: tutorial/022_imax1 · Expected: 👍 accept · Size: 809 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.36 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 16 records; native primitives:

023_imax2

Test: tutorial/023_imax2 · Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.11 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 17 records; native primitives:

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: 2.87 ms · instructions: 2.4 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 12 records; native primitives:

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: 3.25 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 16 records; native primitives:

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: 2.62 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 9 records; native primitives:

027_levelMaxAbsorb

Test: tutorial/027_levelMaxAbsorb · Expected: 👍 accept · Size: 526 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.40 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 12 records; native primitives:

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: 2.83 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 12 records; native primitives:

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: 2.73 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 26 records; native primitives:

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.75 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 73 records; native primitives:

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.01 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 8 declarations, 90 records; native primitives:

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: 3.05 ms · instructions: 2.6 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 10 declarations, 98 records; native primitives:

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: 2.90 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 1 declarations, 9 records; native primitives:

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: 2.73 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 26 records; native primitives:

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: 2.68 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 12 records; native primitives:

036_empty

Test: tutorial/036_empty · Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.15 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 20 records; native primitives:

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: 2.73 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 37 records; native primitives:

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.69 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 65 records; native primitives:

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: 2.67 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 57 records; native primitives:

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.80 ms · instructions: 2.5 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 76 records; native primitives:

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.62 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 75 records; native primitives:

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: 2.68 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 31 records; native primitives:

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: 2.63 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 62 records; native primitives:

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: 2.83 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 61 records; native primitives:

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: 2.82 ms · instructions: 3.0 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 296 records; native primitives:

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: 2.58 ms · instructions: 2.4 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductBadNonSort': type expected, found fun (x0 : Sort (1)) => fun (x1 : Sort (1)) => x0
  at export line 20

047_inductBadNonSort2

Test: tutorial/047_inductBadNonSort2 · Expected: ✋ reject · Size: 598 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 3.44 ms · instructions: 2.4 M · max rss memory: 4.0 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductBadNonSort2': type expected, found aType
  at export line 8

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: 3.00 ms · instructions: 2.3 M · max rss memory: 3.1 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductLevelParam': duplicate universe level parameter 'u'
  at export line 7

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: 2.53 ms · instructions: 2.3 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductTooFewParams': invalid inductive datatype declaration, incorrect number of parameters
  at export line 6

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: 2.56 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductWrongCtorParams': arg #1 of 'inductWrongCtorParams.mk' does not match inductive datatype parameters
  at export line 16

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: 2.62 ms · instructions: 2.4 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductWrongCtorResParams': invalid return type for 'inductWrongCtorResParams.mk'
  at export line 19

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: 2.33 ms · instructions: 2.4 M · max rss memory: 3.1 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductWrongCtorResLevel': invalid return type for 'inductWrongCtorResLevel.mk'
  at export line 23

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: 2.65 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'inductInIndex': invalid return type for 'inductInIndex.mk'
  at export line 14

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: 2.35 ms · instructions: 2.4 M · max rss memory: 3.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'indNeg': arg #1 of 'indNeg.mk' has a non positive occurrence of the datatypes being declared
  at export line 12

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.70 ms · instructions: 2.5 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 80 records; native primitives:

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: 2.66 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'reduceCtorType': invalid return type for 'reduceCtorType.mk'
  at export line 26

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: 2.62 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'indNegReducible': arg #1 of 'indNegReducible.mk' has a non positive occurrence of the datatypes being declared
  at export line 31

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: 2.76 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 32 records; native primitives:

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: 2.70 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 36 records; native primitives:

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: 2.57 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 38 records; native primitives:

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: 2.70 ms · instructions: 2.4 M · max rss memory: 3.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'typeWithTooHighTypeField': universe level of type_of(arg #1) of 'typeWithTooHighTypeField.mk' is too big for the corresponding inductive datatype
  at export line 11

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: 2.62 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 21 records; native primitives:

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: 2.68 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 53 records; native primitives:

064_twoBoolRec

Test: tutorial/064_twoBoolRec · Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.05 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 78 records; native primitives:

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.72 ms · instructions: 2.5 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 58 records; native primitives:

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.66 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 79 records; native primitives:

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.64 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 78 records; native primitives:

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: 13.9 ms · instructions: 2.5 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 39 records; native primitives:

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: 14.8 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 63 records; native primitives:

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: 2.65 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 61 records; native primitives:

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: 3.03 ms · instructions: 3.2 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 303 records; native primitives:

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: 2.65 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 34 records; native primitives:

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: 2.82 ms · instructions: 2.4 M · max rss memory: 3.1 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'BogusRecursor': the exported 'BogusRecursor.rec' differs from the declaration the kernel derives
  universe parameters differ

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.93 ms · instructions: 2.6 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 66 records; native primitives:

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: 2.67 ms · instructions: 2.7 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 5 declarations, 138 records; native primitives:

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.04 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 97 records; native primitives:

077_sortElimProp2Rec

Test: tutorial/077_sortElimProp2Rec · Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 3.21 ms · instructions: 2.6 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 114 records; native primitives:

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: 2.79 ms · instructions: 2.8 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 199 records; native primitives:

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: 2.85 ms · instructions: 2.8 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 205 records; native primitives:

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: 2.89 ms · instructions: 2.9 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 238 records; native primitives:

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: 2.81 ms · instructions: 3.1 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 335 records; native primitives:

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: 3.04 ms · instructions: 4.3 M · max rss memory: 4.8 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 1006 records; native primitives:

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.73 ms · instructions: 2.5 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 74 records; native primitives:

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: 2.65 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 83 records; native primitives:

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: 2.56 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 83 records; native primitives:

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: 2.77 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 96 records; native primitives:

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.62 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projOutOfRange': invalid projection .3 of 'And'
  at export line 67

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.67 ms · instructions: 2.5 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projNotStruct': invalid projection .1 of 'N'
  at export line 64

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: 2.76 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 143 records; native primitives:

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: 2.74 ms · instructions: 2.7 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projProp2': invalid projection .2 of 'PropStructure'
  at export line 143

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: 2.93 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 143 records; native primitives:

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: 2.73 ms · instructions: 2.7 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projProp4': invalid projection .4 of 'PropStructure'
  at export line 143

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: 2.77 ms · instructions: 2.7 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projProp5': invalid projection .4 of 'PropStructure'
  at export line 148

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: 2.75 ms · instructions: 2.7 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projProp6': invalid projection .6 of 'PropStructure'
  at export line 143

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: 2.74 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 111 records; native primitives:

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: 2.88 ms · instructions: 2.9 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projIndexData': invalid projection .1 of 'PropStructure'
  at export line 226

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: 3.07 ms · instructions: 2.9 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'projIndexData2': invalid projection .2 of 'PropStructure'
  at export line 226

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: 2.81 ms · instructions: 2.8 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 177 records; native primitives:

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: 2.83 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 121 records; native primitives:

100_ruleKbad

Test: tutorial/100_ruleKbad · Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 3.44 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'ruleKbad': declaration type mismatch
  the value has type
    (Eq Bool Bool.true Bool.false) → (Bool) → Eq.refl Bool #0
  but is declared with type
    (Eq Bool Bool.true Bool.false) → (x0 : Bool) → Eq Bool (Eq.rec Bool Bool.true (fun (x1 : Bool) => fun (x2 : Eq Bool Bool.true x1) => Bool) x0 Bool.false #1) x0

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: 2.97 ms · instructions: 3.0 M · max rss memory: 4.7 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'ruleKAcc': declaration type mismatch
  the value has type
    (Sort LevelId(1)) → fun (x0 : (x0 : #0) → #1 → Prop) => fun (x1 : #1) => fun (x2 : Acc #2 x0 x1) => fun (x3 : Bool) => Eq.refl Bool x3
  but is declared with type
    (Sort LevelId(1)) → (x0 : (x0 : #0) → #1 → Prop) → (x1 : #1) → (x2 : Acc #2 x0 x1) → (x3 : Bool) → Eq Bool (Acc.rec #4 x0 (fun (x4 : #4) => fun (x5 : Acc #5 x0 x4) => Bool) (fun (x4 : #4) => fun (x5 : (x5 : #5) → (x6 : x0 x5 x4) → Acc #7 x0 x5) => fun (x6 : (x6 : #6) → (x0 x6 x4) → Bool) => x3) x1 x2) x3

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: 2.78 ms · instructions: 2.5 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 54 records; native primitives:

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: 2.74 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 114 records; native primitives:

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.07 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 100 records; native primitives:

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.16 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'proofIrrelevanceBad': declaration type mismatch
  the value has type
    (Sort LevelId(4)) → fun (x0 : #0) => fun (x1 : #1) => rfl #2 x0
  but is declared with type
    (Sort LevelId(4)) → (x0 : #0) → (x1 : #1) → Eq #2 x0 x1

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: 2.67 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 112 records; native primitives:

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: 2.68 ms · instructions: 2.4 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 39 records; native primitives:

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: 2.97 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 5 declarations, 116 records; native primitives:

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: 2.66 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 109 records; native primitives:

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: 2.71 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 111 records; native primitives:

111_indexedUnitEta

Test: tutorial/111_indexedUnitEta · Expected: ✋ reject · Size: 7.2 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 3.23 ms · instructions: 2.7 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'indexedUnitEta': declaration type mismatch
  the value has type
    (IndexedUnit Bool.true) → fun (x0 : IndexedUnit Bool.true) => Eq.refl (IndexedUnit Bool.true) #1
  but is declared with type
    (IndexedUnit Bool.true) → (x0 : IndexedUnit Bool.true) → Eq (IndexedUnit Bool.true) #1 x0

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: 2.81 ms · instructions: 2.9 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 230 records; native primitives:

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: 2.79 ms · instructions: 2.7 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'indexedStructEta': declaration type mismatch
  the value has type
    (IndexedSingleton Bool.true) → Eq.refl (IndexedSingleton Bool.true) #0
  but is declared with type
    (IndexedSingleton Bool.true) → Eq (IndexedSingleton Bool.true) (IndexedSingleton.mk True.intro) #0

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: 2.76 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 104 records; native primitives:

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: 2.64 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 106 records; native primitives:

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.44 ms · instructions: 2.6 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'funEtaBad': declaration type mismatch
  the value has type
    (Sort LevelId(4)) → fun (x0 : Sort (1)) => fun (x1 : (x1 : #1) → #2) => fun (x2 : (x2 : #2) → x0) => Eq.refl ((x3 : #3) → x0) x2
  but is declared with type
    (Sort LevelId(4)) → (x0 : Sort (1)) → (x1 : (x1 : #1) → #2) → (x2 : (x2 : #2) → x0) → Eq ((x3 : #3) → x0) (fun (x3 : #3) => x2 (x1 x3)) x2

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: 2.44 ms · instructions: 2.5 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'reflOccLeft': arg #1 of 'reflOccLeft.mk' has a non positive occurrence of the datatypes being declared
  at export line 61

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.66 ms · instructions: 2.5 M · max rss memory: 3.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'reflOccInIndex': application type mismatch
  in `reflOccInIndex h3`
  expected type: Sort (1)
  but the argument has type: Nat

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.57 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 88 records; native primitives:

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.61 ms · instructions: 2.6 M · max rss memory: 4.5 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 88 records; native primitives:

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: 2.62 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 3 declarations, 91 records; native primitives:

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: 2.74 ms · instructions: 2.8 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 191 records; native primitives:

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: 2.70 ms · instructions: 2.8 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 2 declarations, 151 records; native primitives:

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: 2.82 ms · instructions: 2.9 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 4 declarations, 243 records; native primitives:

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: 2.95 ms · instructions: 3.0 M · max rss memory: 4.6 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'accRecNoEta': declaration type mismatch
  the value has type
    (Sort LevelId(4)) → fun (x0 : (x0 : #0) → #1 → Prop) => fun (x1 : #1) => fun (x2 : Acc #2 x0 x1) => fun (x3 : Bool) => Eq.refl Bool x3
  but is declared with type
    (Sort LevelId(4)) → (x0 : (x0 : #0) → #1 → Prop) → (x1 : #1) → (x2 : Acc #2 x0 x1) → (x3 : Bool) → Eq Bool (Acc.rec #4 x0 (fun (x4 : #4) => fun (x5 : Acc #5 x0 x4) => Bool) (fun (x4 : #4) => fun (x5 : (x5 : #5) → (x6 : x0 x5 x4) → Acc #7 x0 x5) => fun (x6 : (x6 : #6) → (x0 x6 x4) → Bool) => x3) x1 x2) x3

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: 2.55 ms · instructions: 2.6 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 123 records; native primitives:

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: 2.99 ms · instructions: 2.6 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 124 records; native primitives:

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: 2.71 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 124 records; native primitives:

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: 2.58 ms · instructions: 2.7 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 7 declarations, 141 records; native primitives:

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: 3.00 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 153 records; native primitives:

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: 3.00 ms · instructions: 2.7 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
accepted: 6 declarations, 151 records; native primitives:

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: 2.61 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'dup_defs': 'dup_defs' has already been declared
  at export line 7

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: 2.97 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: 'dup_ind_def' has already been declared
  at export line 27

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: 2.58 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: 'dup_ctor_def.mk' has already been declared
  at export line 27

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: 2.65 ms · instructions: 2.4 M · max rss memory: 4.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: 'dup_rec_def.rec' has already been declared
  at export line 27

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: 2.34 ms · instructions: 2.4 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'misnamed_rec': the inductive block does not declare 'misnamed_rec.rec', which the kernel derives
  at export line 25

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: 2.50 ms · instructions: 2.4 M · max rss memory: 4.4 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'dup_rec_def2': 'dup_rec_def2.rec' has already been declared
  at export line 28

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: 2.58 ms · instructions: 2.4 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'dup_ctor_rec': 'dup_ctor_rec.rec' has already been declared
  at export line 24

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: 13.0 ms · instructions: 2.4 M · max rss memory: 3.2 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'DupConCon': duplicate constructor name 'dup_ind_con_con.mk'
  at export line 34

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: 16.2 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'falseFromUnsafe': invalid declaration, it uses unsafe declaration 'unsafeLoop'
  at export line 22

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: 2.88 ms · instructions: 2.4 M · max rss memory: 4.3 MB · run 2026-11-08 11:08:24 UTC

stderr:
rejected: declaration 'partialLoop': unknown constant 'partialLoop'
  at export line 20