From 1021cdea98043dd935dbc8dbe633b90fda68047d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:15:26 +0200
Subject: Update the tests

---
 tests/lean/InfiniteLoop.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/InfiniteLoop.lean')

diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
index 9eb8e22c..b8c2343e 100644
--- a/tests/lean/InfiniteLoop.lean
+++ b/tests/lean/InfiniteLoop.lean
@@ -19,7 +19,7 @@ divergent def foo_loop : Result Unit :=
 
 /- [infinite_loop::foo]:
    Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
-def foo : Result Unit :=
-  foo_loop
+@[reducible] def foo : Result Unit :=
+               foo_loop
 
 end infinite_loop
-- 
cgit v1.2.3