From 6d108adb356845c74e20eecfa3a80a18f89eb80f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 15 Apr 2015 20:55:10 +0200
Subject: [PATCH] Fix test for Church.Squared
---
src/test/resources/regression/synthesis/Church/Squared.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 32b05900f..d660c247e 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -14,6 +14,11 @@ object Numerals {
}
} ensuring (_ >= 0)
+ def add(x: Num, y: Num): Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
def mult(x: Num, y: Num): Num = (y match {
case S(p) =>
add(mult(x, p), x)
--
GitLab