From 31f639b0578e3332ad89363bfc5164c23495dbdf Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 22 Oct 2012 18:56:41 +0200
Subject: [PATCH] One GROUND example that uses a rec. fun.

---
 testcases/Choose.scala | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/testcases/Choose.scala b/testcases/Choose.scala
index 09f606b21..85b6225d7 100644
--- a/testcases/Choose.scala
+++ b/testcases/Choose.scala
@@ -13,4 +13,17 @@ object ChooseTest {
   def c4(a: Int): (Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int) => x1 > a && x2 > a }
   def c5(a: Int): (Int, Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int) => x1 > a && x2 > a }
 
+
+  sealed abstract class List
+  case class Nil() extends List
+  case class Cons(head : Int, tail : List) extends List
+
+  def size(lst : List) : Int = (lst match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def k0() : List = choose {
+    (l : List) => size(l) == 1
+  }
 }
-- 
GitLab