Lean Kernel Arena / con-leche / tutorial

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: 13.0 ms · instructions: 22.7 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (14.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (19.5%)
con-leche: stats: slowest checks: 0.000s definition basicDef (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 12.9 ms · instructions: 22.6 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 1 records, busy 0.000s (0.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.4%)
con-leche: stats: slowest installs: 0.000s quot Quot.ind (#7)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (18.6%)
con-leche: stats: slowest checks: 0.000s definition badDef (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition badDef [at def badDef, fold position 11] (--verified) t=0.0s

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: 12.8 ms · instructions: 22.7 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (21.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s quot Quot (#4); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.4%)
con-leche: stats: slowest checks: 0.000s definition arrowType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.1 ms · instructions: 22.7 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s def dependentType (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.0%)
con-leche: stats: slowest checks: 0.000s definition dependentType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.9 ms · instructions: 22.8 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (15.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s def constType (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (12.5%)
con-leche: stats: slowest checks: 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.9 ms · instructions: 22.9 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (15.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (36.6%)
con-leche: stats: slowest checks: 0.000s definition betaReduction (#12); 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 12.6 ms · instructions: 23.0 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s def constType (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (17.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (33.4%)
con-leche: stats: slowest checks: 0.000s definition betaReduction2 (#12); 0.000s definition constType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 16.3 ms · instructions: 22.9 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (20.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (40.4%)
con-leche: stats: slowest checks: 0.000s definition forallSortWhnf (#12); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.2 ms · instructions: 22.9 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (16.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Empty (#2); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (12.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.9%)
con-leche: stats: slowest checks: 0.000s definition forallSortBad (#12); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at def forallSortBad, fold position 12] (--verified) t=0.0s

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: 14.0 ms · instructions: 22.9 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (20.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (6.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (2.6%)
con-leche: stats: slowest checks: 0.000s definition constType (#11); 0.000s definition nonTypeType (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at def nonTypeType, fold position 12] (--verified) t=0.0s

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: 12.2 ms · instructions: 22.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 4 records, busy 0.000s (1.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at axiom nonTypeAxiom, fold position 12] (--verified) t=0.0s

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: 12.1 ms · instructions: 22.8 M · max rss memory: 20.5 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (14.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (9.7%)
con-leche: stats: slowest checks: 0.000s theorem nonPropThm (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type of theorem nonPropThm is not a proposition [at theorem nonPropThm, fold position 11] (--verified) t=0.0s

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: 20.6 ms · instructions: 22.9 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (14.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s theorem pImpliesP (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (14.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.1%)
con-leche: stats: slowest checks: 0.000s theorem thmProof (#12); 0.000s theorem pImpliesP (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.5 ms · instructions: 22.7 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (14.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (33.9%)
con-leche: stats: slowest checks: 0.000s theorem selfProof (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: unknown constant in value of selfProof [at theorem selfProof, fold position 11] (--verified) t=0.0s

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: 15.4 ms · instructions: 22.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (16.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s axiom Quot.sound (#8); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (32.0%)
con-leche: stats: slowest checks: 0.000s definition levelComp1 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.5 ms · instructions: 22.7 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (16.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (9.7%)
con-leche: stats: slowest checks: 0.000s definition levelComp2 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.4 ms · instructions: 22.7 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (17.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.1%)
con-leche: stats: slowest checks: 0.000s definition levelComp3 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.6 ms · instructions: 23.0 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (15.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s def levelParamF (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (16.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (33.6%)
con-leche: stats: slowest checks: 0.000s definition levelParams (#12); 0.000s definition levelParamF (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 12.3 ms · instructions: 22.6 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 1 records, busy 0.000s (0.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.8%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate universe parameters in tut06_bad01 [at def tut06_bad01, fold position 11] (--verified) t=0.0s

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: 13.8 ms · instructions: 22.6 M · max rss memory: 20.5 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (9.7%)
con-leche: stats: slowest checks: 0.000s definition levelComp4 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.0 ms · instructions: 22.7 M · max rss memory: 22.4 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (18.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0); 0.000s def levelComp5 (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.4%)
con-leche: stats: slowest checks: 0.000s definition levelComp5 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 17.6 ms · instructions: 22.8 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (14.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (28.4%)
con-leche: stats: slowest checks: 0.000s definition imax1 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.8 ms · instructions: 22.8 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (34.5%)
con-leche: stats: slowest checks: 0.000s definition imax2 (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.7 ms · instructions: 22.7 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot.ind (#7); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (30.7%)
con-leche: stats: slowest checks: 0.000s definition levelMaxComm (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.5 ms · instructions: 22.8 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s def levelMaxAssoc (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.5%)
con-leche: stats: slowest checks: 0.000s definition levelMaxAssoc (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.1 ms · instructions: 22.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (14.1%)
con-leche: stats: slowest checks: 0.000s definition levelMaxIdem (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 53.8 ms · instructions: 22.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 10 records, busy 0.000s (6.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (0.8%)
con-leche: stats: slowest installs: 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s quot Quot.ind (#7); 0.000s inductive False (#3); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (15.0%)
con-leche: stats: slowest checks: 0.000s definition levelMaxAbsorb (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.0 ms · instructions: 22.8 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.001s wall, 4 workers + the commit thread, 10 records, busy 0.001s (17.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (22.4%)
con-leche: stats: slowest checks: 0.000s definition inferVar (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.7 ms · instructions: 22.9 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 11 records, busy 0.000s (16.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def defEqLambda (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (41.8%)
con-leche: stats: slowest checks: 0.000s definition defEqLambda (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.6 ms · instructions: 23.8 M · max rss memory: 23.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 18 records, busy 0.000s (19.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def PN (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 4 workers, 7 records, busy 0.000s (25.9%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (31.1%)
con-leche: stats: slowest checks: 0.000s definition PN.lit1 (#15); 0.000s definition PN.succ (#12); 0.000s definition PN.zero (#13); 0.000s definition PN (#11); 0.000s theorem peano1 (#17)
con-leche: stats: peak RSS 0.02 GiB

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: 15.4 ms · instructions: 24.3 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 8 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 19 records, busy 0.001s (18.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 4 workers, 8 records, busy 0.000s (19.7%); tail 0.000s after the last start, 4 busy then, 0.000s worker-time in it (24.7%)
con-leche: stats: slowest checks: 0.000s theorem peano2 (#18); 0.000s definition PN.succ (#12); 0.000s definition PN.zero (#13); 0.000s definition PN (#11); 0.000s definition PN.add (#17)
con-leche: stats: peak RSS 0.02 GiB

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: 14.9 ms · instructions: 24.8 M · max rss memory: 22.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 10 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 21 records, busy 0.000s (16.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 4 workers, 10 records, busy 0.000s (26.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (31.4%)
con-leche: stats: slowest checks: 0.000s theorem peano3 (#20); 0.000s definition PN.lit2 (#16); 0.000s definition PN (#11); 0.000s definition PN.succ (#12); 0.000s definition PN.mul (#19)
con-leche: stats: peak RSS 0.02 GiB

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: 13.2 ms · instructions: 22.7 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 1 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.001s wall, 4 workers + the commit thread, 11 records, busy 0.000s (16.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.0%)
con-leche: stats: slowest checks: 0.000s definition letType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 🚫 declined · exit code 2 · wall time: 14.6 ms · instructions: 22.8 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 4 records, busy 0.000s (1.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Empty (#2); 0.000s inductive Nat (#1); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aDepProp); con-leche does not support such axioms at the moment [at axiom aDepProp, fold position 11] (--verified) t=0.0s

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: 🚫 declined · exit code 2 · wall time: 19.5 ms · instructions: 22.7 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.2%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aProp); con-leche does not support such axioms at the moment [at axiom aProp, fold position 11] (--verified) t=0.0s

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: 16.8 ms · instructions: 22.8 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (20.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def empty (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (14.9%)
con-leche: stats: slowest checks: 0.000s definition empty (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.4 ms · instructions: 22.9 M · max rss memory: 22.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.4%)
con-leche: stats: slowest checks: 0.000s definition boolType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.1 ms · instructions: 23.7 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.001s wall, 4 workers + the commit thread, 7 records, busy 0.001s (18.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.3%)
con-leche: stats: slowest installs: 0.001s inductive TwoBool (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive False (#3); 0.000s inductive Empty (#2)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (18.9%)
con-leche: stats: slowest checks: 0.000s definition twoBool (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.1 ms · instructions: 23.0 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (26.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.9%)
con-leche: stats: slowest installs: 0.000s def andType (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (24.4%)
con-leche: stats: slowest checks: 0.000s definition andType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 20.9 ms · instructions: 24.2 M · max rss memory: 23.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (25.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.2%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (54.8%)
con-leche: stats: slowest checks: 0.000s definition prodType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 12.9 ms · instructions: 24.3 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (28.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (19.1%)
con-leche: stats: slowest checks: 0.000s definition pprodType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.3 ms · instructions: 23.3 M · max rss memory: 21.2 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (21.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.7%)
con-leche: stats: slowest checks: 0.000s definition pUnitType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.3 ms · instructions: 23.0 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def eqType (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (24.4%)
con-leche: stats: slowest checks: 0.000s definition eqType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.7 ms · instructions: 23.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 0 records, busy 0.000s (0.0%)
con-leche: stats: slowest installs: 
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (13.0%)
con-leche: stats: slowest checks: 0.000s definition natDef (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 16.4 ms · instructions: 33.2 M · max rss memory: 20.5 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.002s wall, 4 workers + the commit thread, 15 records, busy 0.002s (26.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.1%)
con-leche: stats: slowest installs: 0.001s inductive RBTree (#13); 0.000s inductive Color (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (19.0%)
con-leche: stats: slowest checks: 0.000s definition rbTreeDef (#14)
con-leche: stats: peak RSS 0.02 GiB

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: 12.0 ms · instructions: 22.7 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 2 records, busy 0.000s (0.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: expected a sort [at inductive inductBadNonSort, fold position 12] (--verified) t=0.0s

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: 13.1 ms · instructions: 22.6 M · max rss memory: 23.1 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 0 records, busy 0.000s (0.0%)
con-leche: stats: slowest installs: 
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aType); con-leche does not support such axioms at the moment [at axiom aType, fold position 11] (--verified) t=0.0s

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: 17.6 ms · instructions: 22.6 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 1 records, busy 0.000s (0.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.9%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate universe parameters in inductLevelParam [at inductive inductLevelParam, fold position 11] (--verified) t=0.0s

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: 14.0 ms · instructions: 22.6 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 1 records, busy 0.000s (0.7%); tail 0.001s after the last start, 1 busy then, 0.000s worker-time in it (0.8%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: number of parameters mismatch [at inductive inductTooFewParams, fold position 11] (--verified) t=0.0s

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: 10.4 ms · instructions: 19.4 M · max rss memory: 18.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor inductWrongCtorParams.rec declares 0 parameters; the block declares 1 (--verified)

051_inductWrongCtorResParams

Test: tutorial/051_inductWrongCtorResParams · Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 10.1 ms · instructions: 19.4 M · max rss memory: 19.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor inductWrongCtorResParams.rec declares 0 parameters; the block declares 2 (--verified)

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: 10.4 ms · instructions: 19.4 M · max rss memory: 18.1 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor inductWrongCtorResLevel.rec declares 0 parameters; the block declares 2 (--verified)

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: 10.5 ms · instructions: 19.3 M · max rss memory: 17.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor inductInIndex.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 20.5 ms · instructions: 19.4 M · max rss memory: 18.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor indNeg.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 15.8 ms · instructions: 24.4 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (26.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive reduceCtorParam (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (11.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (24.7%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 11.1 ms · instructions: 19.4 M · max rss memory: 18.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor reduceCtorType.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 13.0 ms · instructions: 19.4 M · max rss memory: 17.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor indNegReducible.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 12.5 ms · instructions: 23.4 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (22.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PredWithTypeField (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (14.9%)
con-leche: stats: slowest checks: 0.000s definition predWithTypeField (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 13.3 ms · instructions: 23.5 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (29.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (16.9%)
con-leche: stats: slowest installs: 0.000s inductive TypeWithTypeField (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (6.1%)
con-leche: stats: slowest checks: 0.000s definition typeWithTypeField (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.2 ms · instructions: 23.4 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive TypeWithTypeFieldPoly (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.3%)
con-leche: stats: slowest checks: 0.000s definition typeWithTypeFieldPoly (#12)
con-leche: stats: peak RSS 0.02 GiB

061_typeWithTooHighTypeField.mk

Test: tutorial/061_typeWithTooHighTypeField.mk · Expected: ✋ reject · Size: 943 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: ✋ rejected · exit code 1 · wall time: 13.8 ms · instructions: 19.3 M · max rss memory: 17.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor typeWithTooHighTypeField.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 13.1 ms · instructions: 22.9 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 9 records, busy 0.000s (4.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (0.6%)
con-leche: stats: slowest installs: 0.000s def emptyRec (#11); 0.000s inductive Eq (#0); 0.000s inductive Empty (#2); 0.000s axiom Quot.sound (#8); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (29.9%)
con-leche: stats: slowest checks: 0.000s definition emptyRec (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.7 ms · instructions: 23.1 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (30.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (36.2%)
con-leche: stats: slowest installs: 0.000s def boolRec (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (37.5%)
con-leche: stats: slowest checks: 0.000s definition boolRec (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.7 ms · instructions: 23.9 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 9 records, busy 0.001s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.1%)
con-leche: stats: slowest installs: 0.000s inductive TwoBool (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s def twoBoolRec (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (23.8%)
con-leche: stats: slowest checks: 0.000s definition twoBoolRec (#12)
con-leche: stats: peak RSS 0.02 GiB

065_andRec

Test: tutorial/065_andRec · Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 14.9 ms · instructions: 23.1 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (30.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.3%)
con-leche: stats: slowest installs: 0.000s def andRec (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Empty (#2); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (46.4%)
con-leche: stats: slowest checks: 0.000s definition andRec (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.1 ms · instructions: 24.4 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (29.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (17.3%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (17.2%)
con-leche: stats: slowest checks: 0.000s definition prodRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 16.5 ms · instructions: 24.5 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (26.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (40.2%)
con-leche: stats: slowest checks: 0.000s definition pprodRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.9 ms · instructions: 23.4 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (17.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive False (#3)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (28.1%)
con-leche: stats: slowest checks: 0.000s definition punitRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 19.0 ms · instructions: 23.2 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (18.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def eqRec (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (36.5%)
con-leche: stats: slowest checks: 0.000s definition eqRec (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.9 ms · instructions: 23.9 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (15.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive N (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (38.0%)
con-leche: stats: slowest checks: 0.000s definition nRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 22.3 ms · instructions: 34.0 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.002s (29.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.3%)
con-leche: stats: slowest installs: 0.000s inductive RBTree (#13); 0.000s inductive And (#9); 0.000s inductive Color (#11); 0.000s inductive Bool (#10); 0.000s inductive N (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (61.5%)
con-leche: stats: slowest checks: 0.000s definition rbTreeRef (#14)
con-leche: stats: peak RSS 0.02 GiB

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: 14.7 ms · instructions: 23.5 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (18.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive BoolProp (#11); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (19.1%)
con-leche: stats: slowest checks: 0.000s definition boolPropRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 10.5 ms · instructions: 19.4 M · max rss memory: 17.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor BogusRecursor.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 13.4 ms · instructions: 24.5 M · max rss memory: 21.3 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (27.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.3%)
con-leche: stats: slowest installs: 0.000s inductive Exists (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (49.5%)
con-leche: stats: slowest checks: 0.000s definition existsRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.1 ms · instructions: 24.1 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (27.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (35.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s def typeSingletonRecReduction (#13); 0.000s inductive NewSingleton (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (26.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (41.4%)
con-leche: stats: slowest checks: 0.000s definition typeSingletonRecReduction (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.9 ms · instructions: 24.6 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (28.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.1%)
con-leche: stats: slowest installs: 0.001s inductive SortElimProp (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (46.6%)
con-leche: stats: slowest checks: 0.000s definition sortElimPropRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.7 ms · instructions: 25.0 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (18.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive SortElimProp2 (#12); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (23.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (38.3%)
con-leche: stats: slowest checks: 0.000s definition sortElimProp2Rec (#13); 0.000s definition id (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.1 ms · instructions: 24.2 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (29.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (36.1%)
con-leche: stats: slowest installs: 0.000s theorem boolRecEqns (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (53.4%)
con-leche: stats: slowest checks: 0.000s theorem boolRecEqns (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.5 ms · instructions: 25.5 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (27.6%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (15.9%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (72.2%)
con-leche: stats: slowest checks: 0.000s theorem prodRecEqns (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 18.1 ms · instructions: 25.8 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (17.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive N (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (28.6%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (43.2%)
con-leche: stats: slowest checks: 0.000s theorem nRecReduction (#14); 0.000s definition N.add (#12); 0.000s definition id (#13)
con-leche: stats: peak RSS 0.02 GiB

081_listRecReduction

Test: tutorial/081_listRecReduction · Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 16.4 ms · instructions: 28.0 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 16 records, busy 0.001s (17.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive List (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def List.recOn (#12)
con-leche: stats: check pool: 0.000s wall, 4 workers, 4 records, busy 0.000s (24.7%); tail 0.000s after the last start, 3 busy then, 0.000s worker-time in it (32.1%)
con-leche: stats: slowest checks: 0.000s theorem listRecReduction (#15); 0.000s definition myListApped (#13); 0.000s definition List.recOn (#12); 0.000s definition id (#14)
con-leche: stats: peak RSS 0.02 GiB

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: 18.0 ms · instructions: 43.6 M · max rss memory: 23.3 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.002s (24.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.0%)
con-leche: stats: slowest installs: 0.000s inductive RBTree (#13); 0.000s inductive Color (#11); 0.000s inductive And (#9); 0.000s inductive N (#12); 0.000s inductive Bool (#10)
con-leche: stats: check pool: 0.001s wall, 3 workers, 3 records, busy 0.001s (30.0%); tail 0.001s after the last start, 2 busy then, 0.001s worker-time in it (32.3%)
con-leche: stats: slowest checks: 0.000s theorem RBTree.id_spec (#16); 0.000s definition RBTree.id (#14); 0.000s definition id (#15)
con-leche: stats: peak RSS 0.02 GiB

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: 18.6 ms · instructions: 23.2 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.002s (31.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.0%)
con-leche: stats: slowest installs: 0.000s theorem And.left (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (17.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.6%)
con-leche: stats: slowest checks: 0.000s theorem And.left (#11); 0.000s theorem And.right (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.0 ms · instructions: 24.5 M · max rss memory: 21.2 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (26.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Prod (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (68.8%)
con-leche: stats: slowest checks: 0.000s definition Prod.fst (#12); 0.000s definition Prod.snd (#13)
con-leche: stats: peak RSS 0.02 GiB

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: 16.8 ms · instructions: 24.6 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (25.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive PProd (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (10.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.7%)
con-leche: stats: slowest checks: 0.000s definition PProd.fst (#12); 0.000s definition PProd.snd (#13)
con-leche: stats: peak RSS 0.02 GiB

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: 13.0 ms · instructions: 24.9 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (16.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PSigma (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def PSigma.fst (#12)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (35.7%)
con-leche: stats: slowest checks: 0.000s definition PSigma.snd (#13); 0.000s definition PSigma.fst (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.7 ms · instructions: 23.0 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.001s wall, 4 workers + the commit thread, 8 records, busy 0.001s (27.1%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (13.9%)
con-leche: stats: slowest installs: 0.000s def projOutOfRange (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (36.1%)
con-leche: stats: slowest checks: 0.000s definition projOutOfRange (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection index out of range [at def projOutOfRange, fold position 11] (--verified) t=0.0s

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: 15.7 ms · instructions: 23.9 M · max rss memory: 20.5 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 11 records, busy 0.000s (11.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.6%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s axiom Quot.sound (#8)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (20.4%)
con-leche: stats: slowest checks: 0.000s definition projNotStruct (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: not a structure-like type, or no such field [at def projNotStruct, fold position 12] (--verified) t=0.0s

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: 16.1 ms · instructions: 25.4 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (20.4%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (142.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive PUnit (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (8.2%)
con-leche: stats: slowest checks: 0.000s definition projProp1 (#13)
con-leche: stats: peak RSS 0.02 GiB

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: 14.7 ms · instructions: 25.4 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (2 still running, not counted): 0.000s wall, 4 workers + the commit thread, 9 records, busy 0.001s (24.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (17.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (23.5%)
con-leche: stats: slowest checks: 0.000s definition projProp2 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp2, fold position 13] (--verified) t=0.0s

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: 16.6 ms · instructions: 25.5 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (11.9%)
con-leche: stats: slowest checks: 0.000s definition projProp3 (#13)
con-leche: stats: peak RSS 0.02 GiB

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: 15.8 ms · instructions: 25.4 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (3 still running, not counted): 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (18.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive PUnit (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (22.9%)
con-leche: stats: slowest checks: 0.000s definition projProp4 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp4, fold position 13] (--verified) t=0.0s

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: 15.4 ms · instructions: 25.5 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (29.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (35.3%)
con-leche: stats: slowest checks: 0.000s definition projProp5 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp5, fold position 13] (--verified) t=0.0s

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: 13.9 ms · instructions: 25.5 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (28.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.7%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#12); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (9.2%)
con-leche: stats: slowest checks: 0.000s definition projProp6 (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection from a propositional structure must be a proposition [at def projProp6, fold position 13] (--verified) t=0.0s

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: 13.7 ms · instructions: 25.5 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (29.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.6%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive ProjDataIndex (#13); 0.000s inductive Bool (#10); 0.000s inductive True (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (28.0%)
con-leche: stats: slowest checks: 0.000s definition projDataIndexRec (#14)
con-leche: stats: peak RSS 0.02 GiB

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: 15.0 ms · instructions: 28.0 M · max rss memory: 22.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.002s (30.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (7.4%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#15); 0.000s inductive Bool (#10); 0.000s inductive True (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (34.0%)
con-leche: stats: slowest checks: 0.000s definition projIndexData (#16)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: invalid projection: the node names another structure [at def projIndexData, fold position 16] (--verified) t=0.0s

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: 17.6 ms · instructions: 27.9 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 17 records, busy 0.002s (28.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.6%)
con-leche: stats: slowest installs: 0.000s inductive N (#11); 0.000s inductive And (#9); 0.000s inductive PropStructure (#15); 0.000s inductive Bool (#10); 0.000s inductive ProjDataIndex (#13)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (16.2%)
con-leche: stats: slowest checks: 0.000s definition projIndexData2 (#16)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: projection index out of range [at def projIndexData2, fold position 16] (--verified) t=0.0s

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: 14.4 ms · instructions: 25.2 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.001s (33.0%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (34.4%)
con-leche: stats: slowest installs: 0.000s inductive Prod (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def projRed (#14); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (25.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (40.8%)
con-leche: stats: slowest checks: 0.000s definition projRed (#14); 0.000s definition rfl (#13); 0.000s definition Prod.snd (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.1 ms · instructions: 23.5 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (8.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s theorem ruleK (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (63.5%)
con-leche: stats: slowest checks: 0.000s theorem ruleK (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.6 ms · instructions: 23.7 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.001s (34.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (34.4%)
con-leche: stats: slowest installs: 0.000s theorem ruleKbad (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (65.1%)
con-leche: stats: slowest checks: 0.000s theorem ruleKbad (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem ruleKbad [at theorem ruleKbad, fold position 11] (--verified) t=0.0s

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: 14.7 ms · instructions: 27.0 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (18.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.3%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem ruleKAcc (#12)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (50.6%)
con-leche: stats: slowest checks: 0.000s theorem ruleKAcc (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem ruleKAcc [at theorem ruleKAcc, fold position 12] (--verified) t=0.0s

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: 15.3 ms · instructions: 22.9 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.0%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def aNatLit (#11); 0.000s inductive Nat (#1); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (12.7%)
con-leche: stats: slowest checks: 0.000s definition aNatLit (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.8 ms · instructions: 23.3 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (5.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (34.6%)
con-leche: stats: slowest checks: 0.000s theorem natLitEq (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.9 ms · instructions: 23.3 M · max rss memory: 21.2 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (16.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (2.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def rfl (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.7%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (43.9%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevance (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 21.5 ms · instructions: 23.4 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (16.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (2.9%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Eq (#0); 0.000s inductive Bool (#10); 0.000s inductive Nat (#1); 0.000s def rfl (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (24.5%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (60.3%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevanceBad (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition proofIrrelevanceBad [at def proofIrrelevanceBad, fold position 12] (--verified) t=0.0s

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: 14.8 ms · instructions: 23.6 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.000s (15.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (13.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (24.0%)
con-leche: stats: slowest checks: 0.000s definition proofIrrelevanceWhnf (#13); 0.000s definition id (#11); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 🚫 declined · exit code 2 · wall time: 12.7 ms · instructions: 23.0 M · max rss memory: 20.7 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 4 records, busy 0.000s (1.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s inductive False (#3)
con-leche: stats: peak RSS 0.02 GiB
con-leche: not implemented yet: non-standard axiom (aType); con-leche does not support such axioms at the moment [at axiom aType, fold position 11] (--verified) t=0.0s

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: 17.5 ms · instructions: 24.0 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 5 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 15 records, busy 0.000s (25.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.1%)
con-leche: stats: slowest installs: 0.000s inductive PUnit (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (14.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (25.9%)
con-leche: stats: slowest checks: 0.000s definition unitEta1 (#14); 0.000s definition rfl (#13); 0.000s definition Unit (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 16.9 ms · instructions: 23.9 M · max rss memory: 21.3 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (22.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive PUnit (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (22.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (55.3%)
con-leche: stats: slowest checks: 0.000s definition unitEta2 (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.6 ms · instructions: 23.8 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.000s (17.1%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (3.1%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Eq (#0); 0.000s inductive Bool (#10); 0.000s inductive PUnit (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (26.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (40.6%)
con-leche: stats: slowest checks: 0.000s definition unitEta3 (#13); 0.000s definition rfl (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 14.3 ms · instructions: 24.1 M · max rss memory: 23.1 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.002s (32.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.3%)
con-leche: stats: slowest installs: 0.001s inductive IndexedUnit (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot.ind (#7); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (68.4%)
con-leche: stats: slowest checks: 0.000s definition indexedUnitEta (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition indexedUnitEta [at def indexedUnitEta, fold position 12] (--verified) t=0.0s

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: 16.1 ms · instructions: 26.0 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 16 records, busy 0.001s (24.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (15.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Prod (#11); 0.000s inductive Bool (#10); 0.000s def structEta (#15); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 4 workers, 4 records, busy 0.000s (15.8%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (24.0%)
con-leche: stats: slowest checks: 0.000s definition structEta (#15); 0.000s definition Prod.snd (#13); 0.000s definition Prod.fst (#12); 0.000s definition rfl (#14)
con-leche: stats: peak RSS 0.02 GiB

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: 31.4 ms · instructions: 24.7 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (3 still running, not counted): 0.003s wall, 4 workers + the commit thread, 9 records, busy 0.000s (1.2%); tail 0.002s after the last start, 1 busy then, 0.000s worker-time in it (0.0%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s quot Quot.lift (#6)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (48.0%)
con-leche: stats: slowest checks: 0.000s definition indexedStructEta (#13)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in definition indexedStructEta [at def indexedStructEta, fold position 13] (--verified) t=0.0s

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: 16.5 ms · instructions: 23.5 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (17.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def rfl (#11); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (27.2%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (39.4%)
con-leche: stats: slowest checks: 0.000s theorem funEta (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.2 ms · instructions: 23.6 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (17.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def rfl (#11); 0.000s inductive Eq (#0); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (38.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (69.4%)
con-leche: stats: slowest checks: 0.000s theorem funEtaDep (#12); 0.000s definition rfl (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.4 ms · instructions: 23.4 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.7%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.7%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem funEtaBad (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (62.9%)
con-leche: stats: slowest checks: 0.000s theorem funEtaBad (#11)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem funEtaBad [at theorem funEtaBad, fold position 11] (--verified) t=0.0s

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: 12.9 ms · instructions: 19.7 M · max rss memory: 19.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: recursor reflOccLeft.rec declares 0 motives; the block has 1 inductive types (--verified)

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: 9.27 ms · instructions: 19.7 M · max rss memory: 19.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: constructor reflOccInIndex.mk declares 1 fields at 0 parameters; its type has 2 binders (--verified)

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: 12.8 ms · instructions: 24.7 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool (1 still running, not counted): 0.000s wall, 4 workers + the commit thread, 14 records, busy 0.001s (26.3%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (30.3%)
con-leche: stats: slowest installs: 0.000s inductive reduceCtorParamRefl (#13); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (8.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (6.6%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 16.8 ms · instructions: 24.7 M · max rss memory: 20.6 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 14 records, busy 0.001s (17.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (18.6%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive reduceCtorParamRefl2 (#13); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def id (#11)
con-leche: stats: check pool: 0.000s wall, 2 workers, 2 records, busy 0.000s (4.5%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.6%)
con-leche: stats: slowest checks: 0.000s definition id (#11); 0.000s definition constType (#12)
con-leche: stats: peak RSS 0.02 GiB

121_rTreeRec

Test: tutorial/121_rTreeRec · Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source · 📖 Tutorial

Result: 👍 accepted · exit code 0 · wall time: 14.5 ms · instructions: 24.5 M · max rss memory: 23.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 3 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.002s (30.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.0%)
con-leche: stats: slowest installs: 0.001s inductive RTree (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (66.7%)
con-leche: stats: slowest checks: 0.000s definition rTreeRec (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.2 ms · instructions: 25.5 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 15 records, busy 0.002s (30.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (12.5%)
con-leche: stats: slowest installs: 0.001s inductive RTree (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 3 workers, 3 records, busy 0.000s (12.9%); tail 0.000s after the last start, 2 busy then, 0.000s worker-time in it (11.9%)
con-leche: stats: slowest checks: 0.000s theorem rtreeRecReduction (#14); 0.000s definition RTree.left (#12); 0.000s definition rfl (#13)
con-leche: stats: peak RSS 0.02 GiB

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: 12.9 ms · instructions: 26.4 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 2 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (31.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.5%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (58.5%)
con-leche: stats: slowest checks: 0.000s definition accRecType (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 15.9 ms · instructions: 27.3 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 4 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.001s (17.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.3%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (73.1%)
con-leche: stats: slowest checks: 0.000s theorem accRecReduction (#12)
con-leche: stats: peak RSS 0.02 GiB

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: 11.3 ms · instructions: 27.0 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 13 records, busy 0.001s (29.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (9.6%)
con-leche: stats: slowest installs: 0.000s inductive Acc (#11); 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (65.2%)
con-leche: stats: slowest checks: 0.000s theorem accRecNoEta (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: type mismatch in theorem accRecNoEta [at theorem accRecNoEta, fold position 12] (--verified) t=0.0s

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: 15.4 ms · instructions: 23.2 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (10.4%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def quotMkType (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.001s wall, 1 worker, 1 records, busy 0.000s (6.3%)
con-leche: stats: slowest checks: 0.000s definition quotMkType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 14.0 ms · instructions: 23.4 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (19.9%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (15.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s def quotIndType (#11); 0.000s quot Quot (#4); 0.000s inductive Eq (#0)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (57.1%)
con-leche: stats: slowest checks: 0.000s definition quotIndType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 15.3 ms · instructions: 23.4 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (15.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (13.5%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s def quotLiftType (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (56.7%)
con-leche: stats: slowest checks: 0.000s definition quotLiftType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 45.0 ms · instructions: 23.4 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 7 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (20.0%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (16.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s def quotSoundType (#11); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot (#4)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (33.8%)
con-leche: stats: slowest checks: 0.000s definition quotSoundType (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 13.3 ms · instructions: 24.0 M · max rss memory: 21.1 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.001s wall, 4 workers + the commit thread, 12 records, busy 0.000s (17.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (19.3%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s quot Quot.ind (#7); 0.000s theorem quotLiftReduction (#11)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (48.5%)
con-leche: stats: slowest checks: 0.000s theorem quotLiftReduction (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 12.3 ms · instructions: 23.8 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stdout:

con-leche: accepted 6 declarations (--verified)

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check 0.0s
con-leche: stats: install pool: 0.000s wall, 4 workers + the commit thread, 12 records, busy 0.000s (14.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (14.2%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive Eq (#0); 0.000s theorem quotIndReduction (#11); 0.000s inductive Nat (#1)
con-leche: stats: check pool: 0.000s wall, 1 worker, 1 records, busy 0.000s (64.7%)
con-leche: stats: slowest checks: 0.000s theorem quotIndReduction (#11)
con-leche: stats: peak RSS 0.02 GiB

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: 12.7 ms · instructions: 22.7 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 5 records, busy 0.000s (1.4%); tail 0.001s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_defs [at def dup_defs, fold position 12] (--verified) t=0.0s

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: 11.6 ms · instructions: 22.8 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.3%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.3%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ind_def [at inductive dup_ind_def, fold position 12] (--verified) t=0.0s

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: 16.3 ms · instructions: 22.8 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 1 records, busy 0.000s (0.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (1.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ctor_def.mk [at inductive dup_ctor_def, fold position 12] (--verified) t=0.0s

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: 12.2 ms · instructions: 23.0 M · max rss memory: 20.8 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 3 records, busy 0.000s (1.8%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.4%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_rec_def.rec [at inductive dup_rec_def, fold position 12] (--verified) t=0.0s

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: 13.7 ms · instructions: 22.9 M · max rss memory: 20.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (3 still running, not counted): 0.001s wall, 4 workers + the commit thread, 13 records, busy 0.000s (15.6%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (24.8%)
con-leche: stats: slowest installs: 0.000s inductive And (#9); 0.000s inductive Bool (#10); 0.000s inductive misnamed_rec (#11); 0.000s inductive Eq (#0); 0.000s def misnamed_rec_user (#12)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: target rec: the block's recursor names are not the generated ones (one T.rec per member) [at inductive misnamed_rec, fold position 11] (--verified) t=0.0s

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: 14.4 ms · instructions: 22.9 M · max rss memory: 20.5 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.001s wall, 4 workers + the commit thread, 9 records, busy 0.000s (2.2%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s quot Quot (#4); 0.000s inductive Nat (#1); 0.000s inductive Empty (#2); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: target rec: the block's recursor names are not the generated ones (one T.rec per member) [at inductive dup_rec_def2, fold position 12] (--verified) t=0.0s

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: 12.4 ms · instructions: 22.9 M · max rss memory: 21.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: stats: phases: parse 0.0s, install 0.0s, check not reached
con-leche: stats: install pool (4 still running, not counted): 0.000s wall, 4 workers + the commit thread, 5 records, busy 0.000s (2.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (0.1%)
con-leche: stats: slowest installs: 0.000s inductive Eq (#0); 0.000s inductive Nat (#1); 0.000s quot Quot (#4); 0.000s inductive Empty (#2); 0.000s quot Quot.mk (#5)
con-leche: stats: peak RSS 0.02 GiB
con-leche: invalid: duplicate declaration dup_ctor_rec.rec [at inductive dup_ctor_rec, fold position 11] (--verified) t=0.0s

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: 10.4 ms · instructions: 19.4 M · max rss memory: 20.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: invalid: duplicate constructor name in an inductive type's ctors (--verified)

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: 9.72 ms · instructions: 19.4 M · max rss memory: 17.9 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: declined: definition with safety "unsafe" (--verified)

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: 9.02 ms · instructions: 19.3 M · max rss memory: 18.0 MB · run 2026-10-24 20:10:08 UTC

stderr:

con-leche: declined: definition with safety "partial" (--verified)