summaryrefslogtreecommitdiff
path: root/tests/lean/InfiniteLoop.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/InfiniteLoop.lean')
-rw-r--r--tests/lean/InfiniteLoop.lean7
1 files changed, 5 insertions, 2 deletions
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
index 9eb8e22c..b5986ed8 100644
--- a/tests/lean/InfiniteLoop.lean
+++ b/tests/lean/InfiniteLoop.lean
@@ -2,6 +2,9 @@
-- [infinite_loop]
import Base
open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
namespace infinite_loop
@@ -19,7 +22,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