From 0efe329423f0073cf41746d7664da8d87b6b7e92 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 11 Feb 2016 23:22:18 +0100 Subject: [PATCH] Remove superflous brackers. --- heap_lang/tests.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heap_lang/tests.v b/heap_lang/tests.v index 28df58ed1..c6745e3ab 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. -- GitLab