From 60ee8c2f76e55c924cb6d76e284a4643d3239a9b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 25 Apr 2025 17:02:23 -0700
Subject: [PATCH] chore: broken test after update stage0 (#8110)

This is a temporary fix for `master` after update stage0 breakage.

cc @Kha @nomeata
---
 tests/lean/run/issue7408.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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