Test "perf/args-before-unfold"
Expected: 👍 accept · Size: 44.5 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 50.0 s · 📄 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.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 2 ms | (÷23) | 45.3 MB | (-32%) | |
| mathgraph | 👍 | 2 ms | (÷22) | 44.4 MB | (-33%) | |
| nanoclo | 👍 | 3 ms | (÷14) | 46.4 MB | (-30%) | |
| con-ron | 👍 | 28 ms | (-22%) | 64.2 MB | (-3%) | |
| nanobruijn | 👍 | 5 ms | (÷7.8) | 11.8 MB | (÷5.6) | |
| nanoda | 👍 | 4 ms | (÷8.4) | 4.0 MB | (÷17) | |
| lazylean | 👍 | 5 ms | (÷6.6) | 24.8 MB | (÷2.7) | |
| con-leche | 👍 | 15 ms | (÷2.4) | 23.2 MB | (÷2.9) | |
| eink0rn | 👍 | 4 ms | (÷8.5) | 16.4 MB | (÷4.1) | |
| official | 👍 | 36 ms | (0%) | 66.4 MB | (0%) | |
| ind-models | 👍 | 112 ms | (×3.1) | 109.0 MB | (+64%) | |
| lean4lean | 👍 | 43 ms | (+19%) | 98.4 MB | (+48%) | |
| tenet | 👍 | 146 ms | (×4.1) | 49.5 MB | (-25%) | |
| tenet-hs | 👍 | 9 ms | (÷4.1) | 22.5 MB | (÷3.0) | |
| lean4cobol | 👍 | 118 ms | (×3.3) | 20.6 MB | (÷3.2) | |
| evmlean | 🚫 | 2.2 s | 264.7 MB | |||
| mini | ⌛ | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 👍 | 2.3 s | (×63) | 1.6 GB | (×25) | |
| tenet-jvm | 👍 | 258 ms | (×7.2) | 73.8 MB | (+11%) | |
| nanoclo-fortran | 👍 | 7 ms | (÷5.4) | 7.6 MB | (÷8.8) | |
| kiota | 👍 | 6 ms | (÷5.9) | 16.5 MB | (÷4.0) | |
| metalean-fast | 👍 | 44 ms | (+21%) | 82.2 MB | (+24%) | |
| canonical-min | 🚫 | 389 ms | 1.1 GB | |||
| rpylean | 👍 | 5 ms | (÷6.9) | 12.7 MB | (÷5.2) | |
| vow-lean-kernel | 👍 | 146 ms | (×4.1) | 11.0 MB | (÷6.0) | |
| parse-only | 👍 | 30 ms | (-17%) | 65.5 MB | (-1%) |