chore: broken test after update stage0

2026-03-20 03:44:10 +00:00 · 2025-04-25 16:41:43 -07:00
1 changed files with 2 additions and 1 deletions
--- 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