summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon HO2024-05-28 18:50:52 +0200
committerGitHub2024-05-28 18:50:52 +0200
commit95cb0eee7f9af0a0fd0d24a2531b5395b98b861f (patch)
tree4f8cea8688c85603ca250afa0b581aa4b96289ee /tests/lean
parentef7792c106a1f33397c206fcb5124b5ddfe64378 (diff)
parentae075db15638ee8878bebe3d31affb1aa320e90f (diff)
Merge pull request #219 from AeneasVerif/son/infinite
Fix the infinite loop test
Diffstat (limited to '')
-rw-r--r--tests/lean/InfiniteLoop.lean25
1 files changed, 25 insertions, 0 deletions
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