Test "perf/discarded-argument"
Expected: 馃憤 accept 路 Size: 15.9鈥疜B 路 Lines: 367 路 lean4export: 3.1.0 路 Lean: 4.29.1 路 馃搫 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 | 鈴憋笍 | 馃 | |||
|---|---|---|---|---|---|---|
| mathgraph | 馃憤 | 1鈥痬s | (梅485) | 37.9鈥疢B | (-40%) | |
| ind-models | 馃憤 | 695鈥痬s | (+5%) | 101.1鈥疢B | (+59%) | |
| official-nightly | 馃憤 | 167鈥痬s | (梅4.0) | 63.9鈥疢B | (0%) | |
| evmlean | 馃毇 | 1.3鈥痵 | 133.0鈥疢B | |||
| nanoda | 馃憤 | 32鈥痬s | (梅21) | 3.4鈥疢B | (梅19) | |
| mini | 馃憤 | 37鈥痬s | (梅18) | 74.5鈥疢B | (+17%) | |
| lean4lean | 馃憤 | 1.2鈥痵 | (+85%) | 100.0鈥疢B | (+57%) | |
| sokonanoda | 馃憤 | 1鈥痬s | (梅484) | 37.9鈥疢B | (-40%) | |
| zignodamus | 馃憤 | 11鈥痬s | (梅62) | 11.9鈥疢B | (梅5.3) | |
| nanoclo | 馃憤 | 2鈥痬s | (梅283) | 47.6鈥疢B | (-25%) | |
| nanobruijn | 馃憤 | 21鈥痬s | (梅31) | 10.7鈥疢B | (梅5.9) | |
| kiota | 馃憤 | 4鈥痬s | (梅183) | 13.0鈥疢B | (梅4.9) | |
| official | 馃憤 | 661鈥痬s | (0%) | 63.6鈥疢B | (0%) | |
| vow-lean-kernel | 馃憤 | 7.3鈥痵 | (脳11) | 16.8鈥疢B | (梅3.8) | |
| rpylean | 馃憤 | 288鈥痬s | (梅2.3) | 41.1鈥疢B | (-35%) | |
| official-v4.28.0 | 馃憤 | 740鈥痬s | (+12%) | 72.8鈥疢B | (+14%) | |
| still-nanoda | 馃憤 | 31鈥痬s | (梅21) | 3.3鈥疢B | (梅20) | |
| nyaya | 馃挜 | 1.7鈥痬 | 16.2鈥疢B | |||
| parse-only | 馃憤 | 28鈥痬s | (梅24) | 62.4鈥疢B | (-2%) |