Matching.scala

import leon.Utils._

object Matching {
    def t1(a: NatList) = choose( (x: Nat) => Cons(x, Nil()) == a)

  abstract class Nat
  case class Z() extends Nat
  case class Succ(n: Nat) extends Nat

  abstract class NatList
  case class Nil() extends NatList
  case class Cons(head: Nat, tail: NatList) extends NatList
}