Test "perf/discarded-argument"
Expected: 👍 accept · Size: 15.9 KB · Lines: 367 · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 50.0 s · 📄 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.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 1 ms | (÷223) | 40.3 MB | (-39%) | |
| mathgraph | 👍 | 1 ms | (÷221) | 35.7 MB | (-46%) | |
| nanoclo | 👍 | 2 ms | (÷76) | 45.4 MB | (-31%) | |
| con-ron | 👍 | 28 ms | (÷5.9) | 61.2 MB | (-7%) | |
| nanobruijn | 👍 | 4 ms | (÷38) | 10.4 MB | (÷6.3) | |
| nanoda | 👍 | 5 ms | (÷34) | 3.3 MB | (÷20) | |
| lazylean | 👍 | 10 ms | (÷17) | 25.0 MB | (÷2.6) | |
| con-leche | 👍 | 14 ms | (÷12) | 22.2 MB | (÷3.0) | |
| eink0rn | 👍 | 90 ms | (-46%) | 49.4 MB | (-25%) | |
| official | 👍 | 166 ms | (0%) | 65.7 MB | (0%) | |
| ind-models | 👍 | 239 ms | (+44%) | 105.6 MB | (+61%) | |
| lean4lean | 👍 | 1.2 s | (×7.4) | 99.1 MB | (+51%) | |
| tenet | 👍 | 153 ms | (-7%) | 49.8 MB | (-24%) | |
| tenet-hs | 👍 | 10 ms | (÷16) | 25.4 MB | (÷2.6) | |
| lean4cobol | 👍 | 3.8 s | (×23) | 16.5 MB | (÷4.0) | |
| evmlean | 🚫 | 1.9 s | 277.2 MB | |||
| mini | 👍 | 37 ms | (÷4.5) | 75.2 MB | (+14%) | |
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 👍 | 52 ms | (÷3.2) | 71.7 MB | (+9%) | |
| tenet-jvm | 👍 | 443 ms | (×2.7) | 102.1 MB | (+55%) | |
| nanoclo-fortran | 👍 | 3 ms | (÷48) | 4.9 MB | (÷14) | |
| kiota | 👍 | 5 ms | (÷32) | 11.5 MB | (÷5.7) | |
| metalean-fast | 👍 | 205 ms | (+24%) | 73.8 MB | (+12%) | |
| canonical-min | 🚫 | 388 ms | 1.1 GB | |||
| rpylean | 👍 | 262 ms | (+58%) | 37.2 MB | (-43%) | |
| vow-lean-kernel | 👍 | 7.3 s | (×44) | 17.1 MB | (÷3.8) | |
| parse-only | 👍 | 28 ms | (÷5.9) | 65.7 MB | (0%) |