From 5d6c27db10ce286eb596c55b937eabff96029417 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Thu, 27 Feb 2025 12:03:13 -0500 Subject: [PATCH] add: test case for pred->fun/fun->pred recursive --- forge/tests/forge/other/recursive-error.frg | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/forge/tests/forge/other/recursive-error.frg b/forge/tests/forge/other/recursive-error.frg index c126a9f6..363869d9 100644 --- a/forge/tests/forge/other/recursive-error.frg +++ b/forge/tests/forge/other/recursive-error.frg @@ -53,7 +53,9 @@ fun h[a: A]: one A { h[a] } fun f[a: A]: one A { g[a] } fun g[a: A]: one A { f[a] } - +// cycle between a function and a predicate +fun i[a: A]: one A { some {b: A | j[b]} } +pred j[a: A] { some i[a] } @@ -73,4 +75,7 @@ test expect { recur_fun_2loop: {some a: A | f[a]} is forge_error "f eventually called itself" recur_fun_self: {some a: A | h[a]} is forge_error "h eventually called itself" + + recur_pred_fun: {some a: A | j[a]} is forge_error "j eventually called itself" + recur_fun_pred: {some a: A | some i[a]} is forge_error "i eventually called itself" } \ No newline at end of file