nanoda - Lean Kernel Arena

Checker "nanoda"

Version: master (4183202) · 📄 Declaration · 🔗 Source

Nanoda - An alternative Lean 4 kernel implementation in Rust.

This is an independent proof checker that validates Lean 4 exports using a different implementation approach. Features:

Written in Rust for performance
Supports standard Lean 4 axioms (propext, choice, etc.)
Configurable axiom checking policy
Native JSON parsing with string optimizations
Parallel checking using multiple threads (set to 4 threads in the kernel arena)

Useful for cross-validation against the official kernel and testing implementation diversity in the Lean ecosystem.

The nanoda integration in the arena does not distinguish between a rejected proof and other forms of failure, so they are all repoted as “rejected”.

Completeness (rightfully accepted tests)

119/119

Soundness (rightfully rejected tests)

55/55

Declined tests

Test	Expected	Result	⏱️		🧠
bogus1	✋	✋	1 ms		3.1 MB
cedar	👍	👍	1.2 m	(-50%)	889.8 MB	(-42%)
constlevels	✋	✋	1 ms		3.1 MB
cslib	👍	👍	3.4 m	(÷2.1)	2.3 GB	(-37%)
ctor-num-fields	✋	✋	1 ms		3.3 MB
init	👍	👍	35.0 s	(-48%)	403.3 MB	(-26%)
init-prelude	👍	👍	145 ms	(÷2.5)	8.5 MB	(÷8.4)
k-rec-conv	✋	✋	1 ms		3.2 MB
large-elim-param	✋	✋	0 ms		3.1 MB
level-imax-leq	✋	✋	1 ms		3.3 MB
level-imax-normalization	✋	✋	1 ms		3.3 MB
level-index-out-of-order	👍	🚫	0 ms		2.9 MB
mathlib	👍	👍	22.1 m	(-25%)	7.9 GB	(-13%)
nat-rec-k-lie	✋	✋	1 ms		3.2 MB
nat-rec-rules	✋	✋	1 ms		3.3 MB
nested-nonuniform-param	🤷	👍	1 ms		3.2 MB
nested-unused-param	✋	✋	2 ms		3.3 MB
proj-non-structure	✋	✋	1 ms		3.3 MB
proj-of-imax-prop	✋	✋	1 ms		3.5 MB
proj-of-prop	✋	✋	1 ms		3.2 MB
proof-irrel	👍	👍	0 ms		3.2 MB
rec-k-lie	✋	✋	1 ms		3.3 MB
sparse-name-index	👍	🚫	0 ms		3.0 MB
std	👍	👍	55.5 s	(÷2.0)	660.6 MB	(-34%)
perf/ (18 tests)		18	7.3 s	(÷2.7)	2.1 GB
app-lam	👍	👍	3.9 s	(-21%)	2.1 GB	(+48%)
args-before-unfold	👍	👍	4 ms	(÷8.3)	4.2 MB	(÷16)
beta-ladder	👍	👍	1.1 s	(-33%)	607.5 MB	(+22%)
church-numerals	👍	👍	24 ms	(÷2.1)	13.7 MB	(÷5.4)
discarded-argument	👍	👍	33 ms	(÷20)	3.4 MB	(÷19)
discarded-argument-match	👍	👍	101 ms	(÷85)	4.8 MB	(÷14)
folded-constant-first	👍	👍	7 ms	(÷5.8)	4.6 MB	(÷15)
folded-constant-last	👍	👍	7 ms	(÷5.8)	4.6 MB	(÷15)
grind-ring-5	👍	👍	1.4 s	(-38%)	151.6 MB	(-34%)
identical-nesting	👍	👍	1 ms	(÷44)	3.1 MB	(÷21)
irrelevance-before-evaluation	👍	👍	1 ms	(÷34)	3.3 MB	(÷19)
let-ladder	👍	👍	631 ms	(-38%)	306.2 MB	(-3%)
refute-cheap-first	✋	✋	1 ms		3.1 MB
refute-cheap-last	✋	✋	35 ms		3.4 MB
repeated-subproblem	👍	👍	1 ms	(÷34)	3.2 MB	(÷20)
shared-subterm	👍	👍	15 ms	(÷3.9)	6.6 MB	(÷11)
shift-cascade	👍	👍	7 ms	(÷7.1)	4.4 MB	(÷15)
unroll-versus-evaluate	👍	👍	1 ms	(÷21)	3.5 MB	(÷19)
tutorial/ (138 tests)		131	74 ms	(÷51)	3.4 MB
001_basicDef	👍	👍	0 ms		3.1 MB
002_badDef	✋	✋	0 ms		3.0 MB
003_arrowType	👍	👍	0 ms		3.0 MB
004_dependentType	👍	👍	0 ms		3.1 MB
005_constType	👍	👍	0 ms		3.0 MB
006_betaReduction	👍	👍	0 ms		3.1 MB
007_betaReduction2	👍	👍	0 ms		3.2 MB
008_forallSortWhnf	👍	👍	0 ms		3.2 MB
009_forallSortBad	✋	✋	0 ms		3.2 MB
010_nonTypeType	✋	✋	0 ms		3.2 MB
011_nonTypeAxiom	✋	✋	0 ms		3.0 MB
012_nonPropThm	✋	✋	0 ms		3.1 MB
013_levelComp1	👍	👍	0 ms		3.1 MB
014_levelComp2	👍	👍	0 ms		3.0 MB
015_levelComp3	👍	👍	0 ms		3.1 MB
016_levelParams	👍	👍	0 ms		3.0 MB
017_tut06_bad01	✋	✋	0 ms		3.2 MB
018_levelComp4	👍	👍	0 ms		3.1 MB
019_levelComp5	👍	👍	0 ms		3.2 MB
020_imax1	👍	👍	0 ms		3.0 MB
021_imax2	👍	👍	0 ms		3.1 MB
022_levelMaxComm	👍	👍	0 ms		2.9 MB
023_levelMaxAssoc	👍	👍	0 ms		3.0 MB
024_levelMaxIdem	👍	👍	0 ms		3.1 MB
025_levelMaxAbsorb	👍	👍	0 ms		3.1 MB
026_inferVar	👍	👍	0 ms		3.1 MB
027_defEqLambda	👍	👍	0 ms		3.1 MB
028_peano1	👍	👍	0 ms		3.0 MB
029_peano2	👍	👍	1 ms		3.1 MB
030_peano3	👍	👍	1 ms		3.1 MB
031_letType	👍	👍	0 ms		2.9 MB
032_letTypeDep	👍	👍	0 ms		3.1 MB
033_letRed	👍	👍	0 ms		3.1 MB
034_empty	👍	👍	0 ms		3.1 MB
035_boolType	👍	👍	0 ms		3.2 MB
036_twoBool	👍	👍	0 ms		3.1 MB
037_andType	👍	👍	0 ms		3.3 MB
038_prodType	👍	👍	1 ms		3.0 MB
039_pprodType	👍	👍	1 ms		3.0 MB
040_pUnitType	👍	👍	0 ms		3.0 MB
041_eqType	👍	👍	0 ms		3.0 MB
042_natDef	👍	👍	0 ms		3.1 MB
043_rbTreeDef	👍	👍	1 ms		3.1 MB
044_inductBadNonSort	✋	✋	0 ms		3.0 MB
045_inductBadNonSort2	✋	✋	0 ms		3.2 MB
046_inductLevelParam	✋	✋	0 ms		3.3 MB
047_inductTooFewParams	✋	✋	0 ms		3.3 MB
048_inductWrongCtorParams	✋	✋	0 ms		3.2 MB
049_inductWrongCtorResParams	✋	✋	0 ms		3.2 MB
050_inductWrongCtorResLevel	✋	✋	0 ms		3.1 MB
051_inductInIndex	✋	✋	0 ms		3.3 MB
052_indNeg	✋	✋	0 ms		3.1 MB
053_reduceCtorParam.mk	👍	👍	1 ms		3.2 MB
054_reduceCtorType.mk	✋	✋	0 ms		3.1 MB
055_indNegReducible	✋	✋	0 ms		3.2 MB
056_predWithTypeField	👍	👍	0 ms		3.0 MB
057_typeWithTypeField	👍	👍	0 ms		3.1 MB
058_typeWithTypeFieldPoly	👍	👍	0 ms		3.1 MB
059_typeWithTooHighTypeField.mk	✋	✋	0 ms		3.2 MB
060_emptyRec	👍	👍	0 ms		3.1 MB
061_boolRec	👍	👍	0 ms		3.1 MB
062_twoBoolRec	👍	👍	1 ms		3.1 MB
063_andRec	👍	👍	0 ms		3.1 MB
064_prodRec	👍	👍	1 ms		3.1 MB
065_pprodRec	👍	👍	1 ms		3.1 MB
066_punitRec	👍	👍	0 ms		3.1 MB
067_eqRec	👍	👍	0 ms		3.1 MB
068_nRec	👍	👍	0 ms		3.1 MB
069_rbTreeRef	👍	👍	1 ms		3.1 MB
070_boolPropRec	👍	👍	0 ms		3.0 MB
071_BogusRecursor	✋	✋	0 ms		3.3 MB
072_existsRec	👍	👍	1 ms		3.1 MB
073_typeSingletonRecReduction	👍	👍	1 ms		3.0 MB
074_sortElimPropRec	👍	👍	1 ms		3.1 MB
075_sortElimProp2Rec	👍	👍	1 ms		3.1 MB
076_boolRecEqns	👍	👍	1 ms		3.2 MB
077_prodRecEqns	👍	👍	1 ms		3.1 MB
078_nRecReduction	👍	👍	1 ms		3.1 MB
079_listRecReduction	👍	👍	1 ms		3.2 MB
080_RBTree.id_spec	👍	👍	2 ms		3.4 MB
081_And.right	👍	👍	1 ms		3.1 MB
082_Prod.snd	👍	👍	1 ms		3.0 MB
083_PProd.snd	👍	👍	1 ms		3.2 MB
084_PSigma.snd	👍	👍	1 ms		3.0 MB
085_projOutOfRange	✋	✋	1 ms		3.1 MB
086_projNotStruct	✋	✋	1 ms		3.1 MB
087_projProp1	👍	👍	1 ms		3.0 MB
088_projProp2	✋	✋	1 ms		3.1 MB
089_projProp3	👍	👍	1 ms		3.1 MB
090_projProp4	✋	✋	1 ms		3.0 MB
091_projProp5	✋	✋	1 ms		3.1 MB
092_projProp6	✋	✋	1 ms		3.1 MB
093_projDataIndexRec	👍	👍	1 ms		3.1 MB
094_projIndexData	✋	✋	1 ms		2.9 MB
095_projIndexData2	✋	✋	1 ms		3.1 MB
096_projRed	👍	👍	1 ms		3.1 MB
097_ruleK	👍	👍	1 ms		3.1 MB
098_ruleKbad	✋	✋	1 ms		3.3 MB
099_ruleKAcc	✋	✋	1 ms		3.1 MB
100_aNatLit	👍	👍	0 ms		2.9 MB
101_natLitEq	👍	👍	1 ms		3.2 MB
102_proofIrrelevance	👍	👍	1 ms		3.1 MB
103_proofIrrelevanceBad	✋	✋	1 ms		3.3 MB
104_proofIrrelevanceWhnf	👍	👍	1 ms		3.1 MB
105_unitEta1	👍	👍	1 ms		3.0 MB
106_unitEta2	👍	👍	1 ms		3.1 MB
107_unitEta3	👍	👍	1 ms		3.1 MB
108_indexedUnitEta	✋	✋	1 ms		3.2 MB
109_structEta	👍	👍	1 ms		3.3 MB
110_indexedStructEta	✋	✋	1 ms		3.2 MB
111_funEta	👍	👍	1 ms		3.1 MB
112_funEtaDep	👍	👍	1 ms		3.1 MB
113_funEtaBad	✋	✋	1 ms		3.0 MB
114_etaRuleK	✋	✋	1 ms		3.2 MB
115_etaCtor	✋	✋	1 ms		3.1 MB
116_reflOccLeft	✋	✋	1 ms		3.2 MB
117_reflOccInIndex	✋	✋	1 ms		3.1 MB
118_reduceCtorParamRefl.mk	👍	👍	1 ms		3.3 MB
119_reduceCtorParamRefl2.mk	👍	👍	1 ms		3.2 MB
120_rTreeRec	👍	👍	1 ms		3.1 MB
121_rtreeRecReduction	👍	👍	1 ms		3.1 MB
122_accRecType	👍	👍	1 ms		3.1 MB
123_accRecReduction	👍	👍	1 ms		3.1 MB
124_accRecNoEta	✋	✋	1 ms		3.1 MB
125_quotMkType	👍	👍	1 ms		3.0 MB
126_quotIndType	👍	👍	1 ms		3.1 MB
127_quotLiftType	👍	👍	1 ms		3.1 MB
128_quotSoundType	👍	👍	1 ms		3.1 MB
129_quotLiftReduction	👍	👍	1 ms		3.2 MB
130_quotIndReduction	👍	👍	1 ms		3.1 MB
131_dup_defs	✋	✋	0 ms		3.1 MB
132_dup_ind_def	✋	🚫	0 ms		3.1 MB
133_dup_ctor_def	✋	🚫	0 ms		2.9 MB
134_dup_rec_def	✋	🚫	0 ms		3.1 MB
135_misnamed_rec_user	✋	🚫	0 ms		3.0 MB
136_dup_rec_def2	✋	🚫	0 ms		3.0 MB
137_dup_ctor_rec	✋	🚫	0 ms		3.1 MB
138_DupConCon	✋	🚫	0 ms		3.1 MB
undecidability/ (9 tests)		4	18 ms	(÷13)	3.4 MB
alg-conv-trans-acc	🤷	✋	3 ms		3.3 MB
alg-conv-trans-acc-left	👍	👍	3 ms		3.2 MB
alg-conv-trans-acc-right	👍	👍	3 ms		3.3 MB
alg-conv-trans-quot	🤷	✋	1 ms		3.2 MB
alg-conv-trans-quot-left	🤷	✋	1 ms		3.1 MB
alg-conv-trans-quot-left-def	🤷	👍	1 ms		3.2 MB
alg-conv-trans-quot-right	👍	👍	1 ms		3.1 MB
subject-reduction-redex	👍	👍	3 ms		3.4 MB
subject-reduction-reduct	🤷	✋	3 ms		3.3 MB

Detailed results

Test "bogus1"

Expected: ✋ reject · Size: 11.4 KB · Lines: 198 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A clearly bogus proof. Also serves as an example for how to write simple cases.

Test result: ✋ rejected · exit code 1 · wall time: 43 ms · instructions: 4.6 M · max rss memory: 3.1 MB

stderr:

thread 'thread_3' (11511) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11507) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "cedar"

Expected: 👍 accept · Size: 790.9 MB · Lines: 14.6 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Lean formalization of, and proofs about, Cedar.

Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.

This test case exports the whole Cedar module and as such contains even unused parts Init and Batteries.

Test result: 👍 accepted · exit code 0 · wall time: 16.8 s · instructions: 432.6 G · max rss memory: 889.8 MB

Test "constlevels"

Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Regression test for undefined behavior in lazy_delta_reduction_step in the official kernel

In the function lazy_delta_reduction_step, the official kernel expects unfold_definition to always succeed. However, if the constant has an incorrect number of level parameters, it actually fails, which leads to memory corruption in lazy_delta_reduction_step.

This test is to check that the official kernel and also other kernels that closely follow the logic of the official kernel correctly handle this unfolding failure.

The issue in the official kernel was originally reported as https://github.com/leanprover/lean4/issues/10577.

Test result: ✋ rejected · exit code 1 · wall time: 4 ms · instructions: 5.1 M · max rss memory: 3.1 MB

stderr:

thread 'thread_1' (11529) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11527) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "cslib"

Expected: 👍 accept · Size: 2.0 GB · Lines: 37.5 M · lean4export: 3.1.0 · Lean: 4.30.0 · 📄 Declaration · 🔗 Source

The Lean Computer Science Library (CSLib).

Test result: 👍 accepted · exit code 0 · wall time: 56.0 s · instructions: 1.2 T · max rss memory: 2.3 GB

Test "ctor-num-fields"

Expected: ✋ reject · Size: 34.1 KB · Lines: 622 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Proof of False via trusted numFields on a constructor.

Define a wrapper structure S with one field, and lie by saying it has 0 fields, making it look unit-like. Then definitional eta means all inhabitants are equal.

Derive a contradiction from S.mk false = S.mk true.

Test result: ✋ rejected · exit code 1 · wall time: 5 ms · instructions: 8.8 M · max rss memory: 3.3 MB

stderr:

thread 'thread_3' (11557) panicked at src/inductive.rs:1241:25:
assertion failed: old.aux_data_ck(new)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11553) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "init"

Expected: 👍 accept · Size: 309.5 MB · Lines: 6.1 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The Init module export from Lean 4 core.

This test contains the fundamental building blocks of Lean 4, including:

Basic data types (Nat, List, Array, String, etc.)
Core tactics and syntax
Foundational mathematical structures
Essential metaprogramming infrastructure

This is one of the smallest meaningful test cases, making it ideal for initial checker validation and debugging.

Test result: 👍 accepted · exit code 0 · wall time: 8.0 s · instructions: 209.7 G · max rss memory: 403.3 MB

Test "init-prelude"

Expected: 👍 accept · Size: 3.5 MB · Lines: 63.7 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The Init.Prelude module export.

Test result: 👍 accepted · exit code 0 · wall time: 36 ms · instructions: 867.6 M · max rss memory: 8.5 MB

Test "k-rec-conv"

Expected: ✋ reject · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Bogus proof that tests for incorrectly implemented K-like reduction.

fun x => x and fun _ => y are not convertible, but a checker that does treat them as convertible would accept the resulting theorem bad, which is true propositionally, but not definitionally.

Regression test for sokonanoda.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 5.2 M · max rss memory: 3.2 MB

stderr:

thread 'thread_0' (11584) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11583) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "large-elim-param"

Expected: ✋ reject · Size: 3.1 KB · Lines: 48 · 📄 Declaration

Proof of False via incorrect large elimination restriction.

If the check for whether a level is surely not zero is implemented wrong, in particular if it incorrectly returns true for params, we can create a universe-polymorphic

inductive MyBool.{u} : Sort u | tt | ff

where the recursor MyBool.rec.{1,0} can do large elimination of a Prop. Because of proof irrelevance we have tt = ff, so we can derive a contradiction.

Found by Anthony Wang using Aristotle.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.2 M · max rss memory: 3.1 MB

stderr:

Error: missing field `lean` at line 1 column 39

run with `-h` or `--help` for help

Test "level-imax-leq"

Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Proof of False via incorrect universe level comparison for imax.

A correct kernel must reject leq(imax(u,v)+1, imax(u,v)), since at u=0, v=0 this becomes leq(1, 0) which is false. However, a checker that only compares the imax arguments structurally (without accounting for an accumulated successor offset) will incorrectly accept it.

This allows defining a universe-collapsing identity function down.{u,v} : Sort (succ (imax u v)) → Sort (imax u v), which is used to cast between True and False via Bool.rec at Sort (imax 0 0) = Prop.

Nanoda incorrectly accepted this proof until it was fixed.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 3.6 M · max rss memory: 3.3 MB

stderr:

thread 'thread_3' (11601) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'thread_2' (11600) panicked at src/inductive.rs:1279:21:
assertion failed: old_r.aux_data_ck(new_r)

thread 'main' (11597) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "level-imax-normalization"

Expected: ✋ reject · Size: 5.8 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Proof of False via incorrect universe level normalization for imax.

A correct kernel must distinguish imax 0 v from succ(imax 0 v), since at v=0 these evaluate to 0 and 1 respectively. However, a level normalization algorithm that drops an accumulated successor offset when decomposing imax u (param v) will produce identical normal forms for both, causing the equivalence check to incorrectly return true.

This allows defining a universe-collapsing identity function down.{v} : Sort (succ (imax 0 v)) → Sort (imax 0 v), and then myProp : Prop := down.{0} Bool (a Prop that is computationally Bool). Proof irrelevance on myProp equates Bool.true and Bool.false, and Bool.rec maps this into False.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 3.5 M · max rss memory: 3.3 MB

stderr:

thread 'thread_3' (11610) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11606) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "level-index-out-of-order"

Expected: 👍 accept · Size: 328 B · Lines: 6 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Lean4export will create internalization-table references contiguously in order: in references for names, il references for levels, and ie references for expressions all work this way.

However, the spec merely requires that these are integers. It's reasonable for an implementation to assume these are approximately dense (and to treat them as array indices instead of hashtable entries), but a kernel should handle skipped indices or out-of-order indices.

This test checks that the kernel doesn't require internaliation-table references to be presented in ascending order. If the level referenes 2 and 1 were swapped, this would be the expected encoding of axiom foo : Sort 2. This encoding should be equivalent.

Test result: 🚫 declined · exit code 2 · wall time: 3 ms · instructions: 2.2 M · max rss memory: 2.9 MB

stderr:

Declined: Level back-reference mismatch, expected Il(1), found Il(2). Back-refs must be continuous.

Test "mathlib"

Expected: 👍 accept · Size: 5.2 GB · Lines: 100.0 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The complete Mathlib library export.

This test contains all the mathematical definitions, theorems, and proofs from Mathlib, representing the largest and most comprehensive test case in the Lean kernel arena.

Test result: 👍 accepted · exit code 0 · wall time: 4.9 m · instructions: 7.9 T · max rss memory: 7.9 GB

Test "nat-rec-k-lie"

Expected: ✋ reject · Size: 6.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Proof of False via trusted k on Nat.rec.

Lie by claiming Nat.rec is K-like. Then replace the major premise by Nat.zero, but nat literals bypasses K-like reduction, so two reduction rules disagree.

∀ n, g n holds by the first, and g 1 is False by the second.

Test result: ✋ rejected · exit code 1 · wall time: 4 ms · instructions: 3.7 M · max rss memory: 3.2 MB

stderr:

thread 'thread_1' (11657) panicked at src/inductive.rs:1279:21:
assertion failed: old_r.aux_data_ck(new_r)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'thread_0' (11656) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)

thread 'main' (11655) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "nat-rec-rules"

Expected: ✋ reject · Size: 8.1 KB · Lines: 128 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration

Proof of False via incorrect recursor rule validation.

When processing an inductive type declaration, a correct kernel must verify that the generated recursor rules match the ones provided in the export data. A checker that accidentally compares the imported rules against themselves (instead of against independently constructed rules) will accept arbitrary recursor reduction behavior.

This test defines Nat with a wrong Nat.rec succ rule that always returns hzero (ignoring the induction hypothesis). Combined with a nat literal extension that hardcodes correct arithmetic for concrete nat literals but falls back to the wrong Nat.rec rules for symbolic arguments, this creates an inconsistency that yields a proof of False.

Nanoda incorrectly accepted this proof until it was fixed.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 4.1 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (11665) panicked at src/inductive.rs:1279:21:
assertion failed: old_r.aux_data_ck(new_r)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'thread_1' (11666) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)

thread 'main' (11664) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "nested-nonuniform-param"

Expected: 🤷 either · Size: 9.2 KB · Lines: 142 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Checks that a parameter supplied to a nested inductive occurrence really acts as the datatype's parameter, i.e. that it is the parameter itself and does not change between recursive occurrences (as is already enforced for non-nested occurrences).

The inductive E : W → Type has constructor E.mk : (w : W) → L (E ⟨false⟩) → E w, where L (α : Type) is nested. The occurrence E ⟨false⟩ inside the nested L uses the constant ⟨false⟩ in the position of E's parameter, instead of the actual parameter w. That argument is type-correct, so it is not caught by merely type-checking the nested application (leanprover/lean4#14577); a correct checker must also verify that it is the expected parameter.

This particular declaration is not known to yield a proof of False: here L stores no value of type α, so the nested occurrence is phantom and E w is isomorphic to Unit for every w. The variant where L actually stores an α (so recursion would descend into an E ⟨false⟩ while the motive is fixed at E w) is already rejected by the kernel's positivity check ("non valid occurrence"). Since it is not a demonstrated unsoundness, it is not settled whether a checker should accept or reject it, so the expected outcome is either and the test does not count towards completeness or soundness.

Origin: raised by @arthur-adjedj on leanprover/lean4#14577 (https://github.com/leanprover/lean4/pull/14577#issuecomment-5101819377) as a case not covered by that PR's fix; related to leanprover/lean4#14576.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 4.2 M · max rss memory: 3.2 MB

Test "nested-unused-param"

Expected: ✋ reject · Size: 59.2 KB · Lines: 1.1 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Checks that the parameters of a nested inductive application are type-checked even when they do not appear in the auxiliary type generated during nested-inductive compilation.

When an inductive E has a constructor whose type contains a nested application L (E w) b, the elaboration of nested inductives replaces that occurrence with an auxiliary type. The argument b does not occur in the auxiliary declaration, so a checker that only checks the auxiliary type never sees b. A correct checker must still ensure b is well-typed; this test rejects if it is not.

Here b is a malformed projection C.0 (C.0 w) (applying a C projection to a value of the unrelated structure W), disguised by a hash collision. If the parameter is not checked, the bogus projection slips through and the resulting E can be used to build an axiom-free proof of False (boom). The projection is merely the payload; the property under test is that the nested-inductive parameter is checked.

Origin: reported as leanprover/lean4#14576 by @kiranandcode, with the original source recorded by @xrchz (https://github.com/xrchz/collatzlean); fixed in leanprover/lean4#14577.

Test result: ✋ rejected · exit code 1 · wall time: 4 ms · instructions: 14.6 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (11683) panicked at src/tc.rs:471:21:
infer_proj prop
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'thread_2' (11685) panicked at src/tc.rs:471:21:
infer_proj prop

thread 'thread_1' (11684) panicked at src/tc.rs:471:21:
infer_proj prop

thread 'main' (11682) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

thread 'thread_3' (11686) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)

Test "perf/app-lam"

Expected: 👍 accept · Size: 1.2 MB · Lines: 28.6 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A synthetically generated term with n levels of alternating applications and lambdas, with DAG sharing.

At each level, a constant is applied to two identical lambda arguments. The export format records these as a single shared expression (DAG). Each lambda body grows with the nesting depth, referencing all enclosing binders.

This tests two aspects of checker performance:

Infer cache: Since both arguments at each level are the same expression, a checker without an infer cache re-infers the type of each shared subterm, doubling work at every level — O(2ⁿ) total.

Substitution cost: Even with a cache, type-inferring each lambda requires substituting into its body (size O(n)) at each of the n levels, giving O(n²) total. Whether this cost arises depends on the checker's binder representation.

Test result: 👍 accepted · exit code 0 · wall time: 8.4 s · instructions: 23.3 G · max rss memory: 2.1 GB

Test "perf/args-before-unfold"

Expected: 👍 accept · Size: 44.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

count #n      and      count (N.add #(n-1) #1)

where #k is the numeral with k successors, and count #k evaluates to #k in Θ(k²) reductions.

N.add #(n-1) #1 reduces to #n in n steps, so the two arguments agree for Θ(n), and the applications agree with them without count ever being unfolded. Evaluating both applications costs Θ(n²). The test asks whether a checker tries the arguments of a shared head constant before unfolding it.

N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 5 ms · instructions: 26.3 M · max rss memory: 4.2 MB

Test "perf/beta-ladder"

Expected: 👍 accept · Size: 450.2 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check reduces

(fun x₁ => … (fun xₙ => x₁ + (x₂ + (… + (xₙ + 0)))) 0 …) 0

to 0, through n beta redexes over a body that reads every binder.

Reducing the ladder takes n beta steps whatever a checker does, so the test is what one step costs. Substituting into the body on entry to binder k copies the n − k redexes still below it, and those copies sum to Θ(n²). Carrying the substitution in an environment leaves the body untouched, for Θ(n).

N=2000 in the Lean source.

Test result: 👍 accepted · exit code 0 · wall time: 1.8 s · instructions: 6.8 G · max rss memory: 607.5 MB

Test "perf/church-numerals"

Expected: 👍 accept · Size: 9.6 KB · Lines: 227 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

cmul (cnum n) (cnum (n+1))      and      cmul (cnum (n+1)) (cnum n)

where cnum k is the Church numeral fun X s z => s (s (... z)) and cmul a b iterates b as many times as a counts.

Both sides have the normal form with n(n+1) applications of the bound s. Unfolding cmul on the left leaves cnum n X (cnum (n+1) X s), where each of the n occurrences of the bound function copies the redex cnum (n+1) X s, so the normal form takes n(n+1) beta steps and shares nothing. No other delta step is available, so the Θ(n²) measured is beta reduction under binders and little else.

N=120 in the Lean source, giving a reduction depth of 14520. From the conv_eval benchmark of András Kovács' smalltt.

Test result: 👍 accepted · exit code 0 · wall time: 16 ms · instructions: 142.8 M · max rss memory: 13.7 MB

Test "perf/discarded-argument"

Expected: 👍 accept · Size: 15.9 KB · Lines: 367 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

dropArg (count #n)      and      dropArg (count #(n+1))

where count #k evaluates to the numeral #k in Θ(k²) reductions, and dropArg maps every numeral to N.O.

Unfolding dropArg leaves N.O against N.O, for Θ(1). Comparing the arguments first evaluates two numerals of different value, for Θ(n²), and then throws that answer away. The test asks whether a checker unfolds a constant before looking at an argument the constant never uses.

N=200 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 12 ms · instructions: 198.9 M · max rss memory: 3.4 MB

Test "perf/discarded-argument-match"

Expected: 👍 accept · Size: 28.6 KB · Lines: 596 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

discarded-argument.lean with count and N.add written by structural recursion, so the declaration to check is the same

dropArg (count #n)      and      dropArg (count #(n+1))

over definitions that unfold through brecOn rather than through N.rec.

brecOn reduces via the course-of-values table N.below #k = m #(k-1) ×' (m #(k-2) ×' (… ×' PUnit)), a k-deep tuple holding the result at every predecessor. The compiled count reads only x.1, so the rest of the table is built and never read, and typing each projection forces N.below to the depth of that projection.

N=200 in the Lean source, matching its pair.

Test result: 👍 accepted · exit code 0 · wall time: 33 ms · instructions: 606.9 M · max rss memory: 4.8 MB

Test "perf/folded-constant-first"

Expected: 👍 accept · Size: 52.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

tagged (count #n)      and      (false, count #n)

where tagged m = (isZero m, m), so unfolding the left side leaves the same application count #n in both components, forced by isZero in one and plain in the other.

The plain occurrences are identical, for Θ(1); the forced one evaluates count #n once. The order matters for a checker that leaves a constant unfolded once it reduces it: reducing the forced component first replaces count #n by its value on one side, and the plain comparison then faces a folded application against an evaluated one. Here the forcing component comes first; folded-constant-last.lean swaps them, and the ratio between the two files is what that costs.

N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §10, where the two orders cost Rocq 3 × 10⁻⁵ s and 0.078 s.

Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 41.8 M · max rss memory: 4.6 MB

Test "perf/folded-constant-last"

Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

tagged (count #n)      and      (count #n, false)

where tagged m = (m, isZero m): folded-constant-first.lean with the components swapped, so the plain occurrences of count #n are compared before anything forces the application.

N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 41.8 M · max rss memory: 4.6 MB

Test "perf/grind-ring-5"

Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A grind tactic test from the Lean 4 test suite.

This produces a theorem with a rather large proof term that needs fast reduction.

Test result: 👍 accepted · exit code 0 · wall time: 626 ms · instructions: 8.4 G · max rss memory: 151.6 MB

Test "perf/identical-nesting"

Expected: 👍 accept · Size: 8.7 KB · Lines: 172 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

f4 (f4 (... (f4 N.O) ...))      and      f4 (f4 (... (f4 N.O) ...))

n applications of f4 on each side, the same term twice, where f0 is the identity on N and each of f1, f2, f3, f4 applies its predecessor twice, so the nesting expands into 16n applications of f0.

The test asks whether a checker compares the two sides before it starts unfolding, which answers in Θ(n). Unfolding one side at a time offers 16n applications to choose from per side, and the reachable pairs of partially unfolded sides grow exponentially in n.

N=30 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 3.8 M · max rss memory: 3.1 MB

Test "perf/irrelevance-before-evaluation"

Expected: 👍 accept · Size: 17.5 KB · Lines: 389 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check is

slowTriv (count #n) = True.intro

proved by Eq.refl, where slowTriv m : True recurses over m, so forcing it to a constructor evaluates the numeral in Θ(n²) reductions.

Checking compares the two proofs as arguments of Eq, whose head is rigid: nothing can be unfolded instead. Proof irrelevance settles the proofs by their type for Θ(1); evaluating the left one to a constructor costs Θ(n²) and yields the answer irrelevance already gave. The test asks whether a checker consults proof irrelevance before it reduces.

N=200 in the Lean source.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 5.1 M · max rss memory: 3.3 MB

Test "perf/let-ladder"

Expected: 👍 accept · Size: 457.3 KB · Lines: 10.4 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check has type Nat and value

let x₃ := 0; x₃ + (let x₂ := 0; x₂ + (let x₁ := 0; x₁ + (x₃ + (x₂ + (x₁ + 0)))))

shown at n=3: n let bindings, each separated from the next by an addition, over an innermost sum that names every binding.

Substituting a binding into the body before checking it traverses O(n) nodes at each of the n bindings, for Θ(n²) in time and in allocated nodes. Recording the binding and reading it where the body names it costs O(1) per binding, for Θ(n).

The additions are what keep the bindings apart: a run of adjacent lets could be opened by a single substitution; not so here. Nat.add is the only application head, so no beta reduction is involved.

N=2000 in the Lean source.

Test result: 👍 accepted · exit code 0 · wall time: 751 ms · instructions: 3.8 G · max rss memory: 306.2 MB

Test "perf/refute-cheap-first"

Expected: ✋ reject · Size: 20.7 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check claims

(false, count #n) = (true, count #(n+1))

and must be rejected. Both sides are constructor applications, so comparing components is the only route, and either component refutes on its own: false against true for Θ(1), the numerals for Θ(n²) (count #k evaluates to #k in Θ(k²) reductions). The test asks in which order a checker visits the components. refute-cheap-last.lean swaps them, and the ratio between the two files is what that order costs.

N=200 in the Lean source. From Courant and Leroy, POPL 2026, §10, where the two orders cost Rocq 4 × 10⁻⁶ s and 0.61 s.

Test result: ✋ rejected · exit code 1 · wall time: 4 ms · instructions: 6.0 M · max rss memory: 3.1 MB

stderr:

thread 'thread_3' (11807) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11803) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "perf/refute-cheap-last"

Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check claims

(count #n, false) = (count #(n+1), true)

and must be rejected: refute-cheap-first.lean with the components swapped, so the cheap refutation sits behind the expensive one for a checker that visits components left to right.

N=200 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: ✋ rejected · exit code 1 · wall time: 12 ms · instructions: 210.0 M · max rss memory: 3.4 MB

stderr:

thread 'thread_0' (11813) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11812) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "perf/repeated-subproblem"

Expected: 👍 accept · Size: 11.4 KB · Lines: 214 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

perfect #n leaf      and      perfect #(n-1) (node leaf leaf)

where perfect #k t builds the perfect binary tree of depth k with leaves t, in k steps that each duplicate the tree so far into both arguments of Tr.node.

Both sides reduce to the perfect tree of depth n. Descending them meets Tr.node u u against Tr.node v v at every level, where both argument positions pose the same subproblem, so the recursion reaches 2^n pairs of nodes of which n are distinct. The test asks whether a checker records the pairs it has proved convertible: Θ(n) if it does, Θ(2ⁿ) if not.

N=20 in the Lean source, stepped up by one rather than doubled. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 5.1 M · max rss memory: 3.2 MB

Test "perf/shared-subterm"

Expected: 👍 accept · Size: 50.1 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

ldepth (perfect #n leaf)      and      ldepth2 (perfect #n leaf)

where perfect #n leaf builds the perfect binary tree of depth n in n steps that each duplicate the tree so far, and ldepth and ldepth2 both return the length of the leftmost path.

The head constants differ, so both sides are evaluated, and neither traversal looks beyond the leftmost path: ldepth walks n nodes for Θ(n), ldepth2 folds n additions over growing numerals for Θ(n²). The test asks whether a checker consumes the tree through its representation, for Θ(n²), or expands it into the 2ⁿ nodes of its normal form.

N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §10.

Test result: 👍 accepted · exit code 0 · wall time: 10 ms · instructions: 90.4 M · max rss memory: 6.6 MB

Test "perf/shift-cascade"

Expected: 👍 accept · Size: 256.3 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Stress test for cascading substitution overhead in kernel let processing.

N nested let bindings inside a lambda, where each value references the outer lambda parameter and the previous binding:

fun (a : Nat → Nat) => let f₁ := fun x => a x let f₂ := fun x => a (f₁ x) ... let fₙ := fun x => a (fₙ₋₁ x) fₙ 0

The kernel processes each let by substituting the value into the body. Each value has a free bvar (references a), so substitution under inner binders creates shifted copies. In a de Bruijn kernel with deferred shifts, these Shift(val, offset) wrappers accumulate: step k must traverse through O(k) wrappers from previous steps, giving O(N²) total work.

A locally-nameless kernel substitutes fvars that need no shifting, giving O(N) total.

N=1000 in the Lean source. Increase to stress further.

Test result: 👍 accepted · exit code 0 · wall time: 6 ms · instructions: 39.3 M · max rss memory: 4.4 MB

Test "perf/unroll-versus-evaluate"

Expected: 👍 accept · Size: 44.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The declaration to check compares

count #(n+1)      and      N.add (count #n) #1

where #k is the numeral with k successors, and count #k evaluates to #k in Θ(k²) reductions.

The head constants differ. Unrolling count once turns the left side into the right side, leaving a traversal of the shared numeral #n, for Θ(n); evaluating both sides costs Θ(n²). The test asks which of two differing head constants a checker chooses to unfold.

N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §2.

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 9.0 M · max rss memory: 3.5 MB

Test "proj-non-structure"

Expected: ✋ reject · Size: 5.0 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Bad has two constructors, so projections should not be allowed. Prove false by using the second constructor, then projecting, hoping that the first constructor is used when inferring the type of the projection.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 3.3 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (11858) panicked at src/tc.rs:437:59:
called `Option::unwrap()` on a `None` value
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11857) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "proj-of-imax-prop"

Expected: ✋ reject · Size: 19.3 KB · Lines: 321 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A closed proof of False, with no axioms, via a data projection out of a proposition whose sort is Prop only up to universe level normalization.

ImaxProp : Sort (imax 1 0) is a proposition, since imax 1 0 normalizes to 0. The exploit uses two definitionally equal spellings of that type. Proof irrelevance is stated through ImaxAsProp : Prop := ImaxProp, whose type is the literal Sort 0, so it is accepted; the data projection imaxProjBool is stated on ImaxProp, whose type is the literal Sort (imax 1 0). A kernel that tests sorts for Prop syntactically does not recognize the latter as a proposition and wrongly allows projecting its Bool field out of a proof. Congruence on the proof-irrelevance equation then equates false and true, giving False.

This is https://github.com/leanprover/lean4/pull/14613, a bug in the official kernel.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 5.9 M · max rss memory: 3.5 MB

stderr:

thread 'thread_2' (11869) panicked at src/tc.rs:471:21:
infer_proj prop
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11866) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "proj-of-prop"

Expected: ✋ reject · Size: 3.9 KB · Lines: 56 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A proof of False via a projection from a Prop-typed structure whose constructor was applied to an ill-typed argument. The exported term is

badFalse : False := (Wrapper.mk True.intro).p

where Wrapper : Prop has a single field p : False, so Wrapper.mk expects a proof of False but is given True.intro : True.

A sound checker must reject this. A checker that types a projection by inferring (rather than checking) its structure argument — i.e. that trusts the structure to be well-typed instead of verifying the constructor's argument types against its binders — will accept it, because Wrapper.mk True.intro still formally inhabits Wrapper at the structural level, and the p projection is then read back out at the declared field type False.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 3.1 M · max rss memory: 3.2 MB

stderr:

thread 'thread_3' (11879) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11875) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "proof-irrel"

Expected: 👍 accept · Size: 1.7 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Incompleteness test for proof irrelevance under a binder.

bar : ∀ h : A → P, Q (h a) := foo where foo : ∀ h : A → P, Q (h b). Checking the assignment needs Q (h a) ≡ Q (h b), i.e. h a ≡ h b. Both h a and h b are proofs of the same Prop P, so they are definitionally equal by proof irrelevance and a complete kernel accepts.

A checker that fails to apply proof irrelevance here — comparing h a and h b structurally and finding the arguments a and b distinct — wrongly rejects a valid proof.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.2 MB

Test "rec-k-lie"

Expected: ✋ reject · Size: 5.3 KB · Lines: 87 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

False theorem via trusted k on a recursor.

Define MyBool with two constructors, and lie by claiming its recursor is K-like, so the major premise is replaced by the first constructor without being examined.

disc MyBool.true is then True rather than False.

MyBool rather than Bool because a module that overwrites an imported constant cannot be re-imported by the exporter.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 3.3 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (11894) panicked at src/inductive.rs:1279:21:
assertion failed: old_r.aux_data_ck(new_r)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11893) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "sparse-name-index"

Expected: 👍 accept · Size: 292 B · Lines: 4 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Lean4export will create internalization-table references contiguously in order: in references for names, il references for levels, and ie references for expressions all work this way.

This test checks that a kernel doesn't require internalization-table references to be assigned sequentially starting from 1. If the "2" and "4" were replaced by "1" and "0", respectively, this would be the expected encoding of axiom foo : Prop. This encoding should be equivalent.

Test result: 🚫 declined · exit code 2 · wall time: 3 ms · instructions: 2.2 M · max rss memory: 3.0 MB

stderr:

Declined: Name back-reference mismatch, expected In(1), found In(2). Back-refs must be continuous.

Test "std"

Expected: 👍 accept · Size: 526.1 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The complete Std library export from Lean 4.

This test contains the standard library extensions beyond core Lean 4, including:

Enhanced data structures (HashMap, RBTree, etc.)
Additional mathematical operations
Extended list and array operations
Utility functions and theorems

This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.

Test result: 👍 accepted · exit code 0 · wall time: 12.0 s · instructions: 333.0 G · max rss memory: 660.6 MB

Test "tutorial/001_basicDef"

Expected: 👍 accept · Size: 367 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Basic definition

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/002_badDef"

Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Mismatched types

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.0 MB

stderr:

thread 'thread_0' (11927) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11926) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/003_arrowType"

Expected: 👍 accept · Size: 622 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Arrow type (function type)

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.0 MB

Test "tutorial/004_dependentType"

Expected: 👍 accept · Size: 460 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Dependent type (forall)

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/005_constType"

Expected: 👍 accept · Size: 897 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Lambda expression

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.0 MB

Test "tutorial/006_betaReduction"

Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Lambda reduction

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.1 MB

Test "tutorial/007_betaReduction2"

Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Lambda reduction under binder

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.2 MB

Test "tutorial/008_forallSortWhnf"

Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The binding domain of a forall may need to be reduce before it is a sort

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.2 MB

Test "tutorial/009_forallSortBad"

Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The binding domain of a forall has to be a sort

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.2 MB

stderr:

thread 'thread_0' (11990) panicked at src/tc.rs:270:18:
infer_sort_of could not infer a sort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11989) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/010_nonTypeType"

Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The type of a declaration has to be a type, not some other expression

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.2 MB

stderr:

thread 'thread_0' (11999) panicked at src/tc.rs:251:18:
ensur_sort could not produce a sort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (11998) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/011_nonTypeAxiom"

Expected: ✋ reject · Size: 1.0 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

This applies to axioms as well, which are easy to overlook because they have no value to check the type against. Letting one through is not merely untidy: an axiom whose type is an arbitrary term inhabits whatever that term is later found definitionally equal to, and the eta and proof irrelevance rules are happy to equate a term like this with a great many things.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.0 MB

stderr:

thread 'thread_0' (12008) panicked at src/tc.rs:251:18:
ensur_sort could not produce a sort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12007) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/012_nonPropThm"

Expected: ✋ reject · Size: 424 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The type of a theorem has to be a proposition

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.1 MB

stderr:

thread 'thread_2' (12019) panicked at src/tc.rs:90:45:
called `Result::unwrap()` on an `Err` value: "Theorem type for nonPropThm must be `Prop` (sort 0); found type 1"
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12016) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/013_levelComp1"

Expected: 👍 accept · Size: 391 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/014_levelComp2"

Expected: 👍 accept · Size: 409 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.0 MB

Test "tutorial/015_levelComp3"

Expected: 👍 accept · Size: 427 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/016_levelParams"

Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level parameters

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.0 MB

Test "tutorial/017_tut06_bad01"

Expected: ✋ reject · Size: 427 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Duplicate universe parameters

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.2 MB

stderr:

thread 'thread_0' (12062) panicked at src/tc.rs:167:9:
assertion failed: self.ctx.no_dupes_all_params(info.uparams)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12061) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/018_levelComp4"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/019_levelComp5"

Expected: 👍 accept · Size: 424 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Some level computation

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.2 MB

Test "tutorial/020_imax1"

Expected: 👍 accept · Size: 809 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type inference for forall using imax

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.0 MB

Test "tutorial/021_imax2"

Expected: 👍 accept · Size: 828 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type inference for forall using imax

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.1 MB

Test "tutorial/022_levelMaxComm"

Expected: 👍 accept · Size: 524 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level equality: max is commutative (max u v ≈ max v u).

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 2.3 M · max rss memory: 2.9 MB

Test "tutorial/023_levelMaxAssoc"

Expected: 👍 accept · Size: 623 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level equality: max is associative (max (max u v) w ≈ max u (max v w)).

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.0 MB

Test "tutorial/024_levelMaxIdem"

Expected: 👍 accept · Size: 447 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level equality: max is idempotent (max u u ≈ u).

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/025_levelMaxAbsorb"

Expected: 👍 accept · Size: 526 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level equality: max absorption (max u (max u v) ≈ max u v).

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/026_inferVar"

Expected: 👍 accept · Size: 713 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type inference of local variables

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/027_defEqLambda"

Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Definitional equality between lambdas

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 2.4 M · max rss memory: 3.1 MB

Test "tutorial/028_peano1"

Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Peano arithmetic: 2 = 2

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.9 M · max rss memory: 3.0 MB

Test "tutorial/029_peano2"

Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Peano arithmetic: 1 + 1 = 2

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 3.2 M · max rss memory: 3.1 MB

Test "tutorial/030_peano3"

Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Peano arithmetic: 2 * 2 = 4

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 3.4 M · max rss memory: 3.1 MB

Test "tutorial/031_letType"

Expected: 👍 accept · Size: 489 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type checking a non-dependent let

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 2.9 MB

Test "tutorial/032_letTypeDep"

Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Type checking a dependent let

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.1 MB

Test "tutorial/033_letRed"

Expected: 👍 accept · Size: 627 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Reducing a let

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.3 M · max rss memory: 3.1 MB

Test "tutorial/034_empty"

Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A simple empty inductive type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.4 M · max rss memory: 3.1 MB

Test "tutorial/035_boolType"

Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A simple enumeration inductive type

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 2.6 M · max rss memory: 3.2 MB

Test "tutorial/036_twoBool"

Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A simple product type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.9 M · max rss memory: 3.1 MB

Test "tutorial/037_andType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A parametrized product type (no level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.9 M · max rss memory: 3.3 MB

Test "tutorial/038_prodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A parametrized product type (with level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 3.0 M · max rss memory: 3.0 MB

Test "tutorial/039_pprodType"

Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A parametrized product type (with more general level parameters)

Test result: 👍 accepted · exit code 0 · wall time: 4 ms · instructions: 3.0 M · max rss memory: 3.0 MB

Test "tutorial/040_pUnitType"

Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Level-polymorphic unit type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.5 M · max rss memory: 3.0 MB

Test "tutorial/041_eqType"

Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Equality, as an important indexed non-recursive data type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.9 M · max rss memory: 3.0 MB

Test "tutorial/042_natDef"

Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A recursive inductive data type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.8 M · max rss memory: 3.1 MB

Test "tutorial/043_rbTreeDef"

Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A recursive indexed data type

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 6.6 M · max rss memory: 3.1 MB

Test "tutorial/044_inductBadNonSort"

Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive type with a non-sort type

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.0 MB

stderr:

thread 'thread_0' (12305) panicked at src/tc.rs:251:18:
ensur_sort could not produce a sort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12304) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/045_inductBadNonSort2"

Expected: ✋ reject · Size: 598 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Another inductive type with a non-sort type

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.2 MB

stderr:

thread 'thread_1' (12315) panicked at src/tc.rs:251:18:
ensur_sort could not produce a sort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12313) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/046_inductLevelParam"

Expected: ✋ reject · Size: 515 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive with duplicate level params

Test result: ✋ rejected · exit code 1 · wall time: 4 ms · instructions: 2.5 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (12323) panicked at src/tc.rs:167:9:
assertion failed: self.ctx.no_dupes_all_params(info.uparams)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12322) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/047_inductTooFewParams"

Expected: ✋ reject · Size: 548 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive with too few parameters in the type

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (12332) panicked at src/inductive.rs:387:22:
exhausted telescope early
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12331) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/048_inductWrongCtorParams"

Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive with a constructor with wrong parameters

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.2 MB

stderr:

thread 'thread_1' (12342) panicked at src/tc.rs:921:71:
assertion failed: self.def_eq(u, v)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12340) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/049_inductWrongCtorResParams"

Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive with a constructor with wrong parameters in result (they are swapped)

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.2 MB

stderr:

thread 'thread_1' (12351) panicked at src/inductive.rs:864:9:
assertion failed: self.is_valid_ind_app(st, parent_ind_name, ctor_type_cursor)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12349) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/050_inductWrongCtorResLevel"

Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive with a constructor with wrong level parameters in result (they are swapped)

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.1 MB

stderr:

thread 'thread_1' (12360) panicked at src/inductive.rs:864:9:
assertion failed: self.is_valid_ind_app(st, parent_ind_name, ctor_type_cursor)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12358) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/051_inductInIndex"

Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

A constructor with an unexpected occurrence of the type in index position of a return type.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.3 MB

stderr:

thread 'thread_0' (12368) panicked at src/inductive.rs:864:9:
assertion failed: self.is_valid_ind_app(st, parent_ind_name, ctor_type_cursor)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12367) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/052_indNeg"

Expected: ✋ reject · Size: 996 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The classic example of an inductive with negative recursive occurrence

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.1 MB

stderr:

thread 'thread_1' (12378) panicked at src/inductive.rs:29:17:
assertion `left == right` failed
  left: false
 right: true
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12376) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/053_reduceCtorParam.mk"

Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

When checking inductives, we expect the kernel to reduce the types of constructor arguments.

Test result: 👍 accepted · exit code 0 · wall time: 30 ms · instructions: 3.1 M · max rss memory: 3.2 MB

Test "tutorial/054_reduceCtorType.mk"

Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

When checking inductives, we expect the kernel to not reduce the type of the constructor itself; that should be all manifest foralls

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.1 MB

stderr:

thread 'thread_0' (12395) panicked at src/inductive.rs:864:9:
assertion failed: self.is_valid_ind_app(st, parent_ind_name, ctor_type_cursor)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12394) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/055_indNegReducible"

Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.7 M · max rss memory: 3.2 MB

stderr:

thread 'thread_3' (12407) panicked at src/inductive.rs:29:17:
assertion `left == right` failed
  left: false
 right: true
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12403) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/056_predWithTypeField"

Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive proposition can have constructors with fields of arbitrary level.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.0 MB

Test "tutorial/057_typeWithTypeField"

Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive type can have fields of level up to that of the inductive.

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.1 MB

Test "tutorial/058_typeWithTypeFieldPoly"

Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive type can have fields of level up to that of the inductive (polymorphic variant).

Test result: 👍 accepted · exit code 0 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.1 MB

Test "tutorial/059_typeWithTooHighTypeField.mk"

Expected: ✋ reject · Size: 943 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

An inductive type can have fields of from higher universes.

Test result: ✋ rejected · exit code 1 · wall time: 3 ms · instructions: 2.6 M · max rss memory: 3.2 MB

stderr:

thread 'thread_2' (12442) panicked at src/inductive.rs:854:17:
Constructor argument was too large for the corresponding inductive type
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread 'main' (12439) panicked at src/tc.rs:139:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }

Test "tutorial/060_emptyRec"

Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source