Scala Type Level Programming: The Natural Numbers: Addition Assertions

type-level-programming-natural-numbers-addition-assertions.scala

  // 0 + 0, 0 + 1
  implicitly[MsbZero#add[MsbZero] =:= MsbZero]
  implicitly[MsbZero#add[MsbOne] =:= MsbOne]

  // 1 + 0, 1 + 1
  implicitly[MsbOne#add[MsbZero] =:= MsbOne]
  implicitly[MsbOne#add[MsbOne] =:= B0[MsbOne]]

  // 2 + 0, 2 + 1, 2 + 2
  implicitly[B0[MsbOne]#add[MsbZero] =:= B0[MsbOne]]
  implicitly[B0[MsbOne]#add[MsbOne] =:= B1[MsbOne]]
  implicitly[B0[MsbOne]#add[B0[MsbOne]] =:= B0[B0[MsbOne]]]

  implicitly[T2#add[T0] =:= T2]
  implicitly[T2#add[T1] =:= T3]
  implicitly[T2#add[T2] =:= T4]

  implicitly[T0#add[T2] =:= T2]
  implicitly[T1#add[T2] =:= T3]
  implicitly[T2#add[T2] =:= T4]

  implicitly[T3#add[T0] =:= T3]
  implicitly[T3#add[T1] =:= T4]
  implicitly[T3#add[T2] =:= T5]
  implicitly[T3#add[T3] =:= T6]

  implicitly[T5#add[T5] =:= T4#add[T6]]
  implicitly[T5#add[T5] =:= T6#add[T4]]
  implicitly[T5#add[T5] =:= T1#add[T2]#add[T3]#add[T4]]