Commit 0efe3294 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove superflous brackers.

parent 79bf7df8
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment