Test "perf/folded-constant-last"
Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 3 ms | (÷16) | 47.1 MB | (-32%) | |
| mathgraph | 👍 | 3 ms | (÷16) | 48.3 MB | (-30%) | |
| nanoclo | 👍 | 4 ms | (÷11) | 54.6 MB | (-21%) | |
| con-ron | 👍 | 32 ms | (-21%) | 69.3 MB | (0%) | |
| nanobruijn | 👍 | 7 ms | (÷5.8) | 13.5 MB | (÷5.1) | |
| nanoda | 👍 | 7 ms | (÷5.8) | 4.4 MB | (÷16) | |
| lazylean | 👍 | 5 ms | (÷8.4) | 26.8 MB | (÷2.6) | |
| con-leche | 👍 | 21 ms | (-47%) | 24.4 MB | (÷2.8) | |
| eink0rn | 👍 | 6 ms | (÷7.1) | 18.6 MB | (÷3.7) | |
| official | 👍 | 41 ms | (0%) | 69.0 MB | (0%) | |
| ind-models | 👍 | 121 ms | (×3.0) | 110.5 MB | (+60%) | |
| lean4lean | 👍 | 47 ms | (+15%) | 99.6 MB | (+44%) | |
| tenet | 👍 | 160 ms | (×3.9) | 52.2 MB | (-24%) | |
| tenet-hs | 👍 | 13 ms | (÷3.2) | 31.5 MB | (÷2.2) | |
| lean4cobol | 👍 | 182 ms | (×4.5) | 28.0 MB | (÷2.5) | |
| evmlean | 🚫 | 2.8 s | 286.8 MB | |||
| mini | ⌛ | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 👍 | 860 ms | (×21) | 768.7 MB | (×11) | |
| tenet-jvm | 👍 | 273 ms | (×6.7) | 76.4 MB | (+11%) | |
| nanoclo-fortran | 👍 | 9 ms | (÷4.4) | 8.2 MB | (÷8.5) | |
| kiota | 👍 | 8 ms | (÷5.1) | 18.6 MB | (÷3.7) | |
| metalean-fast | 👍 | 52 ms | (+27%) | 83.3 MB | (+21%) | |
| canonical-min | 🚫 | 390 ms | 1.1 GB | |||
| rpylean | 👍 | 7 ms | (÷5.5) | 16.1 MB | (÷4.3) | |
| vow-lean-kernel | 👍 | 216 ms | (×5.3) | 22.5 MB | (÷3.1) | |
| parse-only | 👍 | 30 ms | (-25%) | 65.9 MB | (-4%) |