Checker "evmlean"
Version: 0.1.0 · 📄 Declaration · 🔗 Source
A Lean 4 kernel implemented in Solidity and executed on the Ethereum Virtual Machine. Accepting a proof is a metered EVM execution; the same call can be replayed on any EVM chain (36.7KB deployed — sized for the EIP-7907 limit). Rejects all five of the Arena's static adversarial exports at the offending declaration. Declines declarations outside its fragment (nested inductives, multi-type mutual groups, unsafe decls, String reduction) and exports beyond its resource budget.
93/93
50/50
9
Detailed results
Test "bogus1"
Expected: ✋ reject · Size: 11.4 KB · Lines: 198 · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 1.1 s · instructions: 8.1 G · max rss memory: 119.6 MB
stderr:
evmlean: reject (decl 19, value/type mismatch); gas=4671869
Test "cedar"
Expected: 👍 accept · Size: 728.6 MB · Lines: 13.4 M · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 305 ms · instructions: 2.1 G · max rss memory: 88.6 MB
stderr:
evmlean: export is 764035699 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "constlevels"
Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.0-rc2 · 📄 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: 1.0 s · instructions: 9.6 G · max rss memory: 119.2 MB
stderr:
evmlean: reject (decl 23, universe count mismatch); gas=6381225
Test "cslib"
Expected: 👍 accept · Size: 1.2 GB · Lines: 22.8 M · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The Lean Computer Science Library (CSLib).
Test result: 🚫 declined · exit code 2 · wall time: 306 ms · instructions: 2.2 G · max rss memory: 88.4 MB
stderr:
evmlean: export is 1303029010 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "init"
Expected: 👍 accept · Size: 309.5 MB · Lines: 6.1 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 290 ms · instructions: 2.2 G · max rss memory: 88.3 MB
stderr:
evmlean: export is 324561407 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "init-prelude"
Expected: 👍 accept · Size: 3.5 MB · Lines: 63.7 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The Init.Prelude module export.
Test result: 🚫 declined · exit code 2 · wall time: 288 ms · instructions: 2.2 G · max rss memory: 88.1 MB
stderr:
evmlean: export is 3714854 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "k-rec-conv"
Expected: ✋ reject · Size: 13.0 KB · Lines: 243 · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 1.1 s · instructions: 10.1 G · max rss memory: 118.8 MB
stderr:
evmlean: reject (decl 19, value/type mismatch); gas=6784930
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: 480 ms · instructions: 3.9 G · max rss memory: 122.1 MB
stderr:
evmlean: reject (decl 10, unknown constant); gas=472096
Test "level-imax-leq"
Expected: ✋ reject · Size: 5.6 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 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: 540 ms · instructions: 4.5 G · max rss memory: 120.8 MB
stderr:
evmlean: reject (decl 12, value/type mismatch); gas=989529
Test "level-imax-normalization"
Expected: ✋ reject · Size: 5.8 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 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: 517 ms · instructions: 4.6 G · max rss memory: 115.4 MB
stderr:
evmlean: reject (decl 12, value/type mismatch); gas=986829
Test "level-index-out-of-order"
Expected: 👍 accept · Size: 332 B · Lines: 6 · lean4export: 0.1.0 · Lean: 4.27.0-rc1 · 📄 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: 👍 accepted · exit code 0 · wall time: 460 ms · instructions: 3.4 G · max rss memory: 121.5 MB
stderr:
evmlean: accept (decl 1, ok); gas=161061
Test "mathlib"
Expected: 👍 accept · Size: 5.2 GB · Lines: 100.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 304 ms · instructions: 2.2 G · max rss memory: 88.0 MB
stderr:
evmlean: export is 5636308621 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "nat-rec-rules"
Expected: ✋ reject · Size: 8.2 KB · Lines: 128 · lean4export: 3.1.0 · Lean: 4.29.0-rc1 · 📄 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: 589 ms · instructions: 5.1 G · max rss memory: 122.4 MB
stderr:
evmlean: reject (decl 12, recursor rule invalid); gas=1539825
Test "perf/app-lam"
Expected: 👍 accept · Size: 1.2 MB · Lines: 28.6 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 328 ms · instructions: 2.1 G · max rss memory: 88.4 MB
stderr:
evmlean: export is 1276513 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 284 ms · instructions: 2.2 G · max rss memory: 88.3 MB
stderr:
evmlean: export is 10184724 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "perf/shift-cascade"
Expected: 👍 accept · Size: 256.3 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 297 ms · instructions: 2.2 G · max rss memory: 88.7 MB
stderr:
evmlean: export is 262410 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "proj-of-prop"
Expected: ✋ reject · Size: 3.9 KB · Lines: 56 · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 519 ms · instructions: 4.2 G · max rss memory: 122.2 MB
stderr:
evmlean: reject (decl 11, application argument type mismatch); gas=780909
Test "sparse-name-index"
Expected: 👍 accept · Size: 296 B · Lines: 4 · lean4export: 0.1.0 · Lean: 4.27.0-rc1 · 📄 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 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: 👍 accepted · exit code 0 · wall time: 434 ms · instructions: 3.4 G · max rss memory: 122.9 MB
stderr:
evmlean: accept (decl 1, ok); gas=162502
Test "std"
Expected: 👍 accept · Size: 526.1 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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: 🚫 declined · exit code 2 · wall time: 284 ms · instructions: 2.1 G · max rss memory: 88.4 MB
stderr:
evmlean: export is 551674936 bytes, above EVMLEAN_MAX_BYTES=128000; declining
Test "tutorial/001_basicDef"
Expected: 👍 accept · Size: 371 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Basic definition
Test result: 👍 accepted · exit code 0 · wall time: 415 ms · instructions: 3.4 G · max rss memory: 121.4 MB
stderr:
evmlean: accept (decl 1, ok); gas=165610
Test "tutorial/002_badDef"
Expected: ✋ reject · Size: 369 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Mismatched types
Test result: ✋ rejected · exit code 1 · wall time: 425 ms · instructions: 3.4 G · max rss memory: 122.1 MB
stderr:
evmlean: reject (decl 0, value/type mismatch); gas=171329
Test "tutorial/003_arrowType"
Expected: 👍 accept · Size: 626 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Arrow type (function type)
Test result: 👍 accepted · exit code 0 · wall time: 431 ms · instructions: 3.4 G · max rss memory: 121.4 MB
stderr:
evmlean: accept (decl 1, ok); gas=186926
Test "tutorial/004_dependentType"
Expected: 👍 accept · Size: 464 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Dependent type (forall)
Test result: 👍 accepted · exit code 0 · wall time: 434 ms · instructions: 3.4 G · max rss memory: 122.6 MB
stderr:
evmlean: accept (decl 1, ok); gas=175877
Test "tutorial/005_constType"
Expected: 👍 accept · Size: 901 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda expression
Test result: 👍 accepted · exit code 0 · wall time: 430 ms · instructions: 3.5 G · max rss memory: 113.5 MB
stderr:
evmlean: accept (decl 1, ok); gas=214726
Test "tutorial/006_betaReduction"
Expected: 👍 accept · Size: 1.3 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction
Test result: 👍 accepted · exit code 0 · wall time: 433 ms · instructions: 3.6 G · max rss memory: 122.4 MB
stderr:
evmlean: accept (decl 2, ok); gas=288883
Test "tutorial/007_betaReduction2"
Expected: 👍 accept · Size: 1.4 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Lambda reduction under binder
Test result: 👍 accepted · exit code 0 · wall time: 443 ms · instructions: 3.7 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 2, ok); gas=301271
Test "tutorial/008_forallSortWhnf"
Expected: 👍 accept · Size: 1.2 KB · Lines: 25 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 443 ms · instructions: 3.6 G · max rss memory: 122.4 MB
stderr:
evmlean: accept (decl 2, ok); gas=309201
Test "tutorial/009_forallSortBad"
Expected: ✋ reject · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The binding domain of a forall has to be a sort
Test result: ✋ rejected · exit code 1 · wall time: 455 ms · instructions: 3.7 G · max rss memory: 121.0 MB
stderr:
evmlean: reject (decl 1, binder domain is not a sort); gas=280789
Test "tutorial/010_nonTypeType"
Expected: ✋ reject · Size: 1.1 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a declaration has to be a type, not some other expression
Test result: ✋ rejected · exit code 1 · wall time: 433 ms · instructions: 3.5 G · max rss memory: 121.3 MB
stderr:
evmlean: reject (decl 1, type is not a sort); gas=226175
Test "tutorial/011_nonPropThm"
Expected: ✋ reject · Size: 428 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The type of a theorem has to be a proposition
Test result: ✋ rejected · exit code 1 · wall time: 420 ms · instructions: 3.3 G · max rss memory: 118.4 MB
stderr:
evmlean: reject (decl 0, theorem type not a Prop); gas=167426
Test "tutorial/012_levelComp1"
Expected: 👍 accept · Size: 395 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 443 ms · instructions: 3.5 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 1, ok); gas=183484
Test "tutorial/013_levelComp2"
Expected: 👍 accept · Size: 413 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 440 ms · instructions: 3.5 G · max rss memory: 122.1 MB
stderr:
evmlean: accept (decl 1, ok); gas=190027
Test "tutorial/014_levelComp3"
Expected: 👍 accept · Size: 431 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 440 ms · instructions: 3.5 G · max rss memory: 123.2 MB
stderr:
evmlean: accept (decl 1, ok); gas=203541
Test "tutorial/015_levelParams"
Expected: 👍 accept · Size: 1.4 KB · Lines: 29 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level parameters
Test result: 👍 accepted · exit code 0 · wall time: 458 ms · instructions: 3.5 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 2, ok); gas=305780
Test "tutorial/016_tut06_bad01"
Expected: ✋ reject · Size: 431 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Duplicate universe parameters
Test result: ✋ rejected · exit code 1 · wall time: 416 ms · instructions: 3.4 G · max rss memory: 122.7 MB
stderr:
evmlean: reject (decl 0, duplicate universe param); gas=161139
Test "tutorial/017_levelComp4"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 424 ms · instructions: 3.4 G · max rss memory: 122.7 MB
stderr:
evmlean: accept (decl 1, ok); gas=168675
Test "tutorial/018_levelComp5"
Expected: 👍 accept · Size: 428 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Some level computation
Test result: 👍 accepted · exit code 0 · wall time: 420 ms · instructions: 3.4 G · max rss memory: 122.9 MB
stderr:
evmlean: accept (decl 1, ok); gas=169799
Test "tutorial/019_imax1"
Expected: 👍 accept · Size: 813 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 425 ms · instructions: 3.4 G · max rss memory: 121.5 MB
stderr:
evmlean: accept (decl 1, ok); gas=203928
Test "tutorial/020_imax2"
Expected: 👍 accept · Size: 832 B · Lines: 17 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference for forall using imax
Test result: 👍 accepted · exit code 0 · wall time: 449 ms · instructions: 3.6 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 1, ok); gas=243153
Test "tutorial/021_levelMaxComm"
Expected: 👍 accept · Size: 528 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level equality: max is commutative (max u v ≈ max v u).
Test result: 👍 accepted · exit code 0 · wall time: 424 ms · instructions: 3.4 G · max rss memory: 121.8 MB
stderr:
evmlean: accept (decl 1, ok); gas=214851
Test "tutorial/022_levelMaxAssoc"
Expected: 👍 accept · Size: 627 B · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 462 ms · instructions: 3.6 G · max rss memory: 122.6 MB
stderr:
evmlean: accept (decl 1, ok); gas=245538
Test "tutorial/023_levelMaxIdem"
Expected: 👍 accept · Size: 451 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level equality: max is idempotent (max u u ≈ u).
Test result: 👍 accepted · exit code 0 · wall time: 436 ms · instructions: 3.4 G · max rss memory: 122.1 MB
stderr:
evmlean: accept (decl 1, ok); gas=188143
Test "tutorial/024_levelMaxAbsorb"
Expected: 👍 accept · Size: 530 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level equality: max absorption (max u (max u v) ≈ max u v).
Test result: 👍 accepted · exit code 0 · wall time: 452 ms · instructions: 3.5 G · max rss memory: 121.9 MB
stderr:
evmlean: accept (decl 1, ok); gas=225251
Test "tutorial/025_inferVar"
Expected: 👍 accept · Size: 717 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type inference of local variables
Test result: 👍 accepted · exit code 0 · wall time: 426 ms · instructions: 3.5 G · max rss memory: 122.5 MB
stderr:
evmlean: accept (decl 1, ok); gas=199389
Test "tutorial/026_defEqLambda"
Expected: 👍 accept · Size: 1.4 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Definitional equality between lambdas
Test result: 👍 accepted · exit code 0 · wall time: 452 ms · instructions: 3.8 G · max rss memory: 121.3 MB
stderr:
evmlean: accept (decl 1, ok); gas=352731
Test "tutorial/027_peano1"
Expected: 👍 accept · Size: 3.6 KB · Lines: 73 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 = 2
Test result: 👍 accepted · exit code 0 · wall time: 490 ms · instructions: 4.2 G · max rss memory: 122.3 MB
stderr:
evmlean: accept (decl 7, ok); gas=704799
Test "tutorial/028_peano2"
Expected: 👍 accept · Size: 4.5 KB · Lines: 90 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 1 + 1 = 2
Test result: 👍 accepted · exit code 0 · wall time: 578 ms · instructions: 5.2 G · max rss memory: 115.1 MB
stderr:
evmlean: accept (decl 8, ok); gas=1702604
Test "tutorial/029_peano3"
Expected: 👍 accept · Size: 4.9 KB · Lines: 98 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Peano arithmetic: 2 * 2 = 4
Test result: 👍 accepted · exit code 0 · wall time: 700 ms · instructions: 6.4 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 10, ok); gas=2836620
Test "tutorial/030_letType"
Expected: 👍 accept · Size: 493 B · Lines: 9 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a non-dependent let
Test result: 👍 accepted · exit code 0 · wall time: 456 ms · instructions: 3.3 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 1, ok); gas=176778
Test "tutorial/031_letTypeDep"
Expected: 👍 accept · Size: 1.2 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking a dependent let
Test result: 👍 accepted · exit code 0 · wall time: 437 ms · instructions: 3.5 G · max rss memory: 121.9 MB
stderr:
evmlean: accept (decl 3, ok); gas=259315
Test "tutorial/032_letRed"
Expected: 👍 accept · Size: 631 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing a let
Test result: 👍 accepted · exit code 0 · wall time: 439 ms · instructions: 3.3 G · max rss memory: 121.4 MB
stderr:
evmlean: accept (decl 2, ok); gas=187860
Test "tutorial/033_empty"
Expected: 👍 accept · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple empty inductive type
Test result: 👍 accepted · exit code 0 · wall time: 441 ms · instructions: 3.6 G · max rss memory: 122.2 MB
stderr:
evmlean: accept (decl 4, ok); gas=283703
Test "tutorial/034_boolType"
Expected: 👍 accept · Size: 2.3 KB · Lines: 37 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple enumeration inductive type
Test result: 👍 accepted · exit code 0 · wall time: 489 ms · instructions: 4.0 G · max rss memory: 120.8 MB
stderr:
evmlean: accept (decl 6, ok); gas=597017
Test "tutorial/035_twoBool"
Expected: 👍 accept · Size: 4.2 KB · Lines: 65 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A simple product type
Test result: 👍 accepted · exit code 0 · wall time: 561 ms · instructions: 4.5 G · max rss memory: 122.3 MB
stderr:
evmlean: accept (decl 10, ok); gas=1012021
Test "tutorial/036_andType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 57 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (no level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 563 ms · instructions: 4.5 G · max rss memory: 120.8 MB
stderr:
evmlean: accept (decl 5, ok); gas=1061965
Test "tutorial/037_prodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 76 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 721 ms · instructions: 6.5 G · max rss memory: 120.9 MB
stderr:
evmlean: accept (decl 5, ok); gas=3202417
Test "tutorial/038_pprodType"
Expected: 👍 accept · Size: 3.8 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A parametrized product type (with more general level parameters)
Test result: 👍 accepted · exit code 0 · wall time: 771 ms · instructions: 6.8 G · max rss memory: 120.7 MB
stderr:
evmlean: accept (decl 5, ok); gas=3457261
Test "tutorial/039_pUnitType"
Expected: 👍 accept · Size: 1.8 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Level-polymorphic unit type
Test result: 👍 accepted · exit code 0 · wall time: 461 ms · instructions: 3.9 G · max rss memory: 121.8 MB
stderr:
evmlean: accept (decl 5, ok); gas=437652
Test "tutorial/040_eqType"
Expected: 👍 accept · Size: 3.2 KB · Lines: 62 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Equality, as an important indexed non-recursive data type
Test result: 👍 accepted · exit code 0 · wall time: 659 ms · instructions: 5.7 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 5, ok); gas=2398419
Test "tutorial/041_natDef"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive inductive data type
Test result: 👍 accepted · exit code 0 · wall time: 493 ms · instructions: 4.2 G · max rss memory: 120.9 MB
stderr:
evmlean: accept (decl 6, ok); gas=817788
Test "tutorial/042_rbTreeDef"
Expected: 👍 accept · Size: 15.7 KB · Lines: 296 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A recursive indexed data type
Test result: 👍 accepted · exit code 0 · wall time: 3.2 s · instructions: 33.1 G · max rss memory: 120.0 MB
stderr:
evmlean: accept (decl 17, ok); gas=32625643
Test "tutorial/043_inductBadNonSort"
Expected: ✋ reject · Size: 1.2 KB · Lines: 20 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type with a non-sort type
Test result: ✋ rejected · exit code 1 · wall time: 452 ms · instructions: 3.5 G · max rss memory: 122.3 MB
stderr:
evmlean: reject (decl 1, inductive shape); gas=229831
Test "tutorial/044_inductBadNonSort2"
Expected: ✋ reject · Size: 602 B · Lines: 8 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Another inductive type with a non-sort type
Test result: ✋ rejected · exit code 1 · wall time: 412 ms · instructions: 3.5 G · max rss memory: 121.8 MB
stderr:
evmlean: reject (decl 1, inductive shape); gas=177815
Test "tutorial/045_inductLevelParam"
Expected: ✋ reject · Size: 519 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with duplicate level params
Test result: ✋ rejected · exit code 1 · wall time: 442 ms · instructions: 3.3 G · max rss memory: 121.0 MB
stderr:
evmlean: reject (decl 0, duplicate universe param); gas=165661
Test "tutorial/046_inductTooFewParams"
Expected: ✋ reject · Size: 552 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with too few parameters in the type
Test result: ✋ rejected · exit code 1 · wall time: 492 ms · instructions: 3.3 G · max rss memory: 122.9 MB
stderr:
evmlean: reject (decl 0, inductive shape); gas=180384
Test "tutorial/047_inductWrongCtorParams"
Expected: ✋ reject · Size: 1.2 KB · Lines: 16 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters
Test result: ✋ rejected · exit code 1 · wall time: 428 ms · instructions: 3.6 G · max rss memory: 121.6 MB
stderr:
evmlean: reject (decl 1, constructor shape); gas=234585
Test "tutorial/048_inductWrongCtorResParams"
Expected: ✋ reject · Size: 1.3 KB · Lines: 19 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong parameters in result (they are swapped)
Test result: ✋ rejected · exit code 1 · wall time: 455 ms · instructions: 3.6 G · max rss memory: 121.6 MB
stderr:
evmlean: reject (decl 0, constructor result type); gas=275652
Test "tutorial/049_inductWrongCtorResLevel"
Expected: ✋ reject · Size: 1.4 KB · Lines: 23 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with a constructor with wrong level parameters in result (they are swapped)
Test result: ✋ rejected · exit code 1 · wall time: 485 ms · instructions: 3.5 G · max rss memory: 122.7 MB
stderr:
evmlean: reject (decl 0, constructor result levels); gas=291058
Test "tutorial/050_inductInIndex"
Expected: ✋ reject · Size: 1.1 KB · Lines: 14 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 434 ms · instructions: 3.5 G · max rss memory: 122.2 MB
stderr:
evmlean: reject (decl 1, constructor result type); gas=219594
Test "tutorial/051_indNeg"
Expected: ✋ reject · Size: 1000 B · Lines: 12 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The classic example of an inductive with negative recursive occurrence
Test result: ✋ rejected · exit code 1 · wall time: 472 ms · instructions: 3.5 G · max rss memory: 121.4 MB
stderr:
evmlean: reject (decl 0, positivity violation); gas=207656
Test "tutorial/052_reduceCtorParam.mk"
Expected: 👍 accept · Size: 4.1 KB · Lines: 80 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments.
Test result: 👍 accepted · exit code 0 · wall time: 570 ms · instructions: 5.1 G · max rss memory: 121.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=1564651
Test "tutorial/053_reduceCtorType.mk"
Expected: ✋ reject · Size: 1.5 KB · Lines: 26 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 454 ms · instructions: 3.6 G · max rss memory: 122.0 MB
stderr:
evmlean: reject (decl 1, constructor result type); gas=260540
Test "tutorial/054_indNegReducible"
Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 448 ms · instructions: 3.6 G · max rss memory: 120.8 MB
stderr:
evmlean: reject (decl 2, positivity violation); gas=303029
Test "tutorial/055_predWithTypeField"
Expected: 👍 accept · Size: 2.0 KB · Lines: 32 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive proposition can have constructors with fields of arbitrary level.
Test result: 👍 accepted · exit code 0 · wall time: 469 ms · instructions: 3.9 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 5, ok); gas=421634
Test "tutorial/056_typeWithTypeField"
Expected: 👍 accept · Size: 2.1 KB · Lines: 36 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of level up to that of the inductive.
Test result: 👍 accepted · exit code 0 · wall time: 461 ms · instructions: 3.9 G · max rss memory: 112.8 MB
stderr:
evmlean: accept (decl 5, ok); gas=481932
Test "tutorial/057_typeWithTypeFieldPoly"
Expected: 👍 accept · Size: 2.1 KB · Lines: 38 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 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: 484 ms · instructions: 4.0 G · max rss memory: 121.9 MB
stderr:
evmlean: accept (decl 5, ok); gas=531660
Test "tutorial/058_typeWithTooHighTypeField.mk"
Expected: ✋ reject · Size: 947 B · Lines: 11 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive type can have fields of from higher universes.
Test result: ✋ rejected · exit code 1 · wall time: 433 ms · instructions: 3.4 G · max rss memory: 121.3 MB
stderr:
evmlean: reject (decl 0, field universe too large); gas=212947
Test "tutorial/059_emptyRec"
Expected: 👍 accept · Size: 1.2 KB · Lines: 21 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 465 ms · instructions: 3.8 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 4, ok); gas=357577
Test "tutorial/060_boolRec"
Expected: 👍 accept · Size: 3.0 KB · Lines: 53 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 518 ms · instructions: 4.4 G · max rss memory: 121.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=941715
Test "tutorial/061_twoBoolRec"
Expected: 👍 accept · Size: 4.8 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 584 ms · instructions: 4.7 G · max rss memory: 121.3 MB
stderr:
evmlean: accept (decl 10, ok); gas=1308965
Test "tutorial/062_andRec"
Expected: 👍 accept · Size: 3.2 KB · Lines: 58 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 565 ms · instructions: 5.0 G · max rss memory: 122.2 MB
stderr:
evmlean: accept (decl 5, ok); gas=1506816
Test "tutorial/063_prodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 79 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 888 ms · instructions: 7.9 G · max rss memory: 121.1 MB
stderr:
evmlean: accept (decl 5, ok); gas=4860299
Test "tutorial/064_pprodRec"
Expected: 👍 accept · Size: 4.0 KB · Lines: 78 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 920 ms · instructions: 8.1 G · max rss memory: 120.7 MB
stderr:
evmlean: accept (decl 5, ok); gas=4950261
Test "tutorial/065_punitRec"
Expected: 👍 accept · Size: 2.2 KB · Lines: 39 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 495 ms · instructions: 4.0 G · max rss memory: 120.9 MB
stderr:
evmlean: accept (decl 5, ok); gas=595573
Test "tutorial/066_eqRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 63 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 824 ms · instructions: 7.2 G · max rss memory: 120.9 MB
stderr:
evmlean: accept (decl 5, ok); gas=4042663
Test "tutorial/067_nRec"
Expected: 👍 accept · Size: 3.3 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 597 ms · instructions: 4.4 G · max rss memory: 121.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=1016620
Test "tutorial/068_rbTreeRef"
Expected: 👍 accept · Size: 16.2 KB · Lines: 303 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor
Test result: 👍 accepted · exit code 0 · wall time: 4.5 s · instructions: 47.5 G · max rss memory: 119.7 MB
stderr:
evmlean: accept (decl 17, ok); gas=48690916
Test "tutorial/069_boolPropRec"
Expected: 👍 accept · Size: 2.3 KB · Lines: 34 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have more than one constructor.
Test result: 👍 accepted · exit code 0 · wall time: 464 ms · instructions: 4.0 G · max rss memory: 121.4 MB
stderr:
evmlean: accept (decl 6, ok); gas=513377
Test "tutorial/070_existsRec"
Expected: 👍 accept · Size: 3.6 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Prop if they have one constructors and it carries data.
Test result: 👍 accepted · exit code 0 · wall time: 550 ms · instructions: 4.9 G · max rss memory: 121.3 MB
stderr:
evmlean: accept (decl 5, ok); gas=1342188
Test "tutorial/071_sortElimPropRec"
Expected: 👍 accept · Size: 5.6 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index
Test result: 👍 accepted · exit code 0 · wall time: 824 ms · instructions: 7.5 G · max rss memory: 121.1 MB
stderr:
evmlean: accept (decl 10, ok); gas=4232746
Test "tutorial/072_sortElimProp2Rec"
Expected: 👍 accept · Size: 6.6 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index. However, it must occur directly in the result type, with no intervening reduction.
Test result: 👍 accepted · exit code 0 · wall time: 620 ms · instructions: 5.6 G · max rss memory: 121.3 MB
stderr:
evmlean: accept (decl 11, ok); gas=2056036
Test "tutorial/073_boolRecEqns"
Expected: 👍 accept · Size: 10.8 KB · Lines: 199 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Bool.rec
Test result: 👍 accepted · exit code 0 · wall time: 976 ms · instructions: 8.9 G · max rss memory: 118.9 MB
stderr:
evmlean: accept (decl 14, ok); gas=5671377
Test "tutorial/074_prodRecEqns"
Expected: 👍 accept · Size: 10.1 KB · Lines: 205 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Prod.rec
Test result: 👍 accepted · exit code 0 · wall time: 1.1 s · instructions: 10.6 G · max rss memory: 119.6 MB
stderr:
evmlean: accept (decl 9, ok); gas=7439513
Test "tutorial/075_nRecReduction"
Expected: 👍 accept · Size: 12.7 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A proof relying on the reduction behavior of N.rec
Test result: 👍 accepted · exit code 0 · wall time: 1.2 s · instructions: 10.8 G · max rss memory: 118.7 MB
stderr:
evmlean: accept (decl 16, ok); gas=7840686
Test "tutorial/076_listRecReduction"
Expected: 👍 accept · Size: 17.5 KB · Lines: 335 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of List.rec
Test result: 👍 accepted · exit code 0 · wall time: 2.2 s · instructions: 21.6 G · max rss memory: 128.5 MB
stderr:
evmlean: accept (decl 17, ok); gas=19692220
Test "tutorial/077_RBTree.id_spec"
Expected: 👍 accept · Size: 47.9 KB · Lines: 1.0 k · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RBTree.rec
Test result: 👍 accepted · exit code 0 · wall time: 9.1 s · instructions: 96.7 G · max rss memory: 211.9 MB
stderr:
evmlean: accept (decl 23, ok); gas=127963632
Test "tutorial/078_And.right"
Expected: 👍 accept · Size: 4.3 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking simple projection functions
Test result: 👍 accepted · exit code 0 · wall time: 558 ms · instructions: 4.7 G · max rss memory: 121.3 MB
stderr:
evmlean: accept (decl 6, ok); gas=1315288
Test "tutorial/079_Prod.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions with parameters
Test result: 👍 accepted · exit code 0 · wall time: 798 ms · instructions: 7.2 G · max rss memory: 121.8 MB
stderr:
evmlean: accept (decl 6, ok); gas=4046573
Test "tutorial/080_PProd.snd"
Expected: 👍 accept · Size: 4.5 KB · Lines: 83 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking projection functions
Test result: 👍 accepted · exit code 0 · wall time: 837 ms · instructions: 7.2 G · max rss memory: 120.4 MB
stderr:
evmlean: accept (decl 6, ok); gas=3974812
Test "tutorial/081_PSigma.snd"
Expected: 👍 accept · Size: 5.1 KB · Lines: 96 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type-checking dependent projection functions
Test result: 👍 accepted · exit code 0 · wall time: 838 ms · instructions: 8.0 G · max rss memory: 119.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=4728349
Test "tutorial/082_projOutOfRange"
Expected: ✋ reject · Size: 3.8 KB · Lines: 67 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Out of range projection
Test result: ✋ rejected · exit code 1 · wall time: 557 ms · instructions: 4.7 G · max rss memory: 121.1 MB
stderr:
evmlean: reject (decl 4, projection violation); gas=1189030
Test "tutorial/083_projNotStruct"
Expected: ✋ reject · Size: 3.5 KB · Lines: 64 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection out something that is not a structure
Test result: ✋ rejected · exit code 1 · wall time: 498 ms · instructions: 4.2 G · max rss memory: 121.1 MB
stderr:
evmlean: reject (decl 5, projection violation); gas=839847
Test "tutorial/084_projProp1"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields.
Test result: 👍 accepted · exit code 0 · wall time: 780 ms · instructions: 7.2 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 13, ok); gas=3830409
Test "tutorial/085_projProp2"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: ✋ rejected · exit code 1 · wall time: 792 ms · instructions: 7.2 G · max rss memory: 119.9 MB
stderr:
evmlean: reject (decl 12, projection violation); gas=3850407
Test "tutorial/086_projProp3"
Expected: 👍 accept · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel allows projections out of propositions if they precede all dependent data fields. Non-dependent data fields are not relevant.
Test result: 👍 accepted · exit code 0 · wall time: 776 ms · instructions: 7.4 G · max rss memory: 119.0 MB
stderr:
evmlean: accept (decl 13, ok); gas=3870813
Test "tutorial/087_projProp4"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows data projections out of propositional structures.
Test result: ✋ rejected · exit code 1 · wall time: 797 ms · instructions: 7.4 G · max rss memory: 119.0 MB
stderr:
evmlean: reject (decl 12, projection violation); gas=3885955
Test "tutorial/088_projProp5"
Expected: ✋ reject · Size: 8.4 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition
The lean kernel disallows proof projections out of propositional structures that depend on data.
Test result: ✋ rejected · exit code 1 · wall time: 823 ms · instructions: 7.2 G · max rss memory: 117.7 MB
stderr:
evmlean: reject (decl 12, projection violation); gas=3902786
Test "tutorial/089_projProp6"
Expected: ✋ reject · Size: 8.2 KB · Lines: 143 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out of a proposition.
The lean kernel rejects any projections out of a proposition that come after a dependent data field, even if that is not used by the present projection.
Test result: ✋ rejected · exit code 1 · wall time: 786 ms · instructions: 7.4 G · max rss memory: 119.1 MB
stderr:
evmlean: reject (decl 12, projection violation); gas=3887463
Test "tutorial/090_projDataIndexRec"
Expected: 👍 accept · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The recursor for ProjDataIndex allows elimination into sort.
Test result: 👍 accepted · exit code 0 · wall time: 607 ms · instructions: 5.3 G · max rss memory: 121.8 MB
stderr:
evmlean: accept (decl 14, ok); gas=1709691
Test "tutorial/091_projIndexData"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
Test result: ✋ rejected · exit code 1 · wall time: 576 ms · instructions: 5.0 G · max rss memory: 121.1 MB
stderr:
evmlean: reject (decl 13, unknown constant); gas=1499358
Test "tutorial/092_projIndexData2"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
This also forbids projecting out proofs that follow such fields.
Test result: ✋ rejected · exit code 1 · wall time: 580 ms · instructions: 5.1 G · max rss memory: 120.2 MB
stderr:
evmlean: reject (decl 13, unknown constant); gas=1500687
Test "tutorial/093_projRed"
Expected: 👍 accept · Size: 9.9 KB · Lines: 177 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Projection reductions
Test result: 👍 accepted · exit code 0 · wall time: 1.1 s · instructions: 9.9 G · max rss memory: 119.5 MB
stderr:
evmlean: accept (decl 16, ok); gas=6734060
Test "tutorial/094_ruleK"
Expected: 👍 accept · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq:
The recursor reduces even if the major argument is not a constructor,
as long replacing the major argument with a constructor is type correct.
Test result: 👍 accepted · exit code 0 · wall time: 776 ms · instructions: 6.9 G · max rss memory: 122.2 MB
stderr:
evmlean: accept (decl 10, ok); gas=3510701
Test "tutorial/095_ruleKbad"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k for Eq should not fire if the types of the major argument
do not match that of the constructor.
Test result: ✋ rejected · exit code 1 · wall time: 783 ms · instructions: 7.2 G · max rss memory: 119.4 MB
stderr:
evmlean: reject (decl 9, value/type mismatch); gas=3714117
Test "tutorial/096_ruleKAcc"
Expected: ✋ reject · Size: 12.8 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rule k should not fire for Acc.
Test result: ✋ rejected · exit code 1 · wall time: 1.4 s · instructions: 14.5 G · max rss memory: 120.0 MB
stderr:
evmlean: reject (decl 13, value/type mismatch); gas=11849716
Test "tutorial/097_aNatLit"
Expected: 👍 accept · Size: 3.0 KB · Lines: 54 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Type checking Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 509 ms · instructions: 4.3 G · max rss memory: 121.8 MB
stderr:
evmlean: accept (decl 6, ok); gas=801269
Test "tutorial/098_natLitEq"
Expected: 👍 accept · Size: 6.1 KB · Lines: 114 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reducing Nat literals
Test result: 👍 accepted · exit code 0 · wall time: 726 ms · instructions: 6.6 G · max rss memory: 121.6 MB
stderr:
evmlean: accept (decl 10, ok); gas=3184310
Test "tutorial/099_proofIrrelevance"
Expected: 👍 accept · Size: 5.0 KB · Lines: 100 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Proof irrelevance: every Prop is a subsingleton, if p : Prop then all elements of p
are definitionally equal.
Test result: 👍 accepted · exit code 0 · wall time: 685 ms · instructions: 6.0 G · max rss memory: 120.9 MB
stderr:
evmlean: accept (decl 6, ok); gas=2711062
Test "tutorial/100_proofIrrelevanceBad"
Expected: ✋ reject · Size: 4.7 KB · Lines: 93 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Proof irrelevance is limited to Prop: if p : Type, then all elements of p are not
definitionally equal.
Test result: ✋ rejected · exit code 1 · wall time: 686 ms · instructions: 6.0 G · max rss memory: 121.3 MB
stderr:
evmlean: reject (decl 5, value/type mismatch); gas=2765039
Test "tutorial/101_proofIrrelevanceWhnf"
Expected: 👍 accept · Size: 5.6 KB · Lines: 112 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Proof irrelevance: if p : A and A is definitionally equal to Prop, then all elements of p
are still definitionally equal. Just applying proof irrelevance at Sort 0 isn't sufficient.
Test result: 👍 accepted · exit code 0 · wall time: 689 ms · instructions: 6.3 G · max rss memory: 122.2 MB
stderr:
evmlean: accept (decl 7, ok); gas=2980677
Test "tutorial/102_unitEta1"
Expected: 👍 accept · Size: 6.2 KB · Lines: 116 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 692 ms · instructions: 6.4 G · max rss memory: 120.0 MB
stderr:
evmlean: accept (decl 11, ok); gas=2951074
Test "tutorial/103_unitEta2"
Expected: 👍 accept · Size: 6.0 KB · Lines: 109 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 694 ms · instructions: 6.3 G · max rss memory: 121.5 MB
stderr:
evmlean: accept (decl 10, ok); gas=2914815
Test "tutorial/104_unitEta3"
Expected: 👍 accept · Size: 6.0 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Unit eta
Test result: 👍 accepted · exit code 0 · wall time: 745 ms · instructions: 6.3 G · max rss memory: 119.6 MB
stderr:
evmlean: accept (decl 10, ok); gas=2940260
Test "tutorial/105_structEta"
Expected: 👍 accept · Size: 12.5 KB · Lines: 230 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Structure eta
Test result: 👍 accepted · exit code 0 · wall time: 1.3 s · instructions: 12.9 G · max rss memory: 119.3 MB
stderr:
evmlean: accept (decl 16, ok); gas=10004099
Test "tutorial/106_funEta"
Expected: 👍 accept · Size: 5.2 KB · Lines: 104 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for non-dependent functions.
Test result: 👍 accepted · exit code 0 · wall time: 691 ms · instructions: 6.2 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=2794480
Test "tutorial/107_funEtaDep"
Expected: 👍 accept · Size: 5.3 KB · Lines: 106 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Function eta for dependent functions (pi types).
Test result: 👍 accepted · exit code 0 · wall time: 710 ms · instructions: 6.2 G · max rss memory: 121.2 MB
stderr:
evmlean: accept (decl 6, ok); gas=2878102
Test "tutorial/108_funEtaBad"
Expected: ✋ reject · Size: 4.9 KB · Lines: 97 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Eta should not identify functions with different bodies.
Test result: ✋ rejected · exit code 1 · wall time: 706 ms · instructions: 6.7 G · max rss memory: 121.9 MB
stderr:
evmlean: reject (decl 4, value/type mismatch); gas=3194318
Test "tutorial/109_etaRuleK"
Expected: ✋ reject · Size: 6.5 KB · Lines: 121 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied recursor with rule k and a free variable trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 807 ms · instructions: 7.3 G · max rss memory: 122.7 MB
stderr:
evmlean: reject (decl 9, value/type mismatch); gas=3930760
Test "tutorial/110_etaCtor"
Expected: ✋ reject · Size: 9.0 KB · Lines: 148 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Corner case for function eta: Does a defeq between a partially applied constructor trigger eta expansion?
Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.
Test result: ✋ rejected · exit code 1 · wall time: 803 ms · instructions: 7.5 G · max rss memory: 119.4 MB
stderr:
evmlean: reject (decl 18, value/type mismatch); gas=4015857
Test "tutorial/111_reflOccLeft"
Expected: ✋ reject · Size: 3.7 KB · Lines: 61 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence on the left of an arrow, behind further arrows inside a constructor argument.
The constructor argument is a function type Nat → (I → Nat).
Test result: ✋ rejected · exit code 1 · wall time: 508 ms · instructions: 4.4 G · max rss memory: 122.5 MB
stderr:
evmlean: reject (decl 5, positivity violation); gas=862059
Test "tutorial/112_reflOccInIndex"
Expected: ✋ reject · Size: 4.0 KB · Lines: 66 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Rejection: recursive occurrence in index position, behind a further arrow.
We build an indexed inductive I : Type → Type with a constructor argument
Nat → I (I α), so the recursive occurrence appears as an index argument.
Test result: ✋ rejected · exit code 1 · wall time: 512 ms · instructions: 4.4 G · max rss memory: 120.5 MB
stderr:
evmlean: reject (decl 5, application argument type mismatch); gas=877471
Test "tutorial/113_reduceCtorParamRefl.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 628 ms · instructions: 5.7 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 6, ok); gas=2186555
Test "tutorial/114_reduceCtorParamRefl2.mk"
Expected: 👍 accept · Size: 4.5 KB · Lines: 88 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.
Test result: 👍 accepted · exit code 0 · wall time: 629 ms · instructions: 5.6 G · max rss memory: 122.0 MB
stderr:
evmlean: accept (decl 6, ok); gas=2125836
Test "tutorial/115_rTreeRec"
Expected: 👍 accept · Size: 5.5 KB · Lines: 91 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of the generated recursor.
Test result: 👍 accepted · exit code 0 · wall time: 643 ms · instructions: 5.8 G · max rss memory: 122.2 MB
stderr:
evmlean: accept (decl 11, ok); gas=2309277
Test "tutorial/116_rtreeRecReduction"
Expected: 👍 accept · Size: 10.8 KB · Lines: 193 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of RTree.rec on RTree.mk.
Test result: 👍 accepted · exit code 0 · wall time: 886 ms · instructions: 8.5 G · max rss memory: 119.8 MB
stderr:
evmlean: accept (decl 17, ok); gas=5083677
Test "tutorial/117_accRecType"
Expected: 👍 accept · Size: 7.5 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Acc.rec.
Test result: 👍 accepted · exit code 0 · wall time: 1.5 s · instructions: 15.4 G · max rss memory: 120.6 MB
stderr:
evmlean: accept (decl 5, ok); gas=13076413
Test "tutorial/118_accRecReduction"
Expected: 👍 accept · Size: 13.4 KB · Lines: 252 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec reduces on Acc.intro.
Test result: 👍 accepted · exit code 0 · wall time: 1.6 s · instructions: 16.4 G · max rss memory: 119.7 MB
stderr:
evmlean: accept (decl 14, ok); gas=13809024
Test "tutorial/119_accRecNoEta"
Expected: ✋ reject · Size: 13.0 KB · Lines: 244 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Acc.rec does not have structure eta.
Test result: ✋ rejected · exit code 1 · wall time: 1.5 s · instructions: 14.5 G · max rss memory: 120.2 MB
stderr:
evmlean: reject (decl 13, value/type mismatch); gas=11852310
Test "tutorial/120_quotMkType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 123 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 893 ms · instructions: 8.6 G · max rss memory: 120.2 MB
stderr:
evmlean: accept (decl 9, ok); gas=5324486
Test "tutorial/121_quotIndType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.ind.
Test result: 👍 accepted · exit code 0 · wall time: 935 ms · instructions: 8.8 G · max rss memory: 119.7 MB
stderr:
evmlean: accept (decl 9, ok); gas=5480738
Test "tutorial/122_quotLiftType"
Expected: 👍 accept · Size: 6.3 KB · Lines: 124 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.lift.
Test result: 👍 accepted · exit code 0 · wall time: 1.1 s · instructions: 10.4 G · max rss memory: 122.3 MB
stderr:
evmlean: accept (decl 9, ok); gas=7361785
Test "tutorial/123_quotSoundType"
Expected: 👍 accept · Size: 7.2 KB · Lines: 141 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Asserting the type of Quot.sound.
Test result: 👍 accepted · exit code 0 · wall time: 978 ms · instructions: 8.9 G · max rss memory: 121.5 MB
stderr:
evmlean: accept (decl 10, ok); gas=5834310
Test "tutorial/124_quotLiftReduction"
Expected: 👍 accept · Size: 7.8 KB · Lines: 153 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.lift on Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 1.0 s · instructions: 9.7 G · max rss memory: 119.9 MB
stderr:
evmlean: accept (decl 9, ok); gas=6471708
Test "tutorial/125_quotIndReduction"
Expected: 👍 accept · Size: 7.6 KB · Lines: 151 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Reduction behavior of Quot.ind on Quot.mk.
Test result: 👍 accepted · exit code 0 · wall time: 1.0 s · instructions: 9.7 G · max rss memory: 116.3 MB
stderr:
evmlean: accept (decl 9, ok); gas=6620214
Test "tutorial/126_dup_defs"
Expected: ✋ reject · Size: 479 B · Lines: 7 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Two definitions with the same name
Test result: ✋ rejected · exit code 1 · wall time: 463 ms · instructions: 3.4 G · max rss memory: 121.8 MB
stderr:
evmlean: reject (decl 1, duplicate name); gas=166442
Test "tutorial/127_dup_ind_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 417 ms · instructions: 3.5 G · max rss memory: 117.1 MB
stderr:
evmlean: reject (decl 1, duplicate name); gas=196861
Test "tutorial/128_dup_ctor_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a constructor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 435 ms · instructions: 3.4 G · max rss memory: 120.5 MB
stderr:
evmlean: reject (decl 1, duplicate name); gas=205220
Test "tutorial/129_dup_rec_def"
Expected: ✋ reject · Size: 1.7 KB · Lines: 27 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A definition and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 426 ms · instructions: 3.5 G · max rss memory: 121.4 MB
stderr:
evmlean: reject (decl 1, duplicate name); gas=222174
Test "tutorial/130_misnamed_rec_user"
Expected: ✋ reject · Size: 2.0 KB · Lines: 33 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
The name of the recursor for misnamed_rec must be misnamed_rec.rec:
another name (like misnamed_rec.not_rec) should be rejected.
dupRecUser is included so that checkers that recreate the recursor (as misnamed_rec.rec)
rather than validating it still fail, because misnamed_rec_user references misnamed_rec.not_rec.
Test result: ✋ rejected · exit code 1 · wall time: 447 ms · instructions: 3.5 G · max rss memory: 122.0 MB
stderr:
evmlean: reject (decl 0, recursor shape); gas=223210
Test "tutorial/131_dup_rec_def2"
Expected: ✋ reject · Size: 1.7 KB · Lines: 28 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
Even if a kernel doesn't catch a recursor for dup_rec_def2 that is misnamed
as dup_rec_def2.not_rec, it should catch some other constant being given
the name dup_rec_def2.rec that is reserved for the recursor.
Test result: ✋ rejected · exit code 1 · wall time: 425 ms · instructions: 3.5 G · max rss memory: 121.4 MB
stderr:
evmlean: reject (decl 1, recursor shape); gas=225243
Test "tutorial/132_dup_ctor_rec"
Expected: ✋ reject · Size: 1.5 KB · Lines: 24 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
A constructor and a recursor with the same name
Test result: ✋ rejected · exit code 1 · wall time: 456 ms · instructions: 3.5 G · max rss memory: 121.2 MB
stderr:
evmlean: reject (decl 0, duplicate name); gas=208901
Test "tutorial/133_DupConCon"
Expected: ✋ reject · Size: 2.2 KB · Lines: 35 · lean4export: 3.1.0 · Lean: 4.27.0-rc1 · 📄 Declaration · 🔗 Source
An inductive with two constructors with the same name
Test result: ✋ rejected · exit code 1 · wall time: 429 ms · instructions: 3.6 G · max rss memory: 122.0 MB
stderr:
evmlean: reject (decl 0, duplicate name); gas=217252