Skip to content

Commit

Permalink
add: test case for pred->fun/fun->pred recursive
Browse files Browse the repository at this point in the history
  • Loading branch information
tnelson committed Feb 27, 2025
1 parent b84bf65 commit 5d6c27d
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion forge/tests/forge/other/recursive-error.frg
Original file line number Diff line number Diff line change
Expand Up @@ -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] }



Expand All @@ -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"
}

0 comments on commit 5d6c27d

Please sign in to comment.