diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala index 32b05900f7c4527287b5f92f24bb8c053899b484..d660c247ea4c68993dd4d59a7fc0f61e913935bc 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)