Skip to content
Snippets Groups Projects
Commit b0289e1f authored by Lars Hupel's avatar Lars Hupel Committed by Etienne Kneuss
Browse files

additional regression test for unapply patterns

parent 715fe63a
No related branches found
No related tags found
No related merge requests found
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
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment