Lean Kernel Arena / tenet / tutorial

Checker "tenet" on the tests of "tutorial"

Checker: tenet · Version: 0.11.3 · 📄 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: 87.8 ms · instructions: 564.6 M · max rss memory: 43.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 90.6 ms · instructions: 596.1 M · max rss memory: 43.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def badDef (0.01s)
    declaration type mismatch for 'badDef'
      expected: Prop
      inferred: Sort 2
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 91.2 ms · instructions: 581.2 M · max rss memory: 43.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 90.9 ms · instructions: 591.3 M · max rss memory: 43.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 93.6 ms · instructions: 595.5 M · max rss memory: 43.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 96.5 ms · instructions: 640.0 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 96.5 ms · instructions: 643.6 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 94.4 ms · instructions: 652.5 M · max rss memory: 43.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 98.1 ms · instructions: 677.2 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def forallSortBad (0.01s)
    type expected, but got
      _fvar.2199023255556
    of type
      _fvar.2199023255555
FAILED: 1 checked, 1 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 97.0 ms · instructions: 631.2 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def nonTypeType (0.01s)
    type expected, but got
      constType
    of type
      Type → Type → Type
FAILED: 1 checked, 1 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 99.4 ms · instructions: 630.0 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL axiom nonTypeAxiom (0.01s)
    type expected, but got
      constType
    of type
      Type → Type → Type
FAILED: 1 checked, 1 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 94.6 ms · instructions: 579.6 M · max rss memory: 43.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm nonPropThm (0.01s)
    type of theorem 'nonPropThm' is not a proposition: Prop
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 97.6 ms · instructions: 622.8 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 93.8 ms · instructions: 542.4 M · max rss memory: 43.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm selfProof (0.00s)
    'selfProof' refers to 'selfProof', which is itself; a declaration may only use constants already in the environment
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 92.4 ms · instructions: 571.0 M · max rss memory: 43.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 97.7 ms · instructions: 572.2 M · max rss memory: 42.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 97.7 ms · instructions: 572.3 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 111 ms · instructions: 658.3 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 96.1 ms · instructions: 561.7 M · max rss memory: 43.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def tut06_bad01 (0.01s)
    failed to add declaration to environment, duplicate universe level parameter: 'u'
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 88.5 ms · instructions: 563.6 M · max rss memory: 43.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 108 ms · instructions: 565.5 M · max rss memory: 43.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 101 ms · instructions: 605.7 M · max rss memory: 43.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 103 ms · instructions: 604.2 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 96.8 ms · instructions: 574.5 M · max rss memory: 43.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 95.3 ms · instructions: 574.9 M · max rss memory: 42.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 110 ms · instructions: 572.4 M · max rss memory: 43.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 130 ms · instructions: 576.1 M · max rss memory: 43.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 105 ms · instructions: 598.1 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 621.2 M · max rss memory: 43.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 107 ms · instructions: 670.8 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 7 constants, 0.1s, 4 jobs

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: 105 ms · instructions: 677.6 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 8 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 107 ms · instructions: 679.6 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 10 checked, 0 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 102 ms · instructions: 597.1 M · max rss memory: 43.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 1 checked, 0 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 106 ms · instructions: 635.9 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 101 ms · instructions: 608.7 M · max rss memory: 43.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 110 ms · instructions: 710.1 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 118 ms · instructions: 753.7 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 763.4 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 120 ms · instructions: 764.2 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 139 ms · instructions: 774.6 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 146 ms · instructions: 775.5 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 150 ms · instructions: 758.7 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 146 ms · instructions: 767.6 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 145 ms · instructions: 769.6 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 785.8 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 14 constants, 0.1s, 4 jobs

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: 119 ms · instructions: 675.4 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductBadNonSort (0.02s)
    type expected, but got
      fun (x : Type) => fun (y : Type) => x
    of type
      fun (x : Type) => fun (y : Type) => x
FAILED: 1 checked, 1 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 137 ms · instructions: 617.2 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductBadNonSort2 (0.02s)
    type expected, but got
      aType
    of type
      aType
FAILED: 1 checked, 1 failed, 0 skipped, 2 constants, 0.1s, 4 jobs

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: 117 ms · instructions: 576.6 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductLevelParam (0.01s)
    failed to add declaration to environment, duplicate universe level parameter: 'u'
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 580.4 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductTooFewParams (0.01s)
    invalid inductive datatype declaration, incorrect number of parameters
FAILED: 0 checked, 1 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 115 ms · instructions: 598.5 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductWrongCtorParams (0.01s)
    invalid occurrence of datatype 'inductWrongCtorParams' being declared: it must be applied to the parameters and universe levels of the mutual declaration
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 585.8 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductWrongCtorResParams (0.01s)
    invalid occurrence of datatype 'inductWrongCtorResParams' being declared: it must be applied to the parameters and universe levels of the mutual declaration
FAILED: 0 checked, 1 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 116 ms · instructions: 592.2 M · max rss memory: 43.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductWrongCtorResLevel (0.01s)
    invalid occurrence of datatype 'inductWrongCtorResLevel' being declared: it must be applied to the parameters and universe levels of the mutual declaration
FAILED: 0 checked, 1 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 677.3 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive inductInIndex (0.02s)
    invalid return type for 'inductInIndex.mk'
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 129 ms · instructions: 659.3 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive indNeg (0.02s)
    arg #1 of 'indNeg.mk' has a non positive occurrence of the datatypes being declared
FAILED: 0 checked, 1 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 136 ms · instructions: 783.1 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 134 ms · instructions: 702.7 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive reduceCtorType (0.02s)
    invalid return type for 'reduceCtorType.mk'
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 129 ms · instructions: 707.3 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive indNegReducible (0.02s)
    arg #1 of 'indNegReducible.mk' has a non positive occurrence of the datatypes being declared
FAILED: 2 checked, 1 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 138 ms · instructions: 754.6 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 140 ms · instructions: 761.6 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 146 ms · instructions: 768.0 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 138 ms · instructions: 653.7 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive typeWithTooHighTypeField (0.02s)
    universe level of type_of(arg #1) of 'typeWithTooHighTypeField.mk' is too big for the corresponding inductive datatype
FAILED: 0 checked, 1 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 127 ms · instructions: 720.0 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 3 constants, 0.1s, 4 jobs

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: 155 ms · instructions: 764.4 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 134 ms · instructions: 774.7 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 141 ms · instructions: 770.5 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 137 ms · instructions: 778.6 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 124 ms · instructions: 777.9 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 127 ms · instructions: 762.8 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 124 ms · instructions: 767.3 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 769.5 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 119 ms · instructions: 786.0 M · max rss memory: 44.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 14 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 748.8 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 127 ms · instructions: 763.4 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive BogusRecursor (0.03s)
    'BogusRecursor.rec': exported universe parameters does not match the kernel's
      exported: []
      kernel:   [u]
FAILED: 2 checked, 1 failed, 0 skipped, 6 constants, 0.1s, 4 jobs

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: 131 ms · instructions: 772.3 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 125 ms · instructions: 783.3 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 5 checked, 0 failed, 0 skipped, 12 constants, 0.1s, 4 jobs

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: 133 ms · instructions: 771.2 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 134 ms · instructions: 787.0 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 9 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 787.3 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 145 ms · instructions: 793.8 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 7 constants, 0.1s, 4 jobs

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: 141 ms · instructions: 798.4 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 13 constants, 0.1s, 4 jobs

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: 135 ms · instructions: 804.3 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 14 constants, 0.1s, 4 jobs

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: 147 ms · instructions: 825.7 M · max rss memory: 45.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 19 constants, 0.1s, 4 jobs

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: 146 ms · instructions: 767.5 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 163 ms · instructions: 780.5 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 139 ms · instructions: 780.5 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 132 ms · instructions: 792.6 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 132 ms · instructions: 789.8 M · max rss memory: 44.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projOutOfRange (0.02s)
    invalid projection
      z.3
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 136 ms · instructions: 791.5 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projNotStruct (0.02s)
    invalid projection
      x.1
FAILED: 1 checked, 1 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 787.1 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

090_projProp2

Test: tutorial/090_projProp2 · Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 127 ms · instructions: 807.4 M · max rss memory: 44.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projProp2 (0.02s)
    invalid projection
      x.2
FAILED: 3 checked, 1 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 119 ms · instructions: 792.6 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 122 ms · instructions: 807.5 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projProp4 (0.02s)
    invalid projection
      x.4
FAILED: 3 checked, 1 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 120 ms · instructions: 806.8 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projProp5 (0.02s)
    invalid projection
      x.4
FAILED: 3 checked, 1 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 125 ms · instructions: 807.2 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projProp6 (0.02s)
    invalid projection
      x.6
FAILED: 3 checked, 1 failed, 0 skipped, 10 constants, 0.1s, 4 jobs

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: 127 ms · instructions: 774.8 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 129 ms · instructions: 817.5 M · max rss memory: 45.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projIndexData (0.00s)
    invalid projection
      x.1
FAILED: 6 checked, 1 failed, 0 skipped, 20 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 817.3 M · max rss memory: 44.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def projIndexData2 (0.00s)
    invalid projection
      x.2
FAILED: 6 checked, 1 failed, 0 skipped, 20 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 801.0 M · max rss memory: 44.4 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 13 constants, 0.1s, 4 jobs

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: 117 ms · instructions: 777.8 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 122 ms · instructions: 802.0 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm ruleKbad (0.02s)
    declaration type mismatch for 'ruleKbad'
      expected: ∀ (h : Eq.{1} Bool Bool.true Bool.false), ∀ (a : Bool), Eq.{1} Bool (Eq.rec.{1, 1} Bool Bool.true (fun (x.«_@».Tutorial.3161876795._hygCtx._hyg.17 : Bool) => fun (x.«_@».Tutorial.3161876795._hygCtx._hyg.19 : Eq.{1} Bool Bool.true x.«_@».Tutorial.3161876795._hygCtx._hyg.17) => Bool) a Bool.false h) a
      inferred: Eq.{1} Bool Bool.true Bool.false → ∀ (a : Bool), Eq.{1} Bool a a
FAILED: 2 checked, 1 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 121 ms · instructions: 821.8 M · max rss memory: 44.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm ruleKAcc (0.03s)
    declaration type mismatch for 'ruleKAcc'
      expected: ∀ (α : Sort u), ∀ (p : α → α → Prop), ∀ (x : α), ∀ (h : Acc.{u} α p x), ∀ (a : Bool), Eq.{1} Bool (Acc.rec.{1, u} α p (fun (x.«_@».Tutorial.4255978773._hygCtx._hyg.22 : α) => fun (x.«_@».Tutorial.4255978773._hygCtx._hyg.24 : Acc.{u} α p x.«_@».Tutorial.4255978773._hygCtx._hyg.22) => Bool) (fun (x.«_@».Tutorial.4255978773._hygCtx._hyg.31 : α) => fun (x.«_@».Tutorial.4255978773._hygCtx._hyg.33 : ∀ (y : α), p y x.«_@».Tutorial.4255978773._hygCtx._hyg.31 → Acc.{u} α p y) => fun (x.«_@».Tutorial.4255978773._hygCtx._hyg.35 : ∀ (y : α), p y x.«_@».Tutorial.4255978773._hygCtx._hyg.31 → Bool) => a) x h) a
      inferred: ∀ (α : Sort u), ∀ (p : α → α → Prop), ∀ (x : α), Acc.{u} α p x → ∀ (a : Bool), Eq.{1} Bool a a
FAILED: 3 checked, 1 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 128 ms · instructions: 804.0 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 118 ms · instructions: 816.8 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 120 ms · instructions: 779.6 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 122 ms · instructions: 805.9 M · max rss memory: 44.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def proofIrrelevanceBad (0.02s)
    declaration type mismatch for 'proofIrrelevanceBad'
      expected: ∀ (p : Type), ∀ (h1 : p), ∀ (h2 : p), Eq.{1} p h1 h2
      inferred: ∀ (p : Type), ∀ (h1 : p), p → Eq.{1} p h1 h1
FAILED: 2 checked, 1 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 109 ms · instructions: 782.8 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 6 constants, 0.1s, 4 jobs

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: 105 ms · instructions: 638.7 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 7 constants, 0.1s, 4 jobs

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: 113 ms · instructions: 786.5 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 5 checked, 0 failed, 0 skipped, 9 constants, 0.1s, 4 jobs

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: 112 ms · instructions: 784.8 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

110_unitEta3

Test: tutorial/110_unitEta3 · Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 112 ms · instructions: 781.8 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 113 ms · instructions: 808.5 M · max rss memory: 44.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def indexedUnitEta (0.02s)
    declaration type mismatch for 'indexedUnitEta'
      expected: ∀ (x : IndexedUnit Bool.true), ∀ (y : IndexedUnit Bool.true), Eq.{1} (IndexedUnit Bool.true) x y
      inferred: ∀ (x : IndexedUnit Bool.true), IndexedUnit Bool.true → Eq.{1} (IndexedUnit Bool.true) x x
FAILED: 3 checked, 1 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 805.6 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 13 constants, 0.1s, 4 jobs

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: 124 ms · instructions: 817.0 M · max rss memory: 44.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def indexedStructEta (0.00s)
    declaration type mismatch for 'indexedStructEta'
      expected: ∀ (x : IndexedSingleton Bool.true), Eq.{1} (IndexedSingleton Bool.true) (IndexedSingleton.mk True.intro) x
      inferred: ∀ (x : IndexedSingleton Bool.true), Eq.{1} (IndexedSingleton Bool.true) x x
FAILED: 4 checked, 1 failed, 0 skipped, 14 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 780.4 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 116 ms · instructions: 779.7 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 129 ms · instructions: 803.8 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm funEtaBad (0.02s)
    declaration type mismatch for 'funEtaBad'
      expected: ∀ (α : Type), ∀ (β : Type), ∀ (g : α → α), ∀ (f : α → β), Eq.{1} (α → β) (fun (x : α) => f (g x)) f
      inferred: ∀ (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 : Type), ∀ (x.«_@».Tutorial.4249243883._hygCtx._hyg.30 : Type), (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.28) → ∀ (f : x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.30), Eq.{1} (x.«_@».Tutorial.4249243883._hygCtx._hyg.28 → x.«_@».Tutorial.4249243883._hygCtx._hyg.30) f f
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 786.6 M · max rss memory: 44.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive reflOccLeft (0.02s)
    arg #1 of 'reflOccLeft.mk' has a non positive occurrence of the datatypes being declared
FAILED: 1 checked, 1 failed, 0 skipped, 7 constants, 0.1s, 4 jobs

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: 127 ms · instructions: 804.0 M · max rss memory: 44.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive reflOccInIndex (0.02s)
    application type mismatch in
      reflOccInIndex x
    argument has type
      Nat
    but function has type
      Type → Type
FAILED: 1 checked, 1 failed, 0 skipped, 7 constants, 0.1s, 4 jobs

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: 120 ms · instructions: 784.2 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 784.4 M · max rss memory: 43.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 5 constants, 0.1s, 4 jobs

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: 118 ms · instructions: 774.8 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 3 checked, 0 failed, 0 skipped, 9 constants, 0.1s, 4 jobs

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: 114 ms · instructions: 795.6 M · max rss memory: 43.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 14 constants, 0.1s, 4 jobs

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: 118 ms · instructions: 779.3 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 2 checked, 0 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 111 ms · instructions: 799.3 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 4 checked, 0 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 129 ms · instructions: 821.7 M · max rss memory: 44.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL thm accRecNoEta (0.02s)
    declaration type mismatch for 'accRecNoEta'
      expected: ∀ {α : Type}, ∀ (r : α → α → Prop), ∀ (a : α), ∀ (h : Acc.{1} α r a), ∀ (p : Bool), Eq.{1} Bool (Acc.rec.{1, 1} α r (fun (x.«_@».Tutorial.4017164079._hygCtx._hyg.22 : α) => fun (x.«_@».Tutorial.4017164079._hygCtx._hyg.24 : Acc.{1} α r x.«_@».Tutorial.4017164079._hygCtx._hyg.22) => Bool) (fun (x.«_@».Tutorial.4017164079._hygCtx._hyg.31 : α) => fun (x.«_@».Tutorial.4017164079._hygCtx._hyg.33 : ∀ (y : α), r y x.«_@».Tutorial.4017164079._hygCtx._hyg.31 → Acc.{1} α r y) => fun (x.«_@».Tutorial.4017164079._hygCtx._hyg.35 : ∀ (y : α), r y x.«_@».Tutorial.4017164079._hygCtx._hyg.31 → Bool) => p) a h) p
      inferred: ∀ (α : Type), ∀ (r : α → α → Prop), ∀ (a : α), Acc.{1} α r a → ∀ (p : Bool), Eq.{1} Bool p p
FAILED: 3 checked, 1 failed, 0 skipped, 11 constants, 0.1s, 4 jobs

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: 130 ms · instructions: 786.7 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 119 ms · instructions: 791.7 M · max rss memory: 44.2 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 130 ms · instructions: 785.2 M · max rss memory: 43.7 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 124 ms · instructions: 789.7 M · max rss memory: 44.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 7 checked, 0 failed, 0 skipped, 9 constants, 0.1s, 4 jobs

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: 123 ms · instructions: 797.5 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 131 ms · instructions: 796.7 M · max rss memory: 44.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
OK: 6 checked, 0 failed, 0 skipped, 8 constants, 0.1s, 4 jobs

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: 107 ms · instructions: 580.4 M · max rss memory: 43.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def dup_defs (0.00s)
    'dup_defs' has already been declared
FAILED: 1 checked, 1 failed, 0 skipped, 1 constants, 0.1s, 4 jobs

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: 96.0 ms · instructions: 592.8 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive dup_ind_def (0.00s)
    'dup_ind_def' has already been declared
FAILED: 1 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 93.6 ms · instructions: 592.7 M · max rss memory: 43.5 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive dup_ctor_def (0.00s)
    'dup_ctor_def' has already been declared
FAILED: 1 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 98.1 ms · instructions: 592.7 M · max rss memory: 43.3 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive dup_rec_def (0.00s)
    'dup_rec_def' has already been declared
FAILED: 1 checked, 1 failed, 0 skipped, 1 constants, 0.0s, 4 jobs

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: 111 ms · instructions: 770.7 M · max rss memory: 44.6 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive misnamed_rec (0.02s)
    unknown constant 'misnamed_rec.not_rec'
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 106 ms · instructions: 652.6 M · max rss memory: 44.0 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive dup_rec_def2 (0.01s)
    'dup_rec_def2.rec' has already been declared
FAILED: 1 checked, 1 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 92.7 ms · instructions: 513.4 M · max rss memory: 43.1 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive dup_ctor_rec (0.00s)
    'dup_ctor_rec' has already been declared
FAILED: 0 checked, 1 failed, 0 skipped, 0 constants, 0.0s, 4 jobs

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: 95.8 ms · instructions: 512.1 M · max rss memory: 42.8 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL inductive DupConCon (0.00s)
    'DupConCon' has already been declared
FAILED: 0 checked, 1 failed, 0 skipped, 0 constants, 0.0s, 4 jobs

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: 112 ms · instructions: 725.4 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def unsafeLoop (0.00s)
    'unsafeLoop' refers to 'unsafeLoop', which is itself; a declaration may only use constants already in the environment
FAIL thm falseFromUnsafe (0.01s)
    invalid declaration, it uses unsafe declaration 'unsafeLoop'
FAILED: 1 checked, 2 failed, 0 skipped, 4 constants, 0.1s, 4 jobs

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: 117 ms · instructions: 725.6 M · max rss memory: 43.9 MB · run 2026-10-24 16:42:18 UTC

stdout:
FAIL def partialLoop (0.00s)
    'partialLoop' refers to 'partialLoop', which is itself; a declaration may only use constants already in the environment
FAIL thm falseFromPartial (0.01s)
    invalid declaration, safe declaration must not contain partial declaration 'partialLoop'
FAILED: 1 checked, 2 failed, 0 skipped, 4 constants, 0.1s, 4 jobs