Lean Kernel Arena / canonical-min / tutorial

Checker "canonical-min" on the tests of "tutorial"

Checker: canonical-min · Version: kernel-arena (0acb45d) · 📄 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: ✋ rejected · exit code 1 · wall time: 927 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 985 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 999 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 960 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 933 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 1 declarations.

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: ✋ rejected · exit code 1 · wall time: 948 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 861 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 2 declarations.

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: ✋ rejected · exit code 1 · wall time: 893 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 🚫 declined · exit code 2 · wall time: 864 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: could not translate forallSortBad: type expected
  x

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: 🚫 declined · exit code 2 · wall time: 873 ms · instructions: 3.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
PANIC at Canonical.toHead Canonical.Util:46:7: unreachable code has been reached
backtrace:
.lake/build/bin/canonical-min-arena(+0x6093c6e) [0x565309e49c6e]
.lake/build/bin/canonical-min-arena(+0x60940fc) [0x565309e4a0fc]
.lake/build/bin/canonical-min-arena(+0x34494) [0x565303dea494]
.lake/build/bin/canonical-min-arena(+0xaecf7) [0x565303e64cf7]
.lake/build/bin/canonical-min-arena(+0x92e67) [0x565303e48e67]
.lake/build/bin/canonical-min-arena(+0xa9fe1) [0x565303e5ffe1]
.lake/build/bin/canonical-min-arena(+0x60abe26) [0x565309e61e26]
.lake/build/bin/canonical-min-arena(+0x831ba) [0x565303e391ba]
.lake/build/bin/canonical-min-arena(+0x60a8df6) [0x565309e5edf6]
.lake/build/bin/canonical-min-arena(+0x1348d78) [0x5653050fed78]
.lake/build/bin/canonical-min-arena(+0x134c13a) [0x56530510213a]
.lake/build/bin/canonical-min-arena(+0x8323f) [0x565303e3923f]
.lake/build/bin/canonical-min-arena(+0xa8bf8) [0x565303e5ebf8]
.lake/build/bin/canonical-min-arena(+0xe2437) [0x565303e98437]
.lake/build/bin/canonical-min-arena(+0xe650e) [0x565303e9c50e]
.lake/build/bin/canonical-min-arena(+0x60a668a) [0x565309e5c68a]
.lake/build/bin/canonical-min-arena(+0x207aa) [0x565303dd67aa]
.lake/build/bin/canonical-min-arena(+0x2168e) [0x565303dd768e]
.lake/build/bin/canonical-min-arena(+0x2454f) [0x565303dda54f]
.lake/build/bin/canonical-min-arena(+0x25025) [0x565303ddb025]
.lake/build/bin/canonical-min-arena(+0x25933) [0x565303ddb933]
.lake/build/bin/canonical-min-arena(+0x1e792) [0x565303dd4792]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x2b285) [0x7f797d220285]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(__libc_start_main+0x88) [0x7f797d220338]
.lake/build/bin/canonical-min-arena(+0x1f895) [0x565303dd5895]
Declined: could not translate nonTypeType: goal ?[anonymous]

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: 👍 accepted · exit code 0 · wall time: 845 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 2 declarations.

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: 838 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 859 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 2 declarations.

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: 🚫 declined · exit code 2 · wall time: 916 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: could not translate selfProof: Unknown constant `selfProof`

015_levelComp1

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

Result: ✋ rejected · exit code 1 · wall time: 860 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 854 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 819 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 825 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 907 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 924 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 879 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 887 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 837 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 832 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 819 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 818 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 831 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 1.05 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 1 declarations.

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: 1.05 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 1 declarations.

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: ✋ rejected · exit code 1 · wall time: 1.08 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 1.06 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 1.06 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 1.02 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 946 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 1.05 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 2 declarations.

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: 1.05 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 3 declarations.

037_boolType

Test: tutorial/037_boolType · Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 1.01 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 🚫 declined · exit code 2 · wall time: 946 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for TwoBool

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: 951 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 960 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 1.01 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 991 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 977 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 🚫 declined · exit code 2 · wall time: 932 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 🚫 declined · exit code 2 · wall time: 930 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for Color

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: 🚫 declined · exit code 2 · wall time: 921 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductBadNonSort

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: 🚫 declined · exit code 2 · wall time: 884 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductBadNonSort2

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: 🚫 declined · exit code 2 · wall time: 892 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductLevelParam

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: 🚫 declined · exit code 2 · wall time: 882 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductTooFewParams

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: 🚫 declined · exit code 2 · wall time: 823 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductWrongCtorParams

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: 🚫 declined · exit code 2 · wall time: 857 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductWrongCtorResParams

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: 🚫 declined · exit code 2 · wall time: 824 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductWrongCtorResLevel

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: 🚫 declined · exit code 2 · wall time: 813 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for inductInIndex

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: 🚫 declined · exit code 2 · wall time: 823 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for indNeg

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: 🚫 declined · exit code 2 · wall time: 853 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reduceCtorParam

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: 🚫 declined · exit code 2 · wall time: 886 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reduceCtorType

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: 🚫 declined · exit code 2 · wall time: 838 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for indNegReducible

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: 🚫 declined · exit code 2 · wall time: 842 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PredWithTypeField

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: 🚫 declined · exit code 2 · wall time: 827 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for TypeWithTypeField

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: 🚫 declined · exit code 2 · wall time: 862 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for TypeWithTypeFieldPoly

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: 🚫 declined · exit code 2 · wall time: 850 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for typeWithTooHighTypeField

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: 818 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 3 declarations.

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: 868 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 🚫 declined · exit code 2 · wall time: 859 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for TwoBool

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: 865 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: ✋ rejected · exit code 1 · wall time: 863 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 845 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 881 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 847 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 🚫 declined · exit code 2 · wall time: 1.08 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 🚫 declined · exit code 2 · wall time: 1.33 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for Color

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: 🚫 declined · exit code 2 · wall time: 1.34 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for BoolProp

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: 🚫 declined · exit code 2 · wall time: 1.33 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for BogusRecursor

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: 1.18 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 🚫 declined · exit code 2 · wall time: 1.11 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for NewSingleton

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: 🚫 declined · exit code 2 · wall time: 1.09 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for SortElimProp

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: 🚫 declined · exit code 2 · wall time: 1.10 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for SortElimProp2

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: ✋ rejected · exit code 1 · wall time: 1.02 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 879 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 7 declarations.

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: 🚫 declined · exit code 2 · wall time: 812 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 803 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 14 declarations.

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: 🚫 declined · exit code 2 · wall time: 800 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for Color

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: 807 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 812 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 794 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 858 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 🚫 declined · exit code 2 · wall time: 965 ms · instructions: 3.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Error: index out of bounds
backtrace:
.lake/build/bin/canonical-min-arena(+0x6093c6e) [0x56328a344c6e]
.lake/build/bin/canonical-min-arena(+0x6094832) [0x56328a345832]
.lake/build/bin/canonical-min-arena(+0x814ff) [0x5632843324ff]
.lake/build/bin/canonical-min-arena(+0x8231d) [0x56328433331d]
.lake/build/bin/canonical-min-arena(+0x92ab3) [0x563284343ab3]
.lake/build/bin/canonical-min-arena(+0x92687) [0x563284343687]
.lake/build/bin/canonical-min-arena(+0x8f4c6) [0x5632843404c6]
.lake/build/bin/canonical-min-arena(+0x60ab50c) [0x56328a35c50c]
.lake/build/bin/canonical-min-arena(+0x845b4) [0x5632843355b4]
.lake/build/bin/canonical-min-arena(+0x60a78bf) [0x56328a3588bf]
.lake/build/bin/canonical-min-arena(+0x134f14c) [0x56328560014c]
.lake/build/bin/canonical-min-arena(+0x134f55f) [0x56328560055f]
.lake/build/bin/canonical-min-arena(+0x84645) [0x563284335645]
.lake/build/bin/canonical-min-arena(+0x92260) [0x563284343260]
.lake/build/bin/canonical-min-arena(+0x8f4c6) [0x5632843404c6]
.lake/build/bin/canonical-min-arena(+0x60ab50c) [0x56328a35c50c]
.lake/build/bin/canonical-min-arena(+0x845b4) [0x5632843355b4]
.lake/build/bin/canonical-min-arena(+0x60a78bf) [0x56328a3588bf]
.lake/build/bin/canonical-min-arena(+0x134f14c) [0x56328560014c]
.lake/build/bin/canonical-min-arena(+0x134f55f) [0x56328560055f]
.lake/build/bin/canonical-min-arena(+0x84645) [0x563284335645]
.lake/build/bin/canonical-min-arena(+0x92260) [0x563284343260]
.lake/build/bin/canonical-min-arena(+0x8f4c6) [0x5632843404c6]
.lake/build/bin/canonical-min-arena(+0x60ab50c) [0x56328a35c50c]
.lake/build/bin/canonical-min-arena(+0x845b4) [0x5632843355b4]
.lake/build/bin/canonical-min-arena(+0x60a78bf) [0x56328a3588bf]
.lake/build/bin/canonical-min-arena(+0x134f14c) [0x56328560014c]
.lake/build/bin/canonical-min-arena(+0x134f55f) [0x56328560055f]
.lake/build/bin/canonical-min-arena(+0x84645) [0x563284335645]
.lake/build/bin/canonical-min-arena(+0x92260) [0x563284343260]
.lake/build/bin/canonical-min-arena(+0xe2552) [0x563284393552]
.lake/build/bin/canonical-min-arena(+0xe650e) [0x56328439750e]
.lake/build/bin/canonical-min-arena(+0x60a668a) [0x56328a35768a]
.lake/build/bin/canonical-min-arena(+0x207aa) [0x5632842d17aa]
.lake/build/bin/canonical-min-arena(+0x2168e) [0x5632842d268e]
.lake/build/bin/canonical-min-arena(+0x2454f) [0x5632842d554f]
.lake/build/bin/canonical-min-arena(+0x25025) [0x5632842d6025]
.lake/build/bin/canonical-min-arena(+0x25933) [0x5632842d6933]
.lake/build/bin/canonical-min-arena(+0x1e792) [0x5632842cf792]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x2b285) [0x7f2d6001b285]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(__libc_start_main+0x88) [0x7f2d6001b338]
.lake/build/bin/canonical-min-arena(+0x1f895) [0x5632842d0895]
Declined: could not translate projOutOfRange: AppBuilder for `mkProjection`, invalid field name '[anonymous]' for
  x
has type
  And x✝¹ x✝

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: 🚫 declined · exit code 2 · wall time: 878 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 🚫 declined · exit code 2 · wall time: 892 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 843 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 832 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 891 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 880 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 858 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for PropStructure

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: 🚫 declined · exit code 2 · wall time: 836 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 🚫 declined · exit code 2 · wall time: 869 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 🚫 declined · exit code 2 · wall time: 907 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for N

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: 854 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 13 declarations.

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: 843 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 861 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 942 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 870 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 855 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: ✋ rejected · exit code 1 · wall time: 866 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 941 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 858 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 852 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 896 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 902 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: ✋ rejected · exit code 1 · wall time: 862 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 🚫 declined · exit code 2 · wall time: 900 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for IndexedUnit

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: ✋ rejected · exit code 1 · wall time: 889 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 🚫 declined · exit code 2 · wall time: 869 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for IndexedSingleton

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: 962 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 868 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 5 declarations.

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: 870 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 🚫 declined · exit code 2 · wall time: 858 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reflOccLeft

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: 🚫 declined · exit code 2 · wall time: 907 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reflOccInIndex

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: 🚫 declined · exit code 2 · wall time: 1.02 s · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reduceCtorParamRefl

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: 🚫 declined · exit code 2 · wall time: 915 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for reduceCtorParamRefl2

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: 🚫 declined · exit code 2 · wall time: 980 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for RTree

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: 🚫 declined · exit code 2 · wall time: 902 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for RTree

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: 951 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 4 declarations.

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: 825 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 11 declarations.

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: 832 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 853 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 851 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 882 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 883 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 9 declarations.

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: 890 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 926 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stdout:
Accepted 8 declarations.

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: 398 ms · instructions: 1.5 G · max rss memory: 798.7 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_defs

133_dup_ind_def

Test: tutorial/133_dup_ind_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 395 ms · instructions: 1.5 G · max rss memory: 798.8 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_ind_def

134_dup_ctor_def

Test: tutorial/134_dup_ctor_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 400 ms · instructions: 1.5 G · max rss memory: 798.8 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_ctor_def.mk

135_dup_rec_def

Test: tutorial/135_dup_rec_def · Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 401 ms · instructions: 1.5 G · max rss memory: 798.9 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_rec_def.rec

136_misnamed_rec_user

Test: tutorial/136_misnamed_rec_user · Expected: ✋ reject · Size: 2.0 KB · Lines: 33 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 🚫 declined · exit code 2 · wall time: 912 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration kind for misnamed_rec

137_dup_rec_def2

Test: tutorial/137_dup_rec_def2 · Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 895 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Rejected.

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: 426 ms · instructions: 1.5 G · max rss memory: 798.8 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_ctor_rec.rec

139_DupConCon

Test: tutorial/139_DupConCon · Expected: ✋ reject · Size: 2.2 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 401 ms · instructions: 1.5 G · max rss memory: 798.7 MB · run 2026-10-24 16:27:15 UTC

stderr:
Invalid export: Duplicate declaration: dup_ind_con_con.mk

140_falseFromUnsafe

Test: tutorial/140_falseFromUnsafe · Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 🚫 declined · exit code 2 · wall time: 868 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration unsafeLoop

141_falseFromPartial

Test: tutorial/141_falseFromPartial · Expected: ✋ reject · Size: 1.3 KB · Lines: 22 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 🚫 declined · exit code 2 · wall time: 868 ms · instructions: 2.3 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC

stderr:
Declined: unsupported declaration partialLoop