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 0000000000000000000000000000000000000000..8a00fd5db94913f9540217b5e9132a5d4187c2a6 --- /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 + +}