diff --git a/heap_lang/tests.v b/heap_lang/tests.v index 28df58ed1b91cd01e259c26ef790a9b7a93f6954..c6745e3aba8cb904af068ded043287d56d281275 100644 --- a/heap_lang/tests.v +++ b/heap_lang/tests.v @@ -55,9 +55,9 @@ Module LiftingTests. Qed. Definition FindPred : val := - λ: "x", (rec: "pred" "y" := + λ: "x", rec: "pred" "y" := let: "yp" := "y" + '1 in - if "yp" < "x" then "pred" "yp" else "y"). + if "yp" < "x" then "pred" "yp" else "y". Definition Pred : val := λ: "x", if "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.