From 3d4db11f536440b11a6a7c41127974824d48201b Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Sat, 15 Dec 2012 17:40:29 +0100
Subject: [PATCH] Example of solution for Church numeral example
---
testcases/synthesis/ChurchNumerals.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
index 229d79945..287e4ecef 100644
--- a/testcases/synthesis/ChurchNumerals.scala
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -18,4 +18,9 @@ object ChurchNumerals {
value(r) == value(x) + value(y)
}
}
+
+ def workingAdd(x : Num, y : Num) : Num = (x match {
+ case Zero() => y
+ case Succ(p) => workingAdd(p, Succ(y))
+ }) ensuring (value(_) == value(x) + value(y))
}
--
GitLab