From 8ea8f2e7dac4fd6c7dd06ff913ea14f2a4fa98b4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 25 Sep 2015 12:15:40 +0200
Subject: [PATCH] An example for FunctionClosure with typed polym. functions
---
.../verification/xlang/valid/Nested15.scala | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/Nested15.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested15.scala b/src/test/resources/regression/verification/xlang/valid/Nested15.scala
new file mode 100644
index 000000000..490404f86
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested15.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.collection._
+object Nested1 {
+
+ def foo[A](i: List[A]): BigInt = {
+ val n = i
+ def rec1[B](j: List[B]) = j ++ j
+ def rec2[C](l: List[C], j: BigInt) = {
+ require(l.nonEmpty)
+ def rec3(k: C) = k :: rec1[C](l)
+ rec3(l.head).size + j + n.size + i.size
+ }
+ rec2(List(true, true, false), 2)
+ } ensuring(i.size + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et:
--
GitLab