Test "perf/folded-constant-last"
Expected: 👍 accept · Size: 51.0 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 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 | (÷15) | 50.6 MB | (-25%) | |
| ind-models | 👍 | 78 ms | (+93%) | 108.0 MB | (+61%) | |
| official-nightly | 👍 | 41 ms | (+1%) | 68.3 MB | (+2%) | |
| evmlean | 🚫 | 2.3 s | 140.6 MB | |||
| nanoda | 👍 | 7 ms | (÷5.8) | 4.4 MB | (÷15) | |
| mini | 💥 | 1.1 m | 90.7 MB | |||
| lean4lean | 👍 | 47 ms | (+14%) | 101.0 MB | (+51%) | |
| sokonanoda | 👍 | 3 ms | (÷14) | 50.3 MB | (-25%) | |
| zignodamus | 👍 | 3 ms | (÷12) | 9.6 MB | (÷7.0) | |
| nanoclo | 👍 | 4 ms | (÷10) | 56.4 MB | (-16%) | |
| nanobruijn | 👍 | 7 ms | (÷5.8) | 14.4 MB | (÷4.7) | |
| kiota | 👍 | 7 ms | (÷6.2) | 13.5 MB | (÷5.0) | |
| official | 👍 | 41 ms | (0%) | 67.1 MB | (0%) | |
| vow-lean-kernel | 👍 | 216 ms | (×5.3) | 22.0 MB | (÷3.0) | |
| rpylean | 👍 | 8 ms | (÷5.0) | 19.9 MB | (÷3.4) | |
| official-v4.28.0 | 👍 | 48 ms | (+19%) | 75.7 MB | (+13%) | |
| still-nanoda | 👍 | 7 ms | (÷5.9) | 4.4 MB | (÷15) | |
| nyaya | ✋ | 17 ms | 13.5 MB | |||
| parse-only | 👍 | 30 ms | (-26%) | 62.3 MB | (-7%) |