diff --git a/tests/lean/run/issue7408.lean b/tests/lean/run/issue7408.lean index 45e7c32e2a..d00e4f6bff 100644 --- a/tests/lean/run/issue7408.lean +++ b/tests/lean/run/issue7408.lean @@ -1,7 +1,8 @@ def computeFuel (mass : Nat) : Nat := let rec go acc cur := let n := cur / 3 - 2 - if n = 0 then acc + cur else go (acc + cur) n + -- TODO: investigate why we need `_ :` + if _ : n = 0 then acc + cur else go (acc + cur) n termination_by cur go 0 mass - mass