From ae075db15638ee8878bebe3d31affb1aa320e90f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 28 May 2024 18:05:01 +0200
Subject: Reactivate the infinite-loop.rs test

---
 tests/lean/InfiniteLoop.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 tests/lean/InfiniteLoop.lean

(limited to 'tests/lean')

diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
new file mode 100644
index 00000000..9eb8e22c
--- /dev/null
+++ b/tests/lean/InfiniteLoop.lean
@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [infinite_loop]
+import Base
+open Primitives
+
+namespace infinite_loop
+
+/- [infinite_loop::bar]:
+   Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 -/
+def bar : Result Unit :=
+  Result.ok ()
+
+/- [infinite_loop::foo]: loop 0:
+   Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 -/
+divergent def foo_loop : Result Unit :=
+  do
+  let _ ← bar
+  foo_loop
+
+/- [infinite_loop::foo]:
+   Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
+def foo : Result Unit :=
+  foo_loop
+
+end infinite_loop
-- 
cgit v1.2.3