Test "perf/folded-constant-last"
Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 50.0 s · 📄 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.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 3 ms | (÷16) | 48.4 MB | (-30%) | |
| sokonanoda | 👍 | 3 ms | (÷16) | 46.2 MB | (-33%) | |
| nanoclo | 👍 | 4 ms | (÷10) | 58.5 MB | (-15%) | |
| con-ron | 👍 | 32 ms | (-21%) | 71.1 MB | (+3%) | |
| lazylean | 👍 | 5 ms | (÷8.1) | 26.7 MB | (÷2.6) | |
| nanoda | 👍 | 7 ms | (÷5.8) | 4.4 MB | (÷16) | |
| nanobruijn | 👍 | 7 ms | (÷5.6) | 17.3 MB | (÷4.0) | |
| con-leche | 👍 | 21 ms | (-47%) | 34.6 MB | (-50%) | |
| eink0rn | 👍 | 6 ms | (÷6.8) | 18.1 MB | (÷3.8) | |
| ind-models | 👍 | 79 ms | (+94%) | 111.9 MB | (+62%) | |
| official | 👍 | 40 ms | (0%) | 69.1 MB | (0%) | |
| lean4lean | 👍 | 47 ms | (+15%) | 100.8 MB | (+46%) | |
| tenet | 👍 | 160 ms | (×3.9) | 51.3 MB | (-26%) | |
| nanoclo-fortran | 👍 | 9 ms | (÷4.4) | 8.1 MB | (÷8.6) | |
| lean4cobol | 👍 | 182 ms | (×4.5) | 27.6 MB | (÷2.5) | |
| evmlean | 🚫 | 2.3 s | 139.1 MB | |||
| mini | 💥 | 49.5 s | 90.2 MB | |||
| overfull | 💥 | 1.7 m | 49.0 MB | |||
| kiota | 👍 | 8 ms | (÷5.0) | 18.3 MB | (÷3.8) | |
| canonical-min | 🚫 | 390 ms | 1.1 GB | |||
| rpylean | 👍 | 7 ms | (÷5.5) | 15.9 MB | (÷4.3) | |
| vow-lean-kernel | 👍 | 216 ms | (×5.3) | 22.2 MB | (÷3.1) | |
| official-v4.28.0 | 👍 | 48 ms | (+19%) | 78.7 MB | (+14%) | |
| still-nanoda | 👍 | 7 ms | (÷5.9) | 4.4 MB | (÷16) | |
| nyaya | ✋ | 17 ms | 13.1 MB | |||
| parse-only | 👍 | 30 ms | (-26%) | 65.8 MB | (-5%) |