diff --git a/testcases/synthesis/io-examples/Lists.scala b/testcases/synthesis/io-examples/Lists.scala new file mode 100644 index 0000000000000000000000000000000000000000..62335cc362ded88ec3118a8456e91a2a102d6d8f --- /dev/null +++ b/testcases/synthesis/io-examples/Lists.scala @@ -0,0 +1,22 @@ +import leon.lang._ +import leon.collection._ +import leon.lang.synthesis._ + +object Lists { + + def safetail(l: List[Int]): List[Int] = choose { (res : List[Int]) => + passes(l, res)(Map( + Cons(1, Cons(2, Cons(3, Cons(4, Nil())))) -> Cons(2, Cons(3, Cons(4, Nil()))), + Cons(2, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())), + Nil() -> Nil() + )) + } + + def uniq(l: List[Int]): List[Int] = choose { (res : List[Int]) => + passes(l, res)(Map( + Cons(1, Cons(1, Cons(1, Cons(2, Nil())))) -> Cons(1, Cons(2, Nil())), + Cons(3, Cons(3, Cons(4, Nil()))) -> Cons(3, Cons(4, Nil())), + Nil() -> Nil() + )) + } +}