This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 1^0 | |
implicitly[T1#exp[T0] =:= T1] | |
// 1^1 | |
implicitly[T1#exp[T1] =:= T1] | |
// 1^2 | |
implicitly[T1#exp[T2] =:= T1] | |
// 1^3 | |
implicitly[T1#exp[T3] =:= T1] | |
// 2^0 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sealed trait Nat { | |
type exp[That <: Nat] <: Nat | |
type expflip[That <: Nat] <: Nat | |
} | |
sealed trait MsbZero extends Nat { | |
override type exp[That <: Nat] = MsbZero | |
override type expflip[That <: Nat] = MsbOne | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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]] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sealed trait Nat { | |
type half <: Nat | |
type add[That <: Nat] <: Nat | |
// TODO: Better name | |
type coreT[That <: Nat] <: Nat | |
} | |
sealed trait MsbZero extends Nat { | |
override type half = MsbZero | |
override type add[That <: Nat] = That |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sealed trait Nat { | |
type inc <: Nat | |
type dbl <: Nat | |
type A = this.type#dbl#inc#dbl#dbl#inc#dbl | |
type B = this.type#dbl#inc#dbl#dbl#inc#dbl#inc | |
type C = this.type#dbl#inc#dbl#inc#dbl#dbl | |
type D = this.type#dbl#inc#dbl#inc#dbl#dbl#inc | |
type E = this.type#dbl#inc#dbl#inc#dbl#inc#dbl | |
type F = this.type#dbl#inc#dbl#inc#dbl#inc#dbl#inc |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 1 = O + 1 | |
implicitly[MsbOne =:= MsbZero#inc] | |
// 2 = O + 1 + 1 | |
implicitly[B0[MsbOne] =:= MsbZero#inc#inc] | |
// 3 = O + 1 + 1 + 1 | |
implicitly[B1[MsbOne] =:= MsbZero#inc#inc#inc] | |
// 4 = O + 1 + 1 + 1 + |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sealed trait Nat { | |
type inc <: Nat | |
type dbl <: Nat | |
} | |
sealed trait MsbZero extends Nat { | |
override type inc = MsbOne | |
override type dbl = MsbZero | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 2 x 3 5 x 7 x 11 x 13 x 17 = 510510 | |
type T510 = T5#mult[T10]#add[T1]#mult[T10] | |
type T510510 = T510#mult[T1000]#add[T510] | |
implicitly[T2#mult[T3]#mult[T5]#mult[T7]#mult[T11]#mult[T13]#mult[T17] =:= T510510] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
implicitly[MsbZero#mult[MsbZero] =:= MsbZero] | |
implicitly[MsbZero#mult[MsbOne] =:= MsbZero] | |
implicitly[MsbOne#mult[MsbZero] =:= MsbZero] | |
implicitly[MsbOne#mult[MsbOne] =:= MsbOne] | |
implicitly[T0#mult[T0] =:= T0] | |
implicitly[T0#mult[T2] =:= T0] | |
implicitly[T0#mult[T4] =:= T0] | |
implicitly[T1#mult[T0] =:= T0] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sealed trait Nat { | |
type mult[That <: Nat] <: Nat | |
} | |
sealed trait MsbZero extends Nat { | |
override type mult[That <: Nat] = MsbZero | |
} | |
sealed trait MsbOne extends Nat { | |
override type mult[That <: Nat] = That |
NewerOlder