blob: 8b52731a597aa5a280c539d30d5a6748e04a0822 (
plain) (
tree)
|
|
sealed trait Nat
sealed trait Succ[Prev <: Nat] extends Nat
sealed trait Zero extends Nat
case class ToInt[N <: Nat](value: Int)
object ToInt {
implicit val caseZero: ToInt[Zero] = ToInt(0)
implicit def caseSucc[Prev <: Nat](implicit e: ToInt[Prev]): ToInt[Succ[Prev]] = ToInt(e.value + 1)
}
object Test {
def main(args: Array[String]): Unit = {
assert(implicitly[ToInt[Zero]].value == 0)
assert(implicitly[ToInt[Succ[Zero]]].value == 1)
assert(implicitly[ToInt[Succ[Succ[Zero]]]].value == 2)
assert(implicitly[ToInt[Succ[Succ[Succ[Zero]]]]].value == 3)
assert(implicitly[ToInt[Succ[Succ[Succ[Succ[Zero]]]]]].value == 4)
assert(implicitly[ToInt[Succ[Succ[Succ[Succ[Succ[Zero]]]]]]].value == 5)
}
}
|