Type level Integers. These are all base 10.
- data E = E
- data D0 n = D0 n
- data D1 n = D1 n
- data D2 n = D2 n
- data D3 n = D3 n
- data D4 n = D4 n
- data D5 n = D5 n
- data D6 n = D6 n
- data D7 n = D7 n
- data D8 n = D8 n
- data D9 n = D9 n
- class Succ x y | x -> y where
- tySucc :: x -> y
- class Pred x y | x -> y where
- tyPred :: x -> y
- class Add m n s | m n -> s where
- tyAdd :: m -> n -> s
- class SmallerThan x y
- class TyNum n
- class TypeNumberToInt ty where
- tyNumToInt :: ty -> Int
Documentation
Show E | |
Reverse' E a a | |
IncrementRightToLeft E (D1 E) | |
ListLength Nil (D0 E) | |
Pred m m' => Add m (D0 E) m | |
TypeNumberToInt (D0 E) | |
TyNum (D9 E) | |
TyNum (D8 E) | |
TyNum (D7 E) | |
TyNum (D6 E) | |
TyNum (D5 E) | |
TyNum (D4 E) | |
TyNum (D3 E) | |
TyNum (D2 E) | |
TyNum (D1 E) | |
TyNum (D0 E) | |
Pred y y' => SmallerThan (D0 E) y | |
Pred n n' => Add (D0 E) n n | |
StripLeadingZeros (D0 E) (D0 E) | |
Add (D0 E) (D0 E) (D0 E) | |
Elem (Cons res nxt) (D0 E) res |
D0 n |
ListLength Nil (D0 E) | |
Pred m m' => Add m (D0 E) m | |
Show n => Show (D0 n) | |
TypeNumberToInt (D0 E) | |
TyNum n => TyNum (D0 n) | |
TyNum (D0 E) | |
Pred y y' => SmallerThan (D0 E) y | |
StripLeadingZeros a b => StripLeadingZeros (D0 a) b | |
Pred n n' => Add (D0 E) n n | |
Reverse' n (D0 a) r => Reverse' (D0 n) a r | |
StripLeadingZeros (D0 E) (D0 E) | |
DecrementRightToLeft (D1 a) (D0 a) | |
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) | |
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) | |
IncrementRightToLeft (D0 a) (D1 a) | |
Add (D0 E) (D0 E) (D0 E) | |
Elem (Cons res nxt) (D0 E) res |
D1 n |
IncrementRightToLeft E (D1 E) | |
Show n => Show (D1 n) | |
TyNum n => TyNum (D1 n) | |
TyNum (D1 E) | |
Reverse' n (D1 a) r => Reverse' (D1 n) a r | |
StripLeadingZeros (D1 a) (D1 a) | |
DecrementRightToLeft (D2 a) (D1 a) | |
DecrementRightToLeft (D1 a) (D0 a) | |
IncrementRightToLeft (D1 a) (D2 a) | |
IncrementRightToLeft (D0 a) (D1 a) |
D2 n |
D3 n |
D4 n |
D5 n |
D6 n |
D7 n |
D8 n |
D9 n |
Show n => Show (D9 n) | |
TyNum n => TyNum (D9 n) | |
TyNum (D9 E) | |
Reverse' n (D9 a) r => Reverse' (D9 n) a r | |
StripLeadingZeros (D9 a) (D9 a) | |
DecrementRightToLeft (D9 a) (D8 a) | |
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) | |
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) | |
IncrementRightToLeft (D8 a) (D9 a) |
class Succ x y | x -> y whereSource
(Reverse a a', IncrementRightToLeft a' b', Reverse b' b) => Succ a b |
class Pred x y | x -> y whereSource
(Reverse a a', DecrementRightToLeft a' b', Reverse b' b'', StripLeadingZeros b'' b) => Pred a b |
class SmallerThan x y Source
(Pred x x', Pred y y', SmallerThan x' y') => SmallerThan x y | |
Pred y y' => SmallerThan (D0 E) y |
TyNum n => TyNum (D9 n) | |
TyNum (D9 E) | |
TyNum n => TyNum (D8 n) | |
TyNum (D8 E) | |
TyNum n => TyNum (D7 n) | |
TyNum (D7 E) | |
TyNum n => TyNum (D6 n) | |
TyNum (D6 E) | |
TyNum n => TyNum (D5 n) | |
TyNum (D5 E) | |
TyNum n => TyNum (D4 n) | |
TyNum (D4 E) | |
TyNum n => TyNum (D3 n) | |
TyNum (D3 E) | |
TyNum n => TyNum (D2 n) | |
TyNum (D2 E) | |
TyNum n => TyNum (D1 n) | |
TyNum (D1 E) | |
TyNum n => TyNum (D0 n) | |
TyNum (D0 E) |
class TypeNumberToInt ty whereSource
Convert a type-level number to an Int. Of course, we can only go this way...
tyNumToInt :: ty -> IntSource
(Pred a b, TypeNumberToInt b) => TypeNumberToInt a | |
TypeNumberToInt (D0 E) |