From b0289e1fc7ead63638e694d12cf89f0fe76a8571 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Fri, 25 Sep 2015 12:16:18 +0200
Subject: [PATCH] additional regression test for unapply patterns
---
.../verification/isabelle/valid/Unapply.scala | 15 +++++++++++++++
1 file changed, 15 insertions(+)
create mode 100644 src/test/resources/regression/verification/isabelle/valid/Unapply.scala
diff --git a/src/test/resources/regression/verification/isabelle/valid/Unapply.scala b/src/test/resources/regression/verification/isabelle/valid/Unapply.scala
new file mode 100644
index 000000000..8a00fd5db
--- /dev/null
+++ b/src/test/resources/regression/verification/isabelle/valid/Unapply.scala
@@ -0,0 +1,15 @@
+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object Unapply {
+
+ @isabelle.proof(method = """(cases "<var xs>", auto)""")
+ def check[A](xs: List[A]) = {
+ xs match {
+ case Nil() => true
+ case _ :: _ => true
+ }
+ }.holds
+
+}
--
GitLab