diff --git a/Changes.md b/Changes.md
new file mode 100644
--- /dev/null
+++ b/Changes.md
@@ -0,0 +1,19 @@
+1.0:
+
+* Change representation of decimals to an inherently normalized form
+  that is symmetric with respect to positive and negative numbers.
+
+* singularize module names
+
+* separate Decimal and general representation
+
+* use Proxys instead of plain types for data functions
+  This is also consistent with new Nat kind,
+  where types of kind Nat have no data values.
+
+* Ord: make infix operators classes and prefix functions type functions
+  It seems to be more natural to me to write
+     x :<: y   and   GTT x y ~ True
+
+* Num, Bool, Ord: remove T suffixes from functions
+  Use qualification instead.
diff --git a/Data/SizedInt.hs b/Data/SizedInt.hs
deleted file mode 100644
--- a/Data/SizedInt.hs
+++ /dev/null
@@ -1,157 +0,0 @@
-module Data.SizedInt
-    ( SizedInt ) where
-
-import Data.Bits
-import Types
-
-newtype (NaturalT nT) => SizedInt nT = SizedInt Integer
-
-sizeT :: SizedInt nT
-      -> nT
-sizeT _ = undefined
-
-mask :: forall nT . NaturalT nT
-     => nT
-     -> Integer
-mask _ = bit (fromIntegerT (undefined :: nT)) - 1
-
-signBit :: forall nT . NaturalT nT
-        => nT
-        -> Int
-signBit _ = fromIntegerT (undefined :: nT) - 1
-
-isNegative :: forall nT . NaturalT nT
-           => SizedInt nT
-           -> Bool
-isNegative (SizedInt x) =
-    testBit x $ signBit (undefined :: nT)
-
-instance NaturalT nT => Eq (SizedInt nT) where
-    (SizedInt x) == (SizedInt y) = x == y
-    (SizedInt x) /= (SizedInt y) = x /= y
-
-instance NaturalT nT => Show (SizedInt nT) where
-    showsPrec prec n =
-        showsPrec prec $ toInteger n
-
-instance NaturalT nT => Read (SizedInt nT) where
-    readsPrec prec str =
-        [ (fromInteger n, str)
-        | (n, str) <- readsPrec prec str ]
-
-instance NaturalT nT => Ord (SizedInt nT) where
-    a `compare` b = toInteger a `compare` toInteger b
-
-instance NaturalT nT => Bounded (SizedInt nT) where
-    minBound = SizedInt $ negate $ 1 `shiftL` (fromIntegerT (undefined :: nT) - 1)
-    maxBound = SizedInt $ (1 `shiftL` (fromIntegerT (undefined :: nT) - 1)) - 1
-
-instance NaturalT nT => Enum (SizedInt nT) where
-    succ x
-       | x == maxBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"
-       | otherwise      = x + 1
-    pred x
-       | x == minBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"
-       | otherwise      = x - 1
-    
-    fromEnum (SizedInt x)
-        | x > toInteger (maxBound :: Int) =
-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: Int"
-        | x < toInteger (minBound :: Int) =
-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: Int"
-        | otherwise =
-            fromInteger x
-    toEnum x
-        | x' > toInteger (maxBound :: SizedInt nT) =
-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))
-        | x' < toInteger (minBound :: SizedInt nT) =
-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))
-        | otherwise =
-            fromInteger x'
-            where x' = toInteger x
-
-instance NaturalT nT => Num (SizedInt nT) where
-    (SizedInt a) + (SizedInt b) =
-        fromInteger $ a + b
-    (SizedInt a) * (SizedInt b) =
-        fromInteger $ a * b
-    negate (SizedInt n) =
-        fromInteger $ (n `xor` mask (undefined :: nT)) + 1
-    a - b =
-        a + (negate b)
-    
-    fromInteger n
-      | n > 0 =
-        SizedInt $ n .&. mask (undefined :: nT)
-    fromInteger n
-      | n < 0 =
-        negate $ fromInteger $ negate n
-    fromInteger _ =
-        SizedInt 0
-    
-    abs s
-      | isNegative s =
-          negate s
-      | otherwise =
-          s
-    signum s
-      | isNegative s =
-          -1
-      | s == 0 =
-          0
-      | otherwise =
-          1
-
-instance NaturalT nT => Real (SizedInt nT) where
-    toRational n = toRational $ toInteger n
-
-instance NaturalT nT => Integral (SizedInt nT) where
-    a `quot` b =
-        fromInteger $ toInteger a `quot` toInteger b
-    a `rem` b =
-        fromInteger $ toInteger a `rem` toInteger b
-    a `div` b =
-        fromInteger $ toInteger a `div` toInteger b
-    a `mod` b =
-        fromInteger $ toInteger a `mod` toInteger b
-    a `quotRem` b =
-        let (quot, rem) = toInteger a `quotRem` toInteger b
-        in (fromInteger quot, fromInteger rem)
-    a `divMod` b =
-        let (div, mod) = toInteger a `divMod` toInteger b
-        in (fromInteger div, fromInteger mod)
-    toInteger s@(SizedInt x) =
-        if isNegative s
-           then let SizedInt x' = negate s in negate x'
-           else x
-
-instance NaturalT nT => Bits (SizedInt nT) where
-    (SizedInt a) .&. (SizedInt b) = SizedInt $ a .&. b
-    (SizedInt a) .|. (SizedInt b) = SizedInt $ a .|. b
-    (SizedInt a) `xor` SizedInt b = SizedInt $ a `xor` b
-    complement (SizedInt x) = SizedInt $ x `xor` mask (undefined :: nT)
-    (SizedInt x) `shiftL` b
-      | b < 0 = error $ "Bits.shiftL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"
-      | otherwise =
-        SizedInt $ mask (undefined :: nT) .&. (x `shiftL` b)
-    s@(SizedInt x) `shiftR` b
-      | b < 0 = error $ "Bits.shiftR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"
-      | isNegative s =
-        SizedInt $ mask (undefined :: nT) .&.
-            ((x `shiftR` b) .|. (mask (undefined :: nT) `shiftL` (fromIntegerT (undefined :: nT) - b)))
-      | otherwise =
-        SizedInt $ (mask (undefined :: nT)) .&. (x `shiftR` b)
-    (SizedInt a) `rotateL` b
-      | b < 0 =
-        error $ "Bits.rotateL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"
-      | otherwise =
-        SizedInt $ mask (undefined :: nT) .&.
-            ((a `shiftL` b) .|. (a `shiftR` (fromIntegerT (undefined :: nT) - b)))
-    (SizedInt a) `rotateR` b
-      | b < 0 =
-        error $ "Bits.rotateR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"
-      | otherwise =
-        SizedInt $ mask (undefined :: nT) .&.
-            ((a `shiftR` b) .|. (a `shiftL` (fromIntegerT (undefined :: nT) - b)))
-    bitSize _ = fromIntegerT (undefined :: nT)
-    isSigned _ = True
diff --git a/Data/SizedWord.hs b/Data/SizedWord.hs
deleted file mode 100644
--- a/Data/SizedWord.hs
+++ /dev/null
@@ -1,133 +0,0 @@
-module Data.SizedWord
-    ( SizedWord ) where
-
-import Data.Bits
-import Types
-
-newtype (NaturalT nT) => SizedWord nT = SizedWord Integer
-
-sizeT :: SizedWord nT
-      -> nT
-sizeT _ = undefined
-
-mask :: forall nT . NaturalT nT
-     => nT
-     -> Integer
-mask _ = bit (fromIntegerT (undefined :: nT)) - 1
-
-instance NaturalT nT => Eq (SizedWord nT) where
-    (SizedWord x) == (SizedWord y) = x == y
-    (SizedWord x) /= (SizedWord y) = x /= y
-
-instance NaturalT nT => Show (SizedWord nT) where
-    showsPrec prec n =
-        showsPrec prec $ toInteger n
-
-instance NaturalT nT => Read (SizedWord nT) where
-    readsPrec prec str =
-        [ (fromInteger n, str)
-        | (n, str) <- readsPrec prec str ]
-
-instance NaturalT nT => Ord (SizedWord nT) where
-    a `compare` b = toInteger a `compare` toInteger b
-
-instance NaturalT nT => Bounded (SizedWord nT) where
-    minBound = 0
-    maxBound = SizedWord $ (1 `shiftL` (fromIntegerT (undefined :: nT))) - 1
-
-instance NaturalT nT => Enum (SizedWord nT) where
-    succ x
-       | x == maxBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"
-       | otherwise      = x + 1
-    pred x
-       | x == minBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"
-       | otherwise      = x - 1
-    
-    fromEnum (SizedWord x)
-        | x > toInteger (maxBound :: Int) =
-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: Int"
-        | x < toInteger (minBound :: Int) =
-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: Int"
-        | otherwise =
-            fromInteger x
-    toEnum x
-        | x > fromIntegral (maxBound :: SizedWord nT) =
-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))
-        | x < fromIntegral (minBound :: SizedWord nT) =
-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))
-        | otherwise =
-            fromInteger $ toInteger x
-
-instance NaturalT nT => Num (SizedWord nT) where
-    (SizedWord a) + (SizedWord b) =
-        fromInteger $ a + b
-    (SizedWord a) * (SizedWord b) =
-        fromInteger $ a * b
-    negate s@(SizedWord n) =
-        fromInteger $ (n `xor` mask (sizeT s)) + 1
-    a - b =
-        a + (negate b)
-    
-    fromInteger n
-      | n > 0 =
-        SizedWord $ n .&. mask (undefined :: nT)
-    fromInteger n
-      | n < 0 =
-        negate $ fromInteger $ negate n
-    fromInteger _ =
-        SizedWord 0
-    
-    abs s = s
-    signum s
-      | s == 0 =
-          0
-      | otherwise =
-          1
-
-instance NaturalT nT => Real (SizedWord nT) where
-    toRational n = toRational $ toInteger n
-
-instance NaturalT nT => Integral (SizedWord nT) where
-    a `quot` b =
-        fromInteger $ toInteger a `quot` toInteger b
-    a `rem` b =
-        fromInteger $ toInteger a `rem` toInteger b
-    a `div` b =
-        fromInteger $ toInteger a `div` toInteger b
-    a `mod` b =
-        fromInteger $ toInteger a `mod` toInteger b
-    a `quotRem` b =
-        let (quot, rem) = toInteger a `quotRem` toInteger b
-        in (fromInteger quot, fromInteger rem)
-    a `divMod` b =
-        let (div, mod) = toInteger a `divMod` toInteger b
-        in (fromInteger div, fromInteger mod)
-    toInteger s@(SizedWord x) = x
-
-instance NaturalT nT => Bits (SizedWord nT) where
-    (SizedWord a) .&. (SizedWord b) = SizedWord $ a .&. b
-    (SizedWord a) .|. (SizedWord b) = SizedWord $ a .|. b
-    (SizedWord a) `xor` SizedWord b = SizedWord $ a `xor` b
-    complement (SizedWord x) = SizedWord $ x `xor` mask (undefined :: nT)
-    s@(SizedWord x) `shiftL` b
-      | b < 0 = error $ "Bits.shiftL{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"
-      | otherwise =
-        SizedWord $ mask (undefined :: nT) .&. (x `shiftL` b)
-    s@(SizedWord x) `shiftR` b
-      | b < 0 = error $ "Bits.shiftR{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"
-      | otherwise =
-        SizedWord $ (x `shiftR` b)
-    s@(SizedWord x) `rotateL` b
-      | b < 0 =
-        error $ "Bits.rotateL{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"
-      | otherwise =
-        SizedWord $ mask (undefined :: nT) .&.
-            ((x `shiftL` b) .|. (x `shiftR` (bitSize s - b)))
-    s@(SizedWord x) `rotateR` b
-      | b < 0 =
-        error $ "Bits.rotateR{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"
-      | otherwise =
-        SizedWord $ mask (undefined :: nT) .&.
-            ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))
-    bitSize _ = fromIntegerT (undefined :: nT)
-    isSigned _ = False
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,4 @@
+Copyright (c) 2013 Henning Thielemann
 Copyright (c) 2008 Peter Gavin
 All rights reserved.
 
diff --git a/Test.hs b/Test.hs
deleted file mode 100644
--- a/Test.hs
+++ /dev/null
@@ -1,243 +0,0 @@
-module Main where
-
-import qualified Test.QuickCheck as Q
-
-import qualified Prelude
-import Data.Char (intToDigit)
-import Control.Monad (when)
-
-import Types
-import Types.Data.Num.Decimal.Literals.TH
-
-testIsPositive1 :: IsPositive D1 -> True
-testIsPositive1 = Prelude.id
-testIsPositive2 :: IsPositive D0 -> False
-testIsPositive2 = Prelude.id
-testIsPositive3 :: IsPositive DN1 -> False
-testIsPositive3 = Prelude.id
-testIsPositive4 :: IsPositive D10 -> True
-testIsPositive4 = Prelude.id
-testIsPositive5 :: IsPositive DN10 -> False
-testIsPositive5 = Prelude.id
-
-testIsNegative1 :: IsNegative D1 -> False
-testIsNegative1 = Prelude.id
-testIsNegative2 :: IsNegative D0 -> False
-testIsNegative2 = Prelude.id
-testIsNegative3 :: IsNegative DN1 -> True
-testIsNegative3 = Prelude.id
-testIsNegative4 :: IsNegative D10 -> False
-testIsNegative4 = Prelude.id
-testIsNegative5 :: IsNegative DN10 -> True
-testIsNegative5 = Prelude.id
-
-testIsZero1 :: IsZero D1 -> False
-testIsZero1 = Prelude.id
-testIsZero2 :: IsZero D0 -> True
-testIsZero2 = Prelude.id
-testIsZero3 :: IsZero DN1 -> False
-testIsZero3 = Prelude.id
-testIsZero4 :: IsZero D10 -> False
-testIsZero4 = Prelude.id
-testIsZero5 :: IsZero DN10 -> False
-testIsZero5 = Prelude.id
-
-testSucc1 :: Succ D0 -> D1
-testSucc1 = Prelude.id
-testSucc2 :: Succ D9 -> D10
-testSucc2 = Prelude.id
-testSucc3 :: Succ DN1 -> D0
-testSucc3 = Prelude.id
-testSucc4 :: Succ D99 -> D100
-testSucc4 = Prelude.id
-testSucc5 :: Succ DN100 -> DN99
-testSucc5 = Prelude.id
-testSucc6 :: Succ D100 -> D101
-testSucc6 = Prelude.id
-testSucc7 :: Succ DN101 -> DN100
-testSucc7 = Prelude.id
-testSucc8 :: Succ D0 -> D1 :+: D0
-testSucc8 = Prelude.id
-testSucc9 :: Succ D0 -> D0 :+: D1
-testSucc9 = Prelude.id
-testSucc10 :: Succ D9 -> D1 :+: D9
-testSucc10 = Prelude.id
-testSucc11 :: Succ D9 -> D9 :+: D1
-testSucc11 = Prelude.id
-
-testPred1 :: Pred D1 -> D0
-testPred1 = Prelude.id
-testPred2 :: Pred D0 -> DN1
-testPred2 = Prelude.id
-testPred3 :: Pred DN1 -> DN2
-testPred3 = Prelude.id
-testPred4 :: Pred DN9 -> DN10
-testPred4 = Prelude.id
-testPred5 :: Pred D10 -> D9
-testPred5 = Prelude.id
-testPred6 :: Pred DN99 -> DN100
-testPred6 = Prelude.id
-testPred7 :: Pred D100 -> D99
-testPred7 = Prelude.id
-testPred8 :: Pred D0 -> D0 :-: D1
-testPred8 = Prelude.id
-testPred9 :: Pred D10 -> D10 :-: D1
-testPred9 = Prelude.id
-testPred10 :: Pred D9 -> D8
-testPred10 = Prelude.id
-testPred11 :: Pred D8 -> D7
-testPred11 = Prelude.id
-testPred12 :: Pred D7 -> D6
-testPred12 = Prelude.id
-testPred13 :: Pred D6 -> D5
-testPred13 = Prelude.id
-testPred14 :: Pred D5 -> D4
-testPred14 = Prelude.id
-testPred15 :: Pred D4 -> D3
-testPred15 = Prelude.id
-testPred16 :: Pred D3 -> D2
-testPred16 = Prelude.id
-testPred17 :: Pred D2 -> D1
-testPred17 = Prelude.id
-testPred18 :: Pred D1 -> D0
-testPred18 = Prelude.id
-
-testAdd1 :: D0 :+: D0 -> D0
-testAdd1 = Prelude.id
-testAdd2 :: DN1 :+: D1 -> D0
-testAdd2 = Prelude.id
-testAdd3 :: D1 :+: DN1 -> D0
-testAdd3 = Prelude.id
-testAdd4 :: D1 :+: D1 -> D2
-testAdd4 = Prelude.id
-testAdd5 :: D9 :+: D1 -> D10
-testAdd5 = Prelude.id
-testAdd6 :: D10 :+: DN1 -> D9
-testAdd6 = Prelude.id
-testAdd7 :: D100 :+: DN1 -> D99
-testAdd7 = Prelude.id
-testAdd8 :: D100 :+: DN10 -> D90
-testAdd8 = Prelude.id
-
-testSub1 :: D0 :-: D0 -> D0
-testSub1 = Prelude.id
-testSub2 :: D1 :-: D0 -> D1
-testSub2 = Prelude.id
-testSub3 :: D0 :-: D1 -> DN1
-testSub3 = Prelude.id
-testSub4 :: DN1 :-: D0 -> DN1
-testSub4 = Prelude.id
-testSub5 :: D0 :-: DN1 -> D1
-testSub5 = Prelude.id
-testSub6 :: D100 :-: D1 -> D99
-testSub6 = Prelude.id
-testSub7 :: DN100 :-: D1 -> DN101
-testSub7 = Prelude.id
-testSub8 :: D100 :-: DN1 -> D101
-testSub8 = Prelude.id
-testSub9 :: DN100 :-: DN1 -> DN99
-testSub9 = Prelude.id
-testSub10 :: D1 :-: D100 -> DN99
-testSub10 = Prelude.id
-testSub11 :: DN1 :-: D100 -> DN101
-testSub11 = Prelude.id
-testSub12 :: D1 :-: DN100 -> D101
-testSub12 = Prelude.id
-testSub13 :: DN1 :-: DN100 -> D99
-testSub13 = Prelude.id
-testSub14 :: D57 :-: D58 -> DN1
-testSub14 = Prelude.id
-testSub15 :: D1000 :-: D11 -> D989
-testSub15 = Prelude.id
-
-testMul1 :: D0 :*: D0 -> D0
-testMul1 = Prelude.id
-testMul2 :: D1 :*: D1 -> D1
-testMul2 = Prelude.id
-testMul3 :: D0 :*: D1 -> D0
-testMul3 = Prelude.id
-testMul4 :: D1 :*: D0 -> D0
-testMul4 = Prelude.id
-testMul5 :: D1 :*: DN1 -> DN1
-testMul5 = Prelude.id
-testMul6 :: DN1 :*: D1 -> DN1
-testMul6 = Prelude.id
-testMul7 :: DN1 :*: DN1 -> D1
-testMul7 = Prelude.id
-testMul8 :: D100 :*: D100 -> D10000
-testMul8 = Prelude.id
-testMul9 :: D17 :*: D31 -> D527
-testMul9 = Prelude.id
-
-testFac1 :: Fac D0 -> D1
-testFac1 = Prelude.id
-testFac2 :: Fac D1 -> D1
-testFac2 = Prelude.id
-testFac3 :: Fac D6 -> D720
-testFac3 = Prelude.id
-$( decLiteralD "D" "d" 3628800 )
-testFac4 :: Fac D10 -> D3628800
-testFac4 = Prelude.id
-
-testEQ1 :: D0 :==: D0 -> True
-testEQ1 = Prelude.id
-testEQ2 :: D0 :==: Pred D1 -> True
-testEQ2 = Prelude.id
-testEQ3 :: (D1 :+: D9) :==: D10 -> True
-testEQ3 = Prelude.id
-testEQ4 :: (D1 :+: D9) :==: D11 -> False
-testEQ4 = Prelude.id
-testEQ5 :: D9 :==: D0 -> False
-testEQ5 = Prelude.id
-testEQ6 :: D8 :==: D0 -> False
-testEQ6 = Prelude.id
-testEQ7 :: D7 :==: D0 -> False
-testEQ7 = Prelude.id
-testEQ8 :: D6 :==: D0 -> False
-testEQ8 = Prelude.id
-testEQ9 :: D5 :==: D0 -> False
-testEQ9 = Prelude.id
-testEQ10 :: D4 :==: D0 -> False
-testEQ10 = Prelude.id
-testEQ11 :: D3 :==: D0 -> False
-testEQ11 = Prelude.id
-testEQ12 :: D2 :==: D0 -> False
-testEQ12 = Prelude.id
-testEQ13 :: D1 :==: D0 -> False
-testEQ13 = Prelude.id
-
-testMin1 :: Min D0 D5 -> D0
-testMin1 = Prelude.id
-testMin2 :: Min D5 D0 -> D0
-testMin2 = Prelude.id
-testMin3 :: Min DN5 D5 -> DN5
-testMin3 = Prelude.id
-
-testMax1 :: Max D1 D6 -> D6
-testMax1 = Prelude.id
-testMax2 :: Max DN6 D6 -> D6
-testMax2 = Prelude.id
-testMax3 :: Max D6 D1 -> D6
-testMax3 = Prelude.id
-
-class TestIter n zero where
-    testIter :: n -> zero -> Prelude.String
-
-instance ( NaturalT n
-         , (n :==: D0) ~ True )
-  => TestIter n True where
-    testIter _ _ = ""
-
-instance ( NaturalT n
-         , (n :==: D0) ~ False
-         , TestIter (Pred n) ((Pred n) :==: D0) )
-  => TestIter n False where
-    testIter n _ =
-        intToDigit (fromIntegerT n) : testIter (_T :: (Pred n)) (_T :: ((Pred n) :==: D0))
-
-main = do
-  let testIterResult = testIter d9 (_T :: False)
-  when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))
-  Q.quickCheck prop_reifyIntegral
-
-prop_reifyIntegral i = reifyIntegral (Prelude.undefined :: Decimal) i fromIntegerT Prelude.== i
diff --git a/Types.hs b/Types.hs
deleted file mode 100644
--- a/Types.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-module Types
-    ( module Types.Base
-    , module Types.Data.Bool
-    , module Types.Data.Num
-    , module Types.Data.List
-    , module Types.Data.Ord
-    ) where
-
-import Types.Base
-import Types.Data.Bool
-import Types.Data.Num
-import Types.Data.List
-import Types.Data.Ord
diff --git a/Types/Base.hs b/Types/Base.hs
deleted file mode 100644
--- a/Types/Base.hs
+++ /dev/null
@@ -1,24 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Decimal.Ops
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Base
-    where
-
-import qualified Prelude
-
-type family Id x
-type instance Id x = x
-
-_T :: a
-_T = Prelude.undefined
diff --git a/Types/Data/Bool.hs b/Types/Data/Bool.hs
deleted file mode 100644
--- a/Types/Data/Bool.hs
+++ /dev/null
@@ -1,70 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Bool
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Bool
-    ( True
-    , trueT
-    , False
-    , falseT
-    , Not
-    , notT
-    , (:&&:)
-    , andT
-    , (:||:)
-    , orT
-    , IfT(..)
-    ) where
-
-import Data.Typeable
-
-import qualified Prelude
-
-data True deriving (Typeable)
-trueT :: True
-trueT = Prelude.undefined
-instance Prelude.Show True where
-    show _ = "True"
-data False deriving (Typeable)
-falseT :: False
-falseT = Prelude.undefined
-instance Prelude.Show False where
-    show _ = "False"
-
-type family Not x
-type instance Not False = True
-type instance Not True  = False
-notT :: x -> Not x
-notT _ = Prelude.undefined
-
-type family x :&&: y
-type instance False :&&: x = False
-type instance True  :&&: x = x
-andT :: x -> y -> x :&&: y
-andT _ _ = Prelude.undefined
-
-type family x :||: y
-type instance True  :||: x = True
-type instance False :||: x = x
-orT :: x -> y -> x :||: y
-orT _ _ = Prelude.undefined
-
-class IfT x y z where
-    type If x y z
-    ifT :: x -> y -> z -> If x y z
-instance IfT True y z where
-    type If True y z = y
-    ifT _ y _ = y
-instance IfT False y z where
-    type If False y z = z
-    ifT _ _ z = z
diff --git a/Types/Data/List.hs b/Types/Data/List.hs
deleted file mode 100644
--- a/Types/Data/List.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-module Types.Data.List
-    ( Cons
-    , Null
-    , IsNull
-    , Head
-    , Tail
-    , Reverse
-    , Append
-    ) where
-
-import qualified Prelude
-
-import Data.Typeable
-
-import Types.Data.Bool
-
-data Cons car cdr deriving (Typeable)
-instance (Prelude.Show car, Prelude.Show cdr) => Prelude.Show (Cons car cdr) where
-    show = showCons
-
-showCons :: forall car cdr . (Prelude.Show car, Prelude.Show cdr) => Cons car cdr -> Prelude.String
-showCons _ = "Cons (" Prelude.++ Prelude.show (Prelude.undefined :: car) Prelude.++ ") (" Prelude.++ Prelude.show (Prelude.undefined :: cdr) Prelude.++ ")"
-
-data Null deriving (Typeable)
-instance Prelude.Show Null where
-    show _ = ""
-
-type family IsNull l
-type instance IsNull (Cons car cdr) = False
-type instance IsNull Null = True
-
-type family Head l
-type instance Head (Cons car cdr) = car
-
-type family Tail l
-type instance Tail (Cons car cdr) = cdr
-
-type family Reverse l
-type instance Reverse l = Reverse' l Null
-
-type family Reverse' l a
-type instance Reverse' Null a = a
-type instance Reverse' (Cons car cdr) a = Reverse' cdr (Cons car a)
-
-type family Append l1 l2
-type instance Append Null l2 = l2
-type instance Append (Cons car1 cdr2) l2 = Cons car1 (Append cdr2 l2)
diff --git a/Types/Data/Num.hs b/Types/Data/Num.hs
deleted file mode 100644
--- a/Types/Data/Num.hs
+++ /dev/null
@@ -1,28 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Num
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Num
-    ( module Types.Data.Num.Ops
-    , module Types.Data.Num.Decimal
-    , reifyIntegralD
-    , reifyPositiveD
-    , reifyNegativeD
-    ) where
-
-import Types.Data.Num.Ops
-import Types.Data.Num.Decimal
-
-reifyIntegralD = reifyIntegral decimal
-reifyPositiveD = reifyPositive decimal
-reifyNegativeD = reifyNegative decimal
diff --git a/Types/Data/Num/Decimal.hs b/Types/Data/Num/Decimal.hs
deleted file mode 100644
--- a/Types/Data/Num/Decimal.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-module Types.Data.Num.Decimal
-    ( module Types.Data.Num.Decimal.Digits
-    , module Types.Data.Num.Decimal.Literals
-    , module Types.Data.Num.Decimal.Ops
-    ) where
-
-import Types.Data.Num.Decimal.Digits
-import Types.Data.Num.Decimal.Literals
-import Types.Data.Num.Decimal.Ops ()
diff --git a/Types/Data/Num/Decimal/Digits.hs b/Types/Data/Num/Decimal/Digits.hs
deleted file mode 100644
--- a/Types/Data/Num/Decimal/Digits.hs
+++ /dev/null
@@ -1,65 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Num.Decimal.Digits
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Num.Decimal.Digits
-    where
-
-import Data.Typeable
-
-import Types.Data.List
-import Types.Data.Num.Ops
-
--- | Representation name for decimal type level numbers.
-data Decimal
-decimal = undefined :: Decimal
-
--- | The wrapper type for decimal type level numbers.
-data Dec x
-data Neg' x
-
--- | The terminator type for decimal digit lists.
-data DecN
-instance Show DecN where
-    show _ = ""
-
-data Dec0 deriving (Typeable)
-instance Show Dec0 where
-    show _ = "0"
-data Dec1 deriving (Typeable)
-instance Show Dec1 where
-    show _ = "1"
-data Dec2 deriving (Typeable)
-instance Show Dec2 where
-    show _ = "2"
-data Dec3 deriving (Typeable)
-instance Show Dec3 where
-    show _ = "3"
-data Dec4 deriving (Typeable)
-instance Show Dec4 where
-    show _ = "4"
-data Dec5 deriving (Typeable)
-instance Show Dec5 where
-    show _ = "5"
-data Dec6 deriving (Typeable)
-instance Show Dec6 where
-    show _ = "6"
-data Dec7 deriving (Typeable)
-instance Show Dec7 where
-    show _ = "7"
-data Dec8 deriving (Typeable)
-instance Show Dec8 where
-    show _ = "8"
-data Dec9 deriving (Typeable)
-instance Show Dec9 where
-    show _ = "9"
diff --git a/Types/Data/Num/Decimal/Literals.hs b/Types/Data/Num/Decimal/Literals.hs
deleted file mode 100644
--- a/Types/Data/Num/Decimal/Literals.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module Types.Data.Num.Decimal.Literals where
-
-import Types.Data.Num.Decimal.Literals.TH
-
-import Types.Data.Num.Decimal.Digits
-import Types.Data.Num.Ops
-
-$( decLiteralsD "D" "d" (-10000) (10000) )
diff --git a/Types/Data/Num/Decimal/Literals/TH.hs b/Types/Data/Num/Decimal/Literals/TH.hs
deleted file mode 100644
--- a/Types/Data/Num/Decimal/Literals/TH.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-module Types.Data.Num.Decimal.Literals.TH where
-
-import Language.Haskell.TH
-
-import qualified Types.Data.Num.Decimal.Digits as D
-import qualified Types.Data.Num.Ops as O
-
-decLiteralT :: Integer -> Q Type
-decLiteralT n = appT (conT (''D.Dec)) (decLiteralT' n)
-    where decLiteralT' n | n < 0     = appT (conT ''D.Neg') (decLiteralT' (-n))
-                         | n == 0    = conT ''D.DecN
-                         | otherwise = appT (appT (conT ''(O.:.)) (decLiteralT' (n `div` 10))) (conT (case n `mod` 10 of
-                                                  0 -> ''D.Dec0 
-                                                  1 -> ''D.Dec1
-                                                  2 -> ''D.Dec2
-                                                  3 -> ''D.Dec3
-                                                  4 -> ''D.Dec4
-                                                  5 -> ''D.Dec5
-                                                  6 -> ''D.Dec6
-                                                  7 -> ''D.Dec7
-                                                  8 -> ''D.Dec8
-                                                  9 -> ''D.Dec9))
-
-decLiteralV :: Integer -> Q Exp
-decLiteralV n = sigE [| undefined |] (decLiteralT n)
-
-decLiteralD :: String
-            -> String
-            -> Integer
-            -> Q [Dec]
-decLiteralD typePrefix valPrefix n =
-    do let suffix = if n < 0 then "N" ++ show (-n) else show n
-           typeName = mkName $ typePrefix ++ suffix
-           valName = mkName $ valPrefix ++ suffix
-       tySyn <- tySynD typeName [] (decLiteralT n)
-       sig   <- sigD valName (conT typeName)
-       val   <- valD (varP valName) (normalB [| undefined |]) []
-       return [ tySyn, sig, val ]
-
-decLiteralsD :: String
-             -> String
-             -> Integer
-             -> Integer
-             -> Q [Dec]
-decLiteralsD typePrefix valPrefix from to =
-    fmap concat $ sequence $ [ decLiteralD typePrefix valPrefix n | n <- [from..to] ]
diff --git a/Types/Data/Num/Decimal/Ops.hs b/Types/Data/Num/Decimal/Ops.hs
deleted file mode 100644
--- a/Types/Data/Num/Decimal/Ops.hs
+++ /dev/null
@@ -1,908 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Num.Decimal.Ops
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Num.Decimal.Ops ()
-    where
-
-import Types.Base
-import Types.Data.Bool
-import Types.Data.Ord
-import Types.Data.Num.Ops
-import Types.Data.Num.Decimal.Literals
-import Types.Data.Num.Decimal.Digits
-
-instance IntegerR Decimal where
-    reifyIntegral _ i k = reifyIntegral' i (\(_ :: s) -> k (undefined :: Dec s))
-
-reifyIntegral' :: Integer -> (forall s. IntegerT' s => s -> w) -> w
-reifyIntegral' i k | i <  0    = go (negate i) (\(_ :: s) -> k (undefined :: Neg' s)) 
-                   | otherwise = go i k
-  where
-   go :: Integer -> (forall s. IntegerT' s => s -> w) -> w
-   go 0 k = k (undefined :: DecN)
-   go i k = let (j, d) =  quotRem i 10 in case d of
-     0 -> go j (\(_ :: s) -> k (undefined :: s :. Dec0))
-     1 -> go j (\(_ :: s) -> k (undefined :: s :. Dec1))
-     2 -> go j (\(_ :: s) -> k (undefined :: s :. Dec2))
-     3 -> go j (\(_ :: s) -> k (undefined :: s :. Dec3))
-     4 -> go j (\(_ :: s) -> k (undefined :: s :. Dec4))
-     5 -> go j (\(_ :: s) -> k (undefined :: s :. Dec5))
-     6 -> go j (\(_ :: s) -> k (undefined :: s :. Dec6))
-     7 -> go j (\(_ :: s) -> k (undefined :: s :. Dec7))
-     8 -> go j (\(_ :: s) -> k (undefined :: s :. Dec8))
-     9 -> go j (\(_ :: s) -> k (undefined :: s :. Dec9))
-
-instance IntegerT' x => IntegerT (Dec x) where
-    fromIntegerT _ = fromIntegerT' (undefined :: x)
-    type Repr (Dec x) = Decimal
-
-class IntegerT' x where
-    fromIntegerT' :: Num y => x -> y
-instance IntegerT' DecN where
-    fromIntegerT' _ = 0
-instance IntegerT' x => IntegerT' (Neg' x) where
-    fromIntegerT' _ = negate (fromIntegerT' (undefined :: x))
-instance IntegerT' xh => IntegerT' (xh :. Dec0) where
-    fromIntegerT' _ = 0 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec1) where
-    fromIntegerT' _ = 1 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec2) where
-    fromIntegerT' _ = 2 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec3) where
-    fromIntegerT' _ = 3 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec4) where
-    fromIntegerT' _ = 4 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec5) where
-    fromIntegerT' _ = 5 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec6) where
-    fromIntegerT' _ = 6 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec7) where
-    fromIntegerT' _ = 7 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec8) where
-    fromIntegerT' _ = 8 + 10 * fromIntegerT' (undefined :: xh)
-instance IntegerT' xh => IntegerT' (xh :. Dec9) where
-    fromIntegerT' _ = 9 + 10 * fromIntegerT' (undefined :: xh)
-
-type family Normalize x
-type instance Normalize (Dec x) = Dec (Normalize' x)
-
-type family Normalize' x
-type instance Normalize' DecN       = DecN
-type instance Normalize' (xh :. xl) = NormalizePos (xh :. xl)
-type instance Normalize' (Neg' x)   = NormalizeNeg x
-
-type family NormalizePos x
-type instance NormalizePos x = NormalizePos' (ReverseDigits x)
-type family NormalizePos' x
-type instance NormalizePos' DecN         = DecN
-type instance NormalizePos' (xh :. Dec0) = NormalizePos' xh
-type instance NormalizePos' (xh :. Dec1) = ReverseDigits (xh :. Dec1)
-type instance NormalizePos' (xh :. Dec2) = ReverseDigits (xh :. Dec2)
-type instance NormalizePos' (xh :. Dec3) = ReverseDigits (xh :. Dec3)
-type instance NormalizePos' (xh :. Dec4) = ReverseDigits (xh :. Dec4)
-type instance NormalizePos' (xh :. Dec5) = ReverseDigits (xh :. Dec5)
-type instance NormalizePos' (xh :. Dec6) = ReverseDigits (xh :. Dec6)
-type instance NormalizePos' (xh :. Dec7) = ReverseDigits (xh :. Dec7)
-type instance NormalizePos' (xh :. Dec8) = ReverseDigits (xh :. Dec8)
-type instance NormalizePos' (xh :. Dec9) = ReverseDigits (xh :. Dec9)
-
-type family ReverseDigits x
-type instance ReverseDigits DecN       = DecN
-type instance ReverseDigits (xh :. xl) = ReverseDigits' (xh :. xl) DecN
-
-type family ReverseDigits' x y
-type instance ReverseDigits' DecN y = y
-type instance ReverseDigits' (xh :. xl) y = ReverseDigits' xh (y :. xl)
-
-type family NormalizeNeg x
-type instance NormalizeNeg (Neg' x)   = Normalize' x -- negate . negate == id
-type instance NormalizeNeg DecN       = DecN         -- negate 0 = 0
-type instance NormalizeNeg (xh :. xl) = NormalizeNeg' (NormalizePos (xh :. xl))
-
-type family NormalizeNeg' x
-type instance NormalizeNeg' DecN = DecN
-type instance NormalizeNeg' (xh :. xl) = Neg' (xh :. xl)
-
--- type family IsPositive x
-type instance IsPositive (Dec x) = IsPositive' x
-type family IsPositive' x
-type instance IsPositive' (Neg' x)   = False
-type instance IsPositive' DecN       = False
-type instance IsPositive' (xh :. xl) = True
-
--- type family IsZero x
-type instance IsZero (Dec x) = IsZero' x
-type family IsZero' x
-type instance IsZero' (Neg' x)   = False
-type instance IsZero' DecN       = True
-type instance IsZero' (xh :. xl) = False
-
--- type family IsNegative x
-type instance IsNegative (Dec x) = IsNegative' x
-type family IsNegative' x
-type instance IsNegative' (Neg' x)   = True
-type instance IsNegative' DecN       = False
-type instance IsNegative' (xh :. xl) = False
-
--- type family Neg x
-type instance Neg (Dec DecN)     = Dec DecN
-type instance Neg (Dec (Neg' x)) = Dec x
-type instance Neg (Dec (xh :. xl)) = Dec (Neg' (xh :. xl))
-
--- type family Succ x
-type instance Succ (Dec x) = Dec (Succ' x)
-
-type family Succ' x
-type instance Succ' (Neg' x   ) = Normalize' (Neg' (Pred'' x))
-type instance Succ' (DecN     ) = DecN :. Dec1
-type instance Succ' (x :. Dec0) = x :. Dec1
-type instance Succ' (x :. Dec1) = x :. Dec2
-type instance Succ' (x :. Dec2) = x :. Dec3
-type instance Succ' (x :. Dec3) = x :. Dec4
-type instance Succ' (x :. Dec4) = x :. Dec5
-type instance Succ' (x :. Dec5) = x :. Dec6
-type instance Succ' (x :. Dec6) = x :. Dec7
-type instance Succ' (x :. Dec7) = x :. Dec8
-type instance Succ' (x :. Dec8) = x :. Dec9
-type instance Succ' (x :. Dec9) = Succ' x :. Dec0
-
--- type family Pred x
-type instance Pred (Dec x)     = Dec (Pred' x)
-
-type family Pred' x
-type instance Pred' x = Normalize' (Pred'' x)
-type family Pred'' x
-type instance Pred'' (Neg' x   ) = Neg' (Succ' x)
-type instance Pred'' (DecN     ) = Neg' (DecN :. Dec1)
-type instance Pred'' (x :. Dec0) = Pred'' x :. Dec9
-type instance Pred'' (x :. Dec1) = x :. Dec0
-type instance Pred'' (x :. Dec2) = x :. Dec1
-type instance Pred'' (x :. Dec3) = x :. Dec2
-type instance Pred'' (x :. Dec4) = x :. Dec3
-type instance Pred'' (x :. Dec5) = x :. Dec4
-type instance Pred'' (x :. Dec6) = x :. Dec5
-type instance Pred'' (x :. Dec7) = x :. Dec6
-type instance Pred'' (x :. Dec8) = x :. Dec7
-type instance Pred'' (x :. Dec9) = x :. Dec8
-
---------------------
--- Addition
-
-type family AddDigit x y
--- putStr $ unlines $ concat $ [ [ "type instance AddDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x+y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
-type instance AddDigit Dec0 Dec0 = Dec0
-type instance AddDigit Dec0 Dec1 = Dec1
-type instance AddDigit Dec0 Dec2 = Dec2
-type instance AddDigit Dec0 Dec3 = Dec3
-type instance AddDigit Dec0 Dec4 = Dec4
-type instance AddDigit Dec0 Dec5 = Dec5
-type instance AddDigit Dec0 Dec6 = Dec6
-type instance AddDigit Dec0 Dec7 = Dec7
-type instance AddDigit Dec0 Dec8 = Dec8
-type instance AddDigit Dec0 Dec9 = Dec9
-
-type instance AddDigit Dec1 Dec0 = Dec1
-type instance AddDigit Dec1 Dec1 = Dec2
-type instance AddDigit Dec1 Dec2 = Dec3
-type instance AddDigit Dec1 Dec3 = Dec4
-type instance AddDigit Dec1 Dec4 = Dec5
-type instance AddDigit Dec1 Dec5 = Dec6
-type instance AddDigit Dec1 Dec6 = Dec7
-type instance AddDigit Dec1 Dec7 = Dec8
-type instance AddDigit Dec1 Dec8 = Dec9
-type instance AddDigit Dec1 Dec9 = Dec0
-
-type instance AddDigit Dec2 Dec0 = Dec2
-type instance AddDigit Dec2 Dec1 = Dec3
-type instance AddDigit Dec2 Dec2 = Dec4
-type instance AddDigit Dec2 Dec3 = Dec5
-type instance AddDigit Dec2 Dec4 = Dec6
-type instance AddDigit Dec2 Dec5 = Dec7
-type instance AddDigit Dec2 Dec6 = Dec8
-type instance AddDigit Dec2 Dec7 = Dec9
-type instance AddDigit Dec2 Dec8 = Dec0
-type instance AddDigit Dec2 Dec9 = Dec1
-
-type instance AddDigit Dec3 Dec0 = Dec3
-type instance AddDigit Dec3 Dec1 = Dec4
-type instance AddDigit Dec3 Dec2 = Dec5
-type instance AddDigit Dec3 Dec3 = Dec6
-type instance AddDigit Dec3 Dec4 = Dec7
-type instance AddDigit Dec3 Dec5 = Dec8
-type instance AddDigit Dec3 Dec6 = Dec9
-type instance AddDigit Dec3 Dec7 = Dec0
-type instance AddDigit Dec3 Dec8 = Dec1
-type instance AddDigit Dec3 Dec9 = Dec2
-
-type instance AddDigit Dec4 Dec0 = Dec4
-type instance AddDigit Dec4 Dec1 = Dec5
-type instance AddDigit Dec4 Dec2 = Dec6
-type instance AddDigit Dec4 Dec3 = Dec7
-type instance AddDigit Dec4 Dec4 = Dec8
-type instance AddDigit Dec4 Dec5 = Dec9
-type instance AddDigit Dec4 Dec6 = Dec0
-type instance AddDigit Dec4 Dec7 = Dec1
-type instance AddDigit Dec4 Dec8 = Dec2
-type instance AddDigit Dec4 Dec9 = Dec3
-
-type instance AddDigit Dec5 Dec0 = Dec5
-type instance AddDigit Dec5 Dec1 = Dec6
-type instance AddDigit Dec5 Dec2 = Dec7
-type instance AddDigit Dec5 Dec3 = Dec8
-type instance AddDigit Dec5 Dec4 = Dec9
-type instance AddDigit Dec5 Dec5 = Dec0
-type instance AddDigit Dec5 Dec6 = Dec1
-type instance AddDigit Dec5 Dec7 = Dec2
-type instance AddDigit Dec5 Dec8 = Dec3
-type instance AddDigit Dec5 Dec9 = Dec4
-
-type instance AddDigit Dec6 Dec0 = Dec6
-type instance AddDigit Dec6 Dec1 = Dec7
-type instance AddDigit Dec6 Dec2 = Dec8
-type instance AddDigit Dec6 Dec3 = Dec9
-type instance AddDigit Dec6 Dec4 = Dec0
-type instance AddDigit Dec6 Dec5 = Dec1
-type instance AddDigit Dec6 Dec6 = Dec2
-type instance AddDigit Dec6 Dec7 = Dec3
-type instance AddDigit Dec6 Dec8 = Dec4
-type instance AddDigit Dec6 Dec9 = Dec5
-
-type instance AddDigit Dec7 Dec0 = Dec7
-type instance AddDigit Dec7 Dec1 = Dec8
-type instance AddDigit Dec7 Dec2 = Dec9
-type instance AddDigit Dec7 Dec3 = Dec0
-type instance AddDigit Dec7 Dec4 = Dec1
-type instance AddDigit Dec7 Dec5 = Dec2
-type instance AddDigit Dec7 Dec6 = Dec3
-type instance AddDigit Dec7 Dec7 = Dec4
-type instance AddDigit Dec7 Dec8 = Dec5
-type instance AddDigit Dec7 Dec9 = Dec6
-
-type instance AddDigit Dec8 Dec0 = Dec8
-type instance AddDigit Dec8 Dec1 = Dec9
-type instance AddDigit Dec8 Dec2 = Dec0
-type instance AddDigit Dec8 Dec3 = Dec1
-type instance AddDigit Dec8 Dec4 = Dec2
-type instance AddDigit Dec8 Dec5 = Dec3
-type instance AddDigit Dec8 Dec6 = Dec4
-type instance AddDigit Dec8 Dec7 = Dec5
-type instance AddDigit Dec8 Dec8 = Dec6
-type instance AddDigit Dec8 Dec9 = Dec7
-
-type instance AddDigit Dec9 Dec0 = Dec9
-type instance AddDigit Dec9 Dec1 = Dec0
-type instance AddDigit Dec9 Dec2 = Dec1
-type instance AddDigit Dec9 Dec3 = Dec2
-type instance AddDigit Dec9 Dec4 = Dec3
-type instance AddDigit Dec9 Dec5 = Dec4
-type instance AddDigit Dec9 Dec6 = Dec5
-type instance AddDigit Dec9 Dec7 = Dec6
-type instance AddDigit Dec9 Dec8 = Dec7
-type instance AddDigit Dec9 Dec9 = Dec8
-
--- | If adding @x@ and @y@ would not carry, then
---   @AddCarry x y z@ evaluates to @z@.  Otherwise,
---   @AddCarry x y z@ evaluates to @Succ' z@
-type family AddCarry x y z
--- putStr $ unlines $ concat $ [ [ "type instance AddCarry Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x + y >= 10 then "Succ'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
-type instance AddCarry Dec0 Dec0 x = Id x
-type instance AddCarry Dec0 Dec1 x = Id x
-type instance AddCarry Dec0 Dec2 x = Id x
-type instance AddCarry Dec0 Dec3 x = Id x
-type instance AddCarry Dec0 Dec4 x = Id x
-type instance AddCarry Dec0 Dec5 x = Id x
-type instance AddCarry Dec0 Dec6 x = Id x
-type instance AddCarry Dec0 Dec7 x = Id x
-type instance AddCarry Dec0 Dec8 x = Id x
-type instance AddCarry Dec0 Dec9 x = Id x
-
-type instance AddCarry Dec1 Dec0 x = Id x
-type instance AddCarry Dec1 Dec1 x = Id x
-type instance AddCarry Dec1 Dec2 x = Id x
-type instance AddCarry Dec1 Dec3 x = Id x
-type instance AddCarry Dec1 Dec4 x = Id x
-type instance AddCarry Dec1 Dec5 x = Id x
-type instance AddCarry Dec1 Dec6 x = Id x
-type instance AddCarry Dec1 Dec7 x = Id x
-type instance AddCarry Dec1 Dec8 x = Id x
-type instance AddCarry Dec1 Dec9 x = Succ' x
-
-type instance AddCarry Dec2 Dec0 x = Id x
-type instance AddCarry Dec2 Dec1 x = Id x
-type instance AddCarry Dec2 Dec2 x = Id x
-type instance AddCarry Dec2 Dec3 x = Id x
-type instance AddCarry Dec2 Dec4 x = Id x
-type instance AddCarry Dec2 Dec5 x = Id x
-type instance AddCarry Dec2 Dec6 x = Id x
-type instance AddCarry Dec2 Dec7 x = Id x
-type instance AddCarry Dec2 Dec8 x = Succ' x
-type instance AddCarry Dec2 Dec9 x = Succ' x
-
-type instance AddCarry Dec3 Dec0 x = Id x
-type instance AddCarry Dec3 Dec1 x = Id x
-type instance AddCarry Dec3 Dec2 x = Id x
-type instance AddCarry Dec3 Dec3 x = Id x
-type instance AddCarry Dec3 Dec4 x = Id x
-type instance AddCarry Dec3 Dec5 x = Id x
-type instance AddCarry Dec3 Dec6 x = Id x
-type instance AddCarry Dec3 Dec7 x = Succ' x
-type instance AddCarry Dec3 Dec8 x = Succ' x
-type instance AddCarry Dec3 Dec9 x = Succ' x
-
-type instance AddCarry Dec4 Dec0 x = Id x
-type instance AddCarry Dec4 Dec1 x = Id x
-type instance AddCarry Dec4 Dec2 x = Id x
-type instance AddCarry Dec4 Dec3 x = Id x
-type instance AddCarry Dec4 Dec4 x = Id x
-type instance AddCarry Dec4 Dec5 x = Id x
-type instance AddCarry Dec4 Dec6 x = Succ' x
-type instance AddCarry Dec4 Dec7 x = Succ' x
-type instance AddCarry Dec4 Dec8 x = Succ' x
-type instance AddCarry Dec4 Dec9 x = Succ' x
-
-type instance AddCarry Dec5 Dec0 x = Id x
-type instance AddCarry Dec5 Dec1 x = Id x
-type instance AddCarry Dec5 Dec2 x = Id x
-type instance AddCarry Dec5 Dec3 x = Id x
-type instance AddCarry Dec5 Dec4 x = Id x
-type instance AddCarry Dec5 Dec5 x = Succ' x
-type instance AddCarry Dec5 Dec6 x = Succ' x
-type instance AddCarry Dec5 Dec7 x = Succ' x
-type instance AddCarry Dec5 Dec8 x = Succ' x
-type instance AddCarry Dec5 Dec9 x = Succ' x
-
-type instance AddCarry Dec6 Dec0 x = Id x
-type instance AddCarry Dec6 Dec1 x = Id x
-type instance AddCarry Dec6 Dec2 x = Id x
-type instance AddCarry Dec6 Dec3 x = Id x
-type instance AddCarry Dec6 Dec4 x = Succ' x
-type instance AddCarry Dec6 Dec5 x = Succ' x
-type instance AddCarry Dec6 Dec6 x = Succ' x
-type instance AddCarry Dec6 Dec7 x = Succ' x
-type instance AddCarry Dec6 Dec8 x = Succ' x
-type instance AddCarry Dec6 Dec9 x = Succ' x
-
-type instance AddCarry Dec7 Dec0 x = Id x
-type instance AddCarry Dec7 Dec1 x = Id x
-type instance AddCarry Dec7 Dec2 x = Id x
-type instance AddCarry Dec7 Dec3 x = Succ' x
-type instance AddCarry Dec7 Dec4 x = Succ' x
-type instance AddCarry Dec7 Dec5 x = Succ' x
-type instance AddCarry Dec7 Dec6 x = Succ' x
-type instance AddCarry Dec7 Dec7 x = Succ' x
-type instance AddCarry Dec7 Dec8 x = Succ' x
-type instance AddCarry Dec7 Dec9 x = Succ' x
-
-type instance AddCarry Dec8 Dec0 x = Id x
-type instance AddCarry Dec8 Dec1 x = Id x
-type instance AddCarry Dec8 Dec2 x = Succ' x
-type instance AddCarry Dec8 Dec3 x = Succ' x
-type instance AddCarry Dec8 Dec4 x = Succ' x
-type instance AddCarry Dec8 Dec5 x = Succ' x
-type instance AddCarry Dec8 Dec6 x = Succ' x
-type instance AddCarry Dec8 Dec7 x = Succ' x
-type instance AddCarry Dec8 Dec8 x = Succ' x
-type instance AddCarry Dec8 Dec9 x = Succ' x
-
-type instance AddCarry Dec9 Dec0 x = Id x
-type instance AddCarry Dec9 Dec1 x = Succ' x
-type instance AddCarry Dec9 Dec2 x = Succ' x
-type instance AddCarry Dec9 Dec3 x = Succ' x
-type instance AddCarry Dec9 Dec4 x = Succ' x
-type instance AddCarry Dec9 Dec5 x = Succ' x
-type instance AddCarry Dec9 Dec6 x = Succ' x
-type instance AddCarry Dec9 Dec7 x = Succ' x
-type instance AddCarry Dec9 Dec8 x = Succ' x
-type instance AddCarry Dec9 Dec9 x = Succ' x
-
--- type family x :+: y
-type instance Dec x :+: Dec y = Dec (Add x y)
-
-type family Add x y
-type instance Add (DecN    ) (DecN    ) = DecN
-type instance Add (xh :. xl) (DecN    ) = (xh :. xl)
-type instance Add (DecN    ) (yh :. yl) = (yh :. yl)
-type instance Add (Neg' x  ) (Neg' y  ) = Neg' (Add x y)
-type instance Add (xh :. xl) (Neg' y  ) = Sub (xh :. xl) y
-type instance Add (Neg' x  ) (yh :. yl) = Sub (yh :. yl) x
-type instance Add (xh :. xl) (yh :. yl) = (AddCarry xl yl (Add xh yh)) :. (AddDigit xl yl)
-
---------------------
--- Subtraction
-
-type family SubDigit x y
--- putStr $ unlines $ concat $ [ [ "type instance SubDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x-y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
-type instance SubDigit Dec0 Dec0 = Dec0
-type instance SubDigit Dec0 Dec1 = Dec9
-type instance SubDigit Dec0 Dec2 = Dec8
-type instance SubDigit Dec0 Dec3 = Dec7
-type instance SubDigit Dec0 Dec4 = Dec6
-type instance SubDigit Dec0 Dec5 = Dec5
-type instance SubDigit Dec0 Dec6 = Dec4
-type instance SubDigit Dec0 Dec7 = Dec3
-type instance SubDigit Dec0 Dec8 = Dec2
-type instance SubDigit Dec0 Dec9 = Dec1
-
-type instance SubDigit Dec1 Dec0 = Dec1
-type instance SubDigit Dec1 Dec1 = Dec0
-type instance SubDigit Dec1 Dec2 = Dec9
-type instance SubDigit Dec1 Dec3 = Dec8
-type instance SubDigit Dec1 Dec4 = Dec7
-type instance SubDigit Dec1 Dec5 = Dec6
-type instance SubDigit Dec1 Dec6 = Dec5
-type instance SubDigit Dec1 Dec7 = Dec4
-type instance SubDigit Dec1 Dec8 = Dec3
-type instance SubDigit Dec1 Dec9 = Dec2
-
-type instance SubDigit Dec2 Dec0 = Dec2
-type instance SubDigit Dec2 Dec1 = Dec1
-type instance SubDigit Dec2 Dec2 = Dec0
-type instance SubDigit Dec2 Dec3 = Dec9
-type instance SubDigit Dec2 Dec4 = Dec8
-type instance SubDigit Dec2 Dec5 = Dec7
-type instance SubDigit Dec2 Dec6 = Dec6
-type instance SubDigit Dec2 Dec7 = Dec5
-type instance SubDigit Dec2 Dec8 = Dec4
-type instance SubDigit Dec2 Dec9 = Dec3
-
-type instance SubDigit Dec3 Dec0 = Dec3
-type instance SubDigit Dec3 Dec1 = Dec2
-type instance SubDigit Dec3 Dec2 = Dec1
-type instance SubDigit Dec3 Dec3 = Dec0
-type instance SubDigit Dec3 Dec4 = Dec9
-type instance SubDigit Dec3 Dec5 = Dec8
-type instance SubDigit Dec3 Dec6 = Dec7
-type instance SubDigit Dec3 Dec7 = Dec6
-type instance SubDigit Dec3 Dec8 = Dec5
-type instance SubDigit Dec3 Dec9 = Dec4
-
-type instance SubDigit Dec4 Dec0 = Dec4
-type instance SubDigit Dec4 Dec1 = Dec3
-type instance SubDigit Dec4 Dec2 = Dec2
-type instance SubDigit Dec4 Dec3 = Dec1
-type instance SubDigit Dec4 Dec4 = Dec0
-type instance SubDigit Dec4 Dec5 = Dec9
-type instance SubDigit Dec4 Dec6 = Dec8
-type instance SubDigit Dec4 Dec7 = Dec7
-type instance SubDigit Dec4 Dec8 = Dec6
-type instance SubDigit Dec4 Dec9 = Dec5
-
-type instance SubDigit Dec5 Dec0 = Dec5
-type instance SubDigit Dec5 Dec1 = Dec4
-type instance SubDigit Dec5 Dec2 = Dec3
-type instance SubDigit Dec5 Dec3 = Dec2
-type instance SubDigit Dec5 Dec4 = Dec1
-type instance SubDigit Dec5 Dec5 = Dec0
-type instance SubDigit Dec5 Dec6 = Dec9
-type instance SubDigit Dec5 Dec7 = Dec8
-type instance SubDigit Dec5 Dec8 = Dec7
-type instance SubDigit Dec5 Dec9 = Dec6
-
-type instance SubDigit Dec6 Dec0 = Dec6
-type instance SubDigit Dec6 Dec1 = Dec5
-type instance SubDigit Dec6 Dec2 = Dec4
-type instance SubDigit Dec6 Dec3 = Dec3
-type instance SubDigit Dec6 Dec4 = Dec2
-type instance SubDigit Dec6 Dec5 = Dec1
-type instance SubDigit Dec6 Dec6 = Dec0
-type instance SubDigit Dec6 Dec7 = Dec9
-type instance SubDigit Dec6 Dec8 = Dec8
-type instance SubDigit Dec6 Dec9 = Dec7
-
-type instance SubDigit Dec7 Dec0 = Dec7
-type instance SubDigit Dec7 Dec1 = Dec6
-type instance SubDigit Dec7 Dec2 = Dec5
-type instance SubDigit Dec7 Dec3 = Dec4
-type instance SubDigit Dec7 Dec4 = Dec3
-type instance SubDigit Dec7 Dec5 = Dec2
-type instance SubDigit Dec7 Dec6 = Dec1
-type instance SubDigit Dec7 Dec7 = Dec0
-type instance SubDigit Dec7 Dec8 = Dec9
-type instance SubDigit Dec7 Dec9 = Dec8
-
-type instance SubDigit Dec8 Dec0 = Dec8
-type instance SubDigit Dec8 Dec1 = Dec7
-type instance SubDigit Dec8 Dec2 = Dec6
-type instance SubDigit Dec8 Dec3 = Dec5
-type instance SubDigit Dec8 Dec4 = Dec4
-type instance SubDigit Dec8 Dec5 = Dec3
-type instance SubDigit Dec8 Dec6 = Dec2
-type instance SubDigit Dec8 Dec7 = Dec1
-type instance SubDigit Dec8 Dec8 = Dec0
-type instance SubDigit Dec8 Dec9 = Dec9
-
-type instance SubDigit Dec9 Dec0 = Dec9
-type instance SubDigit Dec9 Dec1 = Dec8
-type instance SubDigit Dec9 Dec2 = Dec7
-type instance SubDigit Dec9 Dec3 = Dec6
-type instance SubDigit Dec9 Dec4 = Dec5
-type instance SubDigit Dec9 Dec5 = Dec4
-type instance SubDigit Dec9 Dec6 = Dec3
-type instance SubDigit Dec9 Dec7 = Dec2
-type instance SubDigit Dec9 Dec8 = Dec1
-type instance SubDigit Dec9 Dec9 = Dec0
-
--- | If subtracting @y@ from @x@ would not borrow, then
---   @Borrow x y z@ evaluates to @z@.  Otherwise,
---   @Borrow x y z@ evaluates to @Pred' z@
-type family Borrow x y z
--- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "Pred'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
-type instance Borrow Dec0 Dec0 x = Id x
-type instance Borrow Dec0 Dec1 x = Pred' x
-type instance Borrow Dec0 Dec2 x = Pred' x
-type instance Borrow Dec0 Dec3 x = Pred' x
-type instance Borrow Dec0 Dec4 x = Pred' x
-type instance Borrow Dec0 Dec5 x = Pred' x
-type instance Borrow Dec0 Dec6 x = Pred' x
-type instance Borrow Dec0 Dec7 x = Pred' x
-type instance Borrow Dec0 Dec8 x = Pred' x
-type instance Borrow Dec0 Dec9 x = Pred' x
-
-type instance Borrow Dec1 Dec0 x = Id x
-type instance Borrow Dec1 Dec1 x = Id x
-type instance Borrow Dec1 Dec2 x = Pred' x
-type instance Borrow Dec1 Dec3 x = Pred' x
-type instance Borrow Dec1 Dec4 x = Pred' x
-type instance Borrow Dec1 Dec5 x = Pred' x
-type instance Borrow Dec1 Dec6 x = Pred' x
-type instance Borrow Dec1 Dec7 x = Pred' x
-type instance Borrow Dec1 Dec8 x = Pred' x
-type instance Borrow Dec1 Dec9 x = Pred' x
-
-type instance Borrow Dec2 Dec0 x = Id x
-type instance Borrow Dec2 Dec1 x = Id x
-type instance Borrow Dec2 Dec2 x = Id x
-type instance Borrow Dec2 Dec3 x = Pred' x
-type instance Borrow Dec2 Dec4 x = Pred' x
-type instance Borrow Dec2 Dec5 x = Pred' x
-type instance Borrow Dec2 Dec6 x = Pred' x
-type instance Borrow Dec2 Dec7 x = Pred' x
-type instance Borrow Dec2 Dec8 x = Pred' x
-type instance Borrow Dec2 Dec9 x = Pred' x
-
-type instance Borrow Dec3 Dec0 x = Id x
-type instance Borrow Dec3 Dec1 x = Id x
-type instance Borrow Dec3 Dec2 x = Id x
-type instance Borrow Dec3 Dec3 x = Id x
-type instance Borrow Dec3 Dec4 x = Pred' x
-type instance Borrow Dec3 Dec5 x = Pred' x
-type instance Borrow Dec3 Dec6 x = Pred' x
-type instance Borrow Dec3 Dec7 x = Pred' x
-type instance Borrow Dec3 Dec8 x = Pred' x
-type instance Borrow Dec3 Dec9 x = Pred' x
-
-type instance Borrow Dec4 Dec0 x = Id x
-type instance Borrow Dec4 Dec1 x = Id x
-type instance Borrow Dec4 Dec2 x = Id x
-type instance Borrow Dec4 Dec3 x = Id x
-type instance Borrow Dec4 Dec4 x = Id x
-type instance Borrow Dec4 Dec5 x = Pred' x
-type instance Borrow Dec4 Dec6 x = Pred' x
-type instance Borrow Dec4 Dec7 x = Pred' x
-type instance Borrow Dec4 Dec8 x = Pred' x
-type instance Borrow Dec4 Dec9 x = Pred' x
-
-type instance Borrow Dec5 Dec0 x = Id x
-type instance Borrow Dec5 Dec1 x = Id x
-type instance Borrow Dec5 Dec2 x = Id x
-type instance Borrow Dec5 Dec3 x = Id x
-type instance Borrow Dec5 Dec4 x = Id x
-type instance Borrow Dec5 Dec5 x = Id x
-type instance Borrow Dec5 Dec6 x = Pred' x
-type instance Borrow Dec5 Dec7 x = Pred' x
-type instance Borrow Dec5 Dec8 x = Pred' x
-type instance Borrow Dec5 Dec9 x = Pred' x
-
-type instance Borrow Dec6 Dec0 x = Id x
-type instance Borrow Dec6 Dec1 x = Id x
-type instance Borrow Dec6 Dec2 x = Id x
-type instance Borrow Dec6 Dec3 x = Id x
-type instance Borrow Dec6 Dec4 x = Id x
-type instance Borrow Dec6 Dec5 x = Id x
-type instance Borrow Dec6 Dec6 x = Id x
-type instance Borrow Dec6 Dec7 x = Pred' x
-type instance Borrow Dec6 Dec8 x = Pred' x
-type instance Borrow Dec6 Dec9 x = Pred' x
-
-type instance Borrow Dec7 Dec0 x = Id x
-type instance Borrow Dec7 Dec1 x = Id x
-type instance Borrow Dec7 Dec2 x = Id x
-type instance Borrow Dec7 Dec3 x = Id x
-type instance Borrow Dec7 Dec4 x = Id x
-type instance Borrow Dec7 Dec5 x = Id x
-type instance Borrow Dec7 Dec6 x = Id x
-type instance Borrow Dec7 Dec7 x = Id x
-type instance Borrow Dec7 Dec8 x = Pred' x
-type instance Borrow Dec7 Dec9 x = Pred' x
-
-type instance Borrow Dec8 Dec0 x = Id x
-type instance Borrow Dec8 Dec1 x = Id x
-type instance Borrow Dec8 Dec2 x = Id x
-type instance Borrow Dec8 Dec3 x = Id x
-type instance Borrow Dec8 Dec4 x = Id x
-type instance Borrow Dec8 Dec5 x = Id x
-type instance Borrow Dec8 Dec6 x = Id x
-type instance Borrow Dec8 Dec7 x = Id x
-type instance Borrow Dec8 Dec8 x = Id x
-type instance Borrow Dec8 Dec9 x = Pred' x
-
-type instance Borrow Dec9 Dec0 x = Id x
-type instance Borrow Dec9 Dec1 x = Id x
-type instance Borrow Dec9 Dec2 x = Id x
-type instance Borrow Dec9 Dec3 x = Id x
-type instance Borrow Dec9 Dec4 x = Id x
-type instance Borrow Dec9 Dec5 x = Id x
-type instance Borrow Dec9 Dec6 x = Id x
-type instance Borrow Dec9 Dec7 x = Id x
-type instance Borrow Dec9 Dec8 x = Id x
-type instance Borrow Dec9 Dec9 x = Id x
-
--- type family x :-: y
-type instance Dec x :-: Dec y = Dec (Sub x y)
-
-type family Sub x y
-type instance Sub x y = Normalize' (Sub' x y)
-
-type family Sub' x y
-type instance Sub' (Neg' x  ) (Neg' y  ) = Sub' y x
-type instance Sub' (Neg' x  ) (DecN    ) = Neg' x
-type instance Sub' (Neg' x  ) (yh :. yl) = Neg' (Add x (yh :. yl))
-type instance Sub' (DecN    ) (Neg' x  ) = x
-type instance Sub' (DecN    ) (DecN    ) = DecN
-type instance Sub' (DecN    ) (yh :. yl) = Neg' (yh :. yl)
-type instance Sub' (xh :. xl) (Neg' y  ) = Add (xh :. xl) y
-type instance Sub' (xh :. xl) (DecN    ) = xh :. xl
-type instance Sub' (xh :. xl) (yh :. yl) = Sub'' (xh :. xl) (yh :. yl) (Compare' (xh :. xl) (yh :. yl))
-
-type family Sub'' x y c
-type instance Sub'' x y GT = SubPos x y DecN
-type instance Sub'' x y EQ = DecN
-type instance Sub'' x y LT = Neg' (SubPos y x DecN)
-
-type family SubPos x y z
-type instance SubPos (xh :. xl) (yh :. yl) z = SubPos (Borrow xl yl xh) yh (z :. SubDigit xl yl)
-type instance SubPos (xh :. xl) DecN       z = SubPos xh DecN (z :. xl)
-type instance SubPos DecN       DecN       z = ReverseDigits z
-
---------------------
--- Multiplication
-
--- type family Mul2 x
-type instance Mul2 (Dec x) = Mul2' x
-type family Mul2' x
-type instance Mul2' x = Add x x
-
--- type family x :*: y
-type instance (Dec x) :*: (Dec y) = Dec (Mul x y)
-
--- Peasant style
-type family Mul x y
-type instance Mul DecN       DecN       = DecN            -- 0 * 0 = 0
-type instance Mul (xh :. xl) DecN       = DecN            -- x * 0 = 0
-type instance Mul DecN       (yh :. yl) = DecN            -- 0 * x = 0
-type instance Mul (Neg' x)   (Neg' y)   = Mul x y        -- -x * -y = x*y
-type instance Mul (xh :. xl) (Neg' y)   = Neg' (Mul (xh :. xl) y)  -- x * -y = -(x*y)
-type instance Mul (Neg' x)   (yh :. yl) = Neg' (Mul x (yh :. yl))  -- -x * y = -(x*y)
-type instance Mul (xh :. xl) (yh :. yl) = Mul' (xh :. xl) (yh :. yl) DecN -- x & y positive
-
-type family Mul' x y z
-type instance Mul' x DecN       z = z
-type instance Mul' x (yh :. yl) z = Mul' (Mul2' x) (Div2' (yh :. yl)) (If (IsEven' (yh :. yl)) z (Add z x))
-
--- type family Fac x
-type instance Fac x = Fac' x (IsZero x)
-type family Fac' x is0
-type instance Fac' x True = D1
-type instance Fac' x False = x :*: Fac (Pred x)
-
------------
--- Division / Modulus
-
--- type family IsEven x
-type instance IsEven (Dec x) = IsEven' x
-type family IsEven' x
-type instance IsEven' DecN = True
-type instance IsEven' (Neg' x) = IsEven' x
-type instance IsEven' (xh :. Dec0) = True
-type instance IsEven' (xh :. Dec1) = False
-type instance IsEven' (xh :. Dec2) = True
-type instance IsEven' (xh :. Dec3) = False
-type instance IsEven' (xh :. Dec4) = True
-type instance IsEven' (xh :. Dec5) = False
-type instance IsEven' (xh :. Dec6) = True
-type instance IsEven' (xh :. Dec7) = False
-type instance IsEven' (xh :. Dec8) = True
-type instance IsEven' (xh :. Dec9) = False
-
--- type family Div2 x
-type instance Div2 (Dec x) = Dec (Div2' x)
-
-type family Div2Digit x
-type instance Div2Digit Dec0 = Dec0
-type instance Div2Digit Dec1 = Dec0
-type instance Div2Digit Dec2 = Dec1
-type instance Div2Digit Dec3 = Dec1
-type instance Div2Digit Dec4 = Dec2
-type instance Div2Digit Dec5 = Dec2
-type instance Div2Digit Dec6 = Dec3
-type instance Div2Digit Dec7 = Dec3
-type instance Div2Digit Dec8 = Dec4
-type instance Div2Digit Dec9 = Dec4
-
-type family Div2' x
-type instance Div2' DecN       = DecN
-type instance Div2' (Neg' x)   = Neg' (Div2Pos x)
-type instance Div2' (xh :. xl) = Div2Pos (xh :. xl)
-
-type family Div2Pos x
-type instance Div2Pos (xh :. xl) = Normalize' (Div2Pos' xh (Div2Digit xl) (If (IsEven' xh) Dec0 Dec5))
-
-type family Div2Pos' xh xl' rem
-type instance Div2Pos' xh xl' rem =
-    (AddCarry xl' rem (Div2' xh)) :. (AddDigit xl' rem)
-
----------------
--- Exponentiation
-
-type instance Pow2 (Dec x) = Dec (Pow2' x (DecN :. Dec1))
-
-type family Pow2' x y
-type instance Pow2' (Neg' x)   y = DecN
-type instance Pow2' DecN       y = y
-type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)
-
----------------
--- Compare
-
-type family CompareDigit x y
--- putStr $ unlines $ concat $ [ [ "type instance CompareDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = " ++ (if x < y then "LT" else (if x > y then "GT" else "EQ")) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
-type instance CompareDigit Dec0 Dec0 = EQ
-type instance CompareDigit Dec0 Dec1 = LT
-type instance CompareDigit Dec0 Dec2 = LT
-type instance CompareDigit Dec0 Dec3 = LT
-type instance CompareDigit Dec0 Dec4 = LT
-type instance CompareDigit Dec0 Dec5 = LT
-type instance CompareDigit Dec0 Dec6 = LT
-type instance CompareDigit Dec0 Dec7 = LT
-type instance CompareDigit Dec0 Dec8 = LT
-type instance CompareDigit Dec0 Dec9 = LT
-
-type instance CompareDigit Dec1 Dec0 = GT
-type instance CompareDigit Dec1 Dec1 = EQ
-type instance CompareDigit Dec1 Dec2 = LT
-type instance CompareDigit Dec1 Dec3 = LT
-type instance CompareDigit Dec1 Dec4 = LT
-type instance CompareDigit Dec1 Dec5 = LT
-type instance CompareDigit Dec1 Dec6 = LT
-type instance CompareDigit Dec1 Dec7 = LT
-type instance CompareDigit Dec1 Dec8 = LT
-type instance CompareDigit Dec1 Dec9 = LT
-
-type instance CompareDigit Dec2 Dec0 = GT
-type instance CompareDigit Dec2 Dec1 = GT
-type instance CompareDigit Dec2 Dec2 = EQ
-type instance CompareDigit Dec2 Dec3 = LT
-type instance CompareDigit Dec2 Dec4 = LT
-type instance CompareDigit Dec2 Dec5 = LT
-type instance CompareDigit Dec2 Dec6 = LT
-type instance CompareDigit Dec2 Dec7 = LT
-type instance CompareDigit Dec2 Dec8 = LT
-type instance CompareDigit Dec2 Dec9 = LT
-
-type instance CompareDigit Dec3 Dec0 = GT
-type instance CompareDigit Dec3 Dec1 = GT
-type instance CompareDigit Dec3 Dec2 = GT
-type instance CompareDigit Dec3 Dec3 = EQ
-type instance CompareDigit Dec3 Dec4 = LT
-type instance CompareDigit Dec3 Dec5 = LT
-type instance CompareDigit Dec3 Dec6 = LT
-type instance CompareDigit Dec3 Dec7 = LT
-type instance CompareDigit Dec3 Dec8 = LT
-type instance CompareDigit Dec3 Dec9 = LT
-
-type instance CompareDigit Dec4 Dec0 = GT
-type instance CompareDigit Dec4 Dec1 = GT
-type instance CompareDigit Dec4 Dec2 = GT
-type instance CompareDigit Dec4 Dec3 = GT
-type instance CompareDigit Dec4 Dec4 = EQ
-type instance CompareDigit Dec4 Dec5 = LT
-type instance CompareDigit Dec4 Dec6 = LT
-type instance CompareDigit Dec4 Dec7 = LT
-type instance CompareDigit Dec4 Dec8 = LT
-type instance CompareDigit Dec4 Dec9 = LT
-
-type instance CompareDigit Dec5 Dec0 = GT
-type instance CompareDigit Dec5 Dec1 = GT
-type instance CompareDigit Dec5 Dec2 = GT
-type instance CompareDigit Dec5 Dec3 = GT
-type instance CompareDigit Dec5 Dec4 = GT
-type instance CompareDigit Dec5 Dec5 = EQ
-type instance CompareDigit Dec5 Dec6 = LT
-type instance CompareDigit Dec5 Dec7 = LT
-type instance CompareDigit Dec5 Dec8 = LT
-type instance CompareDigit Dec5 Dec9 = LT
-
-type instance CompareDigit Dec6 Dec0 = GT
-type instance CompareDigit Dec6 Dec1 = GT
-type instance CompareDigit Dec6 Dec2 = GT
-type instance CompareDigit Dec6 Dec3 = GT
-type instance CompareDigit Dec6 Dec4 = GT
-type instance CompareDigit Dec6 Dec5 = GT
-type instance CompareDigit Dec6 Dec6 = EQ
-type instance CompareDigit Dec6 Dec7 = LT
-type instance CompareDigit Dec6 Dec8 = LT
-type instance CompareDigit Dec6 Dec9 = LT
-
-type instance CompareDigit Dec7 Dec0 = GT
-type instance CompareDigit Dec7 Dec1 = GT
-type instance CompareDigit Dec7 Dec2 = GT
-type instance CompareDigit Dec7 Dec3 = GT
-type instance CompareDigit Dec7 Dec4 = GT
-type instance CompareDigit Dec7 Dec5 = GT
-type instance CompareDigit Dec7 Dec6 = GT
-type instance CompareDigit Dec7 Dec7 = EQ
-type instance CompareDigit Dec7 Dec8 = LT
-type instance CompareDigit Dec7 Dec9 = LT
-
-type instance CompareDigit Dec8 Dec0 = GT
-type instance CompareDigit Dec8 Dec1 = GT
-type instance CompareDigit Dec8 Dec2 = GT
-type instance CompareDigit Dec8 Dec3 = GT
-type instance CompareDigit Dec8 Dec4 = GT
-type instance CompareDigit Dec8 Dec5 = GT
-type instance CompareDigit Dec8 Dec6 = GT
-type instance CompareDigit Dec8 Dec7 = GT
-type instance CompareDigit Dec8 Dec8 = EQ
-type instance CompareDigit Dec8 Dec9 = LT
-
-type instance CompareDigit Dec9 Dec0 = GT
-type instance CompareDigit Dec9 Dec1 = GT
-type instance CompareDigit Dec9 Dec2 = GT
-type instance CompareDigit Dec9 Dec3 = GT
-type instance CompareDigit Dec9 Dec4 = GT
-type instance CompareDigit Dec9 Dec5 = GT
-type instance CompareDigit Dec9 Dec6 = GT
-type instance CompareDigit Dec9 Dec7 = GT
-type instance CompareDigit Dec9 Dec8 = GT
-type instance CompareDigit Dec9 Dec9 = EQ
-
-type instance Compare (Dec x) (Dec y) = Compare' x y
-type family Compare' x y
-type instance Compare' (Neg' x)   (Neg' y)   = CompareNeg (ComparePos x y EQ)
-type instance Compare' (Neg' x)   DecN       = LT
-type instance Compare' (Neg' x)   (yh :. yl) = LT
-type instance Compare' DecN       (Neg' y)   = GT
-type instance Compare' DecN       DecN       = EQ
-type instance Compare' DecN       (yh :. yl) = LT
-type instance Compare' (xh :. xl) (Neg' y)   = GT
-type instance Compare' (xh :. xl) DecN       = GT
-type instance Compare' (xh :. xl) (yh :. yl) = ComparePos (xh :. xl) (yh :. yl) EQ
-
-type family ComparePos x y c
-type instance ComparePos DecN       DecN       c = c
-type instance ComparePos DecN       (yh :. yl) c = LT
-type instance ComparePos (xh :. xl) DecN       c = GT
-type instance ComparePos (xh :. xl) (yh :. yl) GT = ComparePos' xh yh (CompareDigit xl yl) GT
-type instance ComparePos (xh :. xl) (yh :. yl) EQ = ComparePos xh yh (CompareDigit xl yl)
-type instance ComparePos (xh :. xl) (yh :. yl) LT = ComparePos' xh yh (CompareDigit xl yl) LT
-
-type family ComparePos' x y c l
-type instance ComparePos' x y LT c = ComparePos x y LT
-type instance ComparePos' x y EQ c = ComparePos x y c
-type instance ComparePos' x y GT c = ComparePos x y GT
-
-type family CompareNeg c
-type instance CompareNeg LT = GT
-type instance CompareNeg EQ = EQ
-type instance CompareNeg GT = LT
diff --git a/Types/Data/Num/Ops.hs b/Types/Data/Num/Ops.hs
deleted file mode 100644
--- a/Types/Data/Num/Ops.hs
+++ /dev/null
@@ -1,185 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Decimal.Ops
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Num.Ops
-    ( (:.)
-    , Neg
-    , negT
-    , IsPositive
-    , isPositiveT
-    , IsZero
-    , isZeroT
-    , IsNegative
-    , isNegativeT
-    , Succ
-    , succT
-    , Pred
-    , predT
-    , IsEven
-    , isEvenT
-    , IsOdd
-    , isOddT
-    , (:+:)
-    , addT
-    , (:-:)
-    , subT
-    , (:*:)
-    , mulT
-    , Mul2
-    , mul2T
-    , Pow2
-    , pow2T
-    , DivMod
-    , divModT
-    , Div
-    , divT
-    , Mod
-    , modT
-    , Div2
-    , div2T
-    , Fac
-    , facT
-    , IntegerR (..)
-    , IntegerT (..)
-    , NaturalT
-    , PositiveT
-    , NegativeT
-    , reifyPositive
-    , reifyNegative
-    ) where
-
-import Types.Data.Bool
-
-data ds :. d
-instance (Show ds, Show d) => Show (ds :. d) where
-    show _ = show (undefined :: ds) ++ show (undefined :: d)
-
--- | @Neg x@ evaluates to the additive inverse of (i.e., minus) @x@.
-type family Neg x
-negT :: x -> Neg x
-negT _ = undefined
-
-type family IsPositive x
-isPositiveT :: x -> IsPositive x
-isPositiveT _ = undefined
-
-type family IsZero x
-isZeroT :: x -> IsZero x
-isZeroT _ = undefined
-
-type family IsNegative x
-isNegativeT :: x -> IsNegative x
-isNegativeT _ = undefined
-
-type family Succ x
-succT :: x -> Succ x
-succT _ = undefined
-
-type family Pred x
-predT :: x -> Pred x
-predT _ = undefined
-
-type family IsEven x
-isEvenT :: x -> IsEven x
-isEvenT _ = undefined
-
-type family IsOdd x
-type instance IsOdd x = Not (IsEven x)
-isOddT :: x -> IsOdd x
-isOddT _ = undefined
-
-type family x :+: y
-addT :: x -> y -> x :+: y
-addT _ _ = undefined
-
-type family x :-: y
-subT :: x -> y -> x :-: y
-subT _ _ = undefined
-
-type family x :*: y
-mulT :: x -> y -> x :*: y
-mulT _ _ = undefined
-
-type family Mul2 x
-mul2T :: x -> Mul2 x
-mul2T _ = undefined
-
-type family DivMod x y
-divModT :: x -> y -> DivMod x y
-divModT _ _ = undefined
-
-type family Div x y
-divT :: x -> y -> Div x y
-divT _ _ = undefined
-
-type family Mod x y
-modT :: x -> y -> Mod x y
-modT _ _ = undefined
-
-type family Div2 x
-div2T :: x -> Div2 x
-div2T _ = undefined
-
-type family Fac x
-facT :: x -> Fac x
-facT _ = undefined
-
-type family Pow2 x
-pow2T :: x -> Pow2 x
-pow2T _ = undefined
-
-class IntegerT x => NaturalT x
-instance (IntegerT x, IsNegative x ~ False) => NaturalT x
-
-class IntegerT x => PositiveT x
-instance (IntegerT x, IsPositive x ~ True) => PositiveT x
-class IntegerT x => NegativeT x
-instance (IntegerT x, IsNegative x ~ True) => NegativeT x
-
-class (IntegerR (Repr x)) => IntegerT x where
-    fromIntegerT :: Num y => x -> y
-    type Repr x
-
-class IntegerR r where
-    reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> a
-
-
---- positive and negative assertions: unsafe, in a trusted kernel
-data AssertPos x
-data AssertNeg x
-
-assertPos :: x -> AssertPos x
-assertPos _ = undefined
-
-assertNeg :: x -> AssertNeg x
-assertNeg _ = undefined
-
-type instance IsPositive (AssertPos x) = True
-type instance IsNegative (AssertNeg x) = True
-
-instance IntegerT x => IntegerT (AssertPos x) where 
-    fromIntegerT _ = fromIntegerT (undefined :: x)
-    type Repr (AssertPos x) = Repr x
-
-instance IntegerT x => IntegerT (AssertNeg x) where
-    fromIntegerT _ = fromIntegerT (undefined :: x)
-    type Repr (AssertNeg x) = Repr x
-
-reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a
-reifyPositive r n k | n > 0     = Just (reifyIntegral r n (k . assertPos))
-                    | otherwise = Nothing
-
-reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a
-reifyNegative r n k | n < 0     = Just (reifyIntegral r n (k . assertNeg))
-                    | otherwise = Nothing
diff --git a/Types/Data/Ord.hs b/Types/Data/Ord.hs
deleted file mode 100644
--- a/Types/Data/Ord.hs
+++ /dev/null
@@ -1,128 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Types.Data.Decimal.Digits
--- Copyright   :  (c) 2008 Peter Gavin
--- License     :  BSD-style (see the file LICENSE)
--- 
--- Maintainer  :  pgavin@gmail.com
--- Stability   :  experimental
--- Portability :  non-portable (type families, requires ghc >= 6.9)
---
--- Type-level numerical operations using type families.
--- 
-----------------------------------------------------------------------------
-
-module Types.Data.Ord
-    ( Compare
-    , compareT
-    , LT
-    , EQ
-    , GT
-    , IsLT
-    , isLTT
-    , IsEQ
-    , isEQT
-    , IsGT
-    , isGTT
-    , (:<:)
-    , ltT
-    , (:<=:)
-    , leT
-    , (:==:)
-    , eqT
-    , (:>=:)
-    , geT
-    , (:>:)
-    , gtT
-    , Min
-    , minT
-    , Max
-    , maxT
-    ) where
-
-import qualified Prelude
-
-import Types.Data.Bool
-
-type family Compare x y
-data LT
-data EQ
-data GT
-compareT :: x -> y -> Compare x y
-compareT _ _ = Prelude.undefined
-
-type family IsLT c
-type instance IsLT LT = True
-type instance IsLT EQ = False
-type instance IsLT GT = False
-isLTT :: c -> IsLT c
-isLTT _ = Prelude.undefined
-
-type family IsEQ c
-type instance IsEQ LT = False
-type instance IsEQ EQ = True
-type instance IsEQ GT = False
-isEQT :: c -> IsEQ c
-isEQT _ = Prelude.undefined
-
-type family IsGT c
-type instance IsGT LT = False
-type instance IsGT EQ = False
-type instance IsGT GT = True
-isGTT :: c -> IsGT c
-isGTT _ = Prelude.undefined
-
-type instance Compare LT LT = EQ
-type instance Compare LT EQ = LT
-type instance Compare LT GT = LT
-type instance Compare EQ LT = GT
-type instance Compare EQ EQ = EQ
-type instance Compare EQ GT = LT
-type instance Compare GT LT = GT
-type instance Compare GT EQ = GT
-type instance Compare GT GT = EQ
-
-type family x :<: y
-type instance x :<: y = IsLT (Compare x y)
-ltT :: x -> y -> x :<: y
-ltT _ _ = Prelude.undefined
-
-type family x :<=: y
-type instance x :<=: y = Not (x :>: y)
-leT :: x -> y -> x :<=: y
-leT _ _ = Prelude.undefined
-
-type family x :==: y
-type instance x :==: y = IsEQ (Compare x y)
-eqT :: x -> y -> x :==: y
-eqT _ _ = Prelude.undefined
-
-type family x :/=: y
-type instance x :/=: y = Not (x :==: y)
-neT :: x -> y -> x :/=: y
-neT _ _ = Prelude.undefined
-
-type family x :>=: y
-type instance x :>=: y = Not (x :<: y)
-geT :: x -> y -> x :>=: y
-geT _ _ = Prelude.undefined
-
-type family x :>: y
-type instance x :>: y = IsGT (Compare x y)
-gtT :: x -> y -> x :>: y
-gtT _ _ = Prelude.undefined
-
-type family Min x y
-type instance Min x y = If (x :<=: y) x y
-minT :: x -> y -> Min x y
-minT _ _ = Prelude.undefined
-
-type family Max x y
-type instance Max x y = If (x :>=: y) x y
-maxT :: x -> y -> Max x y
-maxT _ _ = Prelude.undefined
-
-type instance Compare False False = EQ
-type instance Compare False True  = LT
-type instance Compare True  False = GT
-type instance Compare True  True  = EQ
diff --git a/src/Data/SizedInt.hs b/src/Data/SizedInt.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/SizedInt.hs
@@ -0,0 +1,178 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.SizedInt
+    ( SizedInt ) where
+
+import Data.Bits
+          (Bits, shiftL, shiftR, rotateL, rotateR, bit, testBit, popCount,
+           complement, xor, bitSize, isSigned, (.&.), (.|.), )
+
+import qualified Type.Data.Num as Num
+import Type.Base.Proxy (Proxy(Proxy))
+
+
+newtype SizedInt nT = SizedInt Integer
+
+_sizeT :: SizedInt nT -> Proxy nT
+_sizeT _ = Proxy
+
+mask :: forall nT . Num.Natural nT => Proxy nT -> Integer
+mask n = bit (Num.fromInteger n) - 1
+
+signBit :: forall nT . Num.Natural nT => Proxy nT -> Int
+signBit n = Num.fromInteger n - 1
+
+isNegative :: forall nT . Num.Natural nT
+           => SizedInt nT
+           -> Bool
+isNegative (SizedInt x) =
+    testBit x $ signBit (Proxy :: Proxy nT)
+
+instance Num.Natural nT => Eq (SizedInt nT) where
+    (SizedInt x) == (SizedInt y) = x == y
+    (SizedInt x) /= (SizedInt y) = x /= y
+
+instance Num.Natural nT => Show (SizedInt nT) where
+    showsPrec prec n =
+        showsPrec prec $ toInteger n
+
+instance Num.Natural nT => Read (SizedInt nT) where
+    readsPrec prec str0 =
+        [ (fromInteger n, str)
+        | (n, str) <- readsPrec prec str0 ]
+
+instance Num.Natural nT => Ord (SizedInt nT) where
+    a `compare` b = toInteger a `compare` toInteger b
+
+instance Num.Natural nT => Bounded (SizedInt nT) where
+    minBound = SizedInt $ negate $ 1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - 1)
+    maxBound = SizedInt $ (1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - 1)) - 1
+
+instance Num.Natural nT => Enum (SizedInt nT) where
+    succ x
+       | x == maxBound  = error $ "Enum.succ{" ++ showSizedIntType x ++ "}: tried to take `succ' of maxBound"
+       | otherwise      = x + 1
+    pred x
+       | x == minBound  = error $ "Enum.succ{" ++ showSizedIntType x ++ "}: tried to take `pred' of minBound"
+       | otherwise      = x - 1
+    
+    fromEnum s@(SizedInt x)
+        | x > toInteger (maxBound :: Int) =
+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: Int"
+        | x < toInteger (minBound :: Int) =
+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: Int"
+        | otherwise =
+            fromInteger x
+    toEnum x
+        | x' > toInteger (maxBound :: SizedInt nT) =
+            error $ "Enum.fromEnum{" ++ showSizedIntTypeProxy n ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: " ++ showSizedIntTypeProxy n
+        | x' < toInteger (minBound :: SizedInt nT) =
+            error $ "Enum.fromEnum{" ++ showSizedIntTypeProxy n ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: " ++ showSizedIntTypeProxy n
+        | otherwise =
+            fromInteger x'
+            where x' = toInteger x
+                  n = Proxy :: Proxy nT
+
+instance Num.Natural nT => Num (SizedInt nT) where
+    (SizedInt a) + (SizedInt b) =
+        fromInteger $ a + b
+    (SizedInt a) * (SizedInt b) =
+        fromInteger $ a * b
+    negate (SizedInt n) =
+        fromInteger $ (n `xor` mask (Proxy :: Proxy nT)) + 1
+    a - b =
+        a + (negate b)
+
+    fromInteger n =
+      let fromCardinal m = SizedInt $ m .&. mask (Proxy :: Proxy nT)
+      in  if n>=0
+            then fromCardinal n
+            else negate $ fromCardinal $ negate n
+
+    abs s
+      | isNegative s =
+          negate s
+      | otherwise =
+          s
+    signum s
+      | isNegative s =
+          -1
+      | s == 0 =
+          0
+      | otherwise =
+          1
+
+instance Num.Natural nT => Real (SizedInt nT) where
+    toRational n = toRational $ toInteger n
+
+instance Num.Natural nT => Integral (SizedInt nT) where
+    a `quot` b =
+        fromInteger $ toInteger a `quot` toInteger b
+    a `rem` b =
+        fromInteger $ toInteger a `rem` toInteger b
+    a `div` b =
+        fromInteger $ toInteger a `div` toInteger b
+    a `mod` b =
+        fromInteger $ toInteger a `mod` toInteger b
+    a `quotRem` b =
+        let (quot_, rem_) = toInteger a `quotRem` toInteger b
+        in (fromInteger quot_, fromInteger rem_)
+    a `divMod` b =
+        let (div_, mod_) = toInteger a `divMod` toInteger b
+        in (fromInteger div_, fromInteger mod_)
+    toInteger s@(SizedInt x) =
+        if isNegative s
+           then let SizedInt x' = negate s in negate x'
+           else x
+
+instance Num.Natural nT => Bits (SizedInt nT) where
+    (SizedInt a) .&. (SizedInt b) = SizedInt $ a .&. b
+    (SizedInt a) .|. (SizedInt b) = SizedInt $ a .|. b
+    (SizedInt a) `xor` SizedInt b = SizedInt $ a `xor` b
+    complement (SizedInt x) = SizedInt $ x `xor` mask (Proxy :: Proxy nT)
+    bit b =
+      case SizedInt $ bit b of
+        s | b < 0 -> error $ "Bits.bit{" ++ showSizedIntType s ++ "}: tried to set negative position"
+          | b >= bitSize s -> error $ "Bits.bit{" ++ showSizedIntType s ++ "}: tried to set too large position"
+          | otherwise -> s
+    s@(SizedInt x) `testBit` b
+      | b < 0 = error $ "Bits.testBit{" ++ showSizedIntType s ++ "}: tried to test negative position"
+      | b >= bitSize s = error $ "Bits.testBit{" ++ showSizedIntType s ++ "}: tried to test too large position"
+      | otherwise =
+         testBit x b
+    s@(SizedInt x) `shiftL` b
+      | b < 0 = error $ "Bits.shiftL{" ++ showSizedIntType s ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedInt $ mask (Proxy :: Proxy nT) .&. (x `shiftL` b)
+    s@(SizedInt x) `shiftR` b
+      | b < 0 = error $ "Bits.shiftR{" ++ showSizedIntType s ++ "}: tried to shift by negative amount"
+      | isNegative s =
+        SizedInt $ mask (Proxy :: Proxy nT) .&.
+            ((x `shiftR` b) .|. (mask (Proxy :: Proxy nT) `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - b)))
+      | otherwise =
+        SizedInt $ (mask (Proxy :: Proxy nT)) .&. (x `shiftR` b)
+    s@(SizedInt a) `rotateL` b
+      | b < 0 =
+        error $ "Bits.rotateL{" ++ showSizedIntType s ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedInt $ mask (Proxy :: Proxy nT) .&.
+            ((a `shiftL` b) .|. (a `shiftR` (Num.fromInteger (Proxy :: Proxy nT) - b)))
+    s@(SizedInt a) `rotateR` b
+      | b < 0 =
+        error $ "Bits.rotateR{" ++ showSizedIntType s ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedInt $ mask (Proxy :: Proxy nT) .&.
+            ((a `shiftR` b) .|. (a `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - b)))
+    popCount (SizedInt x) = popCount x
+    bitSize _ = Num.fromInteger (Proxy :: Proxy nT)
+    isSigned _ = True
+
+
+showSizedIntTypeProxy :: forall nT. Num.Natural nT => Proxy nT -> String
+showSizedIntTypeProxy n =
+   "SizedInt " ++ show (Num.fromInteger n :: Integer)
+
+showSizedIntType :: forall nT. Num.Natural nT => SizedInt nT -> String
+showSizedIntType _ = showSizedIntTypeProxy (Proxy :: Proxy nT)
diff --git a/src/Data/SizedWord.hs b/src/Data/SizedWord.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/SizedWord.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.SizedWord
+    ( SizedWord ) where
+
+import Data.Bits
+          (Bits, shiftL, shiftR, rotateL, rotateR, bit, testBit, popCount,
+           complement, xor, bitSize, isSigned, (.&.), (.|.), )
+
+import qualified Type.Data.Num as Num
+import Type.Base.Proxy (Proxy(Proxy))
+
+
+newtype SizedWord nT = SizedWord Integer
+
+sizeT :: SizedWord nT -> Proxy nT
+sizeT _ = Proxy
+
+mask :: forall nT . Num.Natural nT => Proxy nT -> Integer
+mask n = bit (Num.fromInteger n) - 1
+
+instance Num.Natural nT => Eq (SizedWord nT) where
+    (SizedWord x) == (SizedWord y) = x == y
+    (SizedWord x) /= (SizedWord y) = x /= y
+
+instance Num.Natural nT => Show (SizedWord nT) where
+    showsPrec prec n =
+        showsPrec prec $ toInteger n
+
+instance Num.Natural nT => Read (SizedWord nT) where
+    readsPrec prec str0 =
+        [ (fromInteger n, str)
+        | (n, str) <- readsPrec prec str0 ]
+
+instance Num.Natural nT => Ord (SizedWord nT) where
+    a `compare` b = toInteger a `compare` toInteger b
+
+instance Num.Natural nT => Bounded (SizedWord nT) where
+    minBound = 0
+    maxBound = SizedWord $ (1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT))) - 1
+
+instance Num.Natural nT => Enum (SizedWord nT) where
+    succ x
+       | x == maxBound  = error $ "Enum.succ{" ++ showSizedWordType x ++ "}: tried to take `succ' of maxBound"
+       | otherwise      = x + 1
+    pred x
+       | x == minBound  = error $ "Enum.succ{" ++ showSizedWordType x ++ "}: tried to take `pred' of minBound"
+       | otherwise      = x - 1
+    
+    fromEnum s@(SizedWord x)
+        | x > toInteger (maxBound :: Int) =
+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: Int"
+        | x < toInteger (minBound :: Int) =
+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: Int"
+        | otherwise =
+            fromInteger x
+    toEnum x
+        | x > fromIntegral (maxBound :: SizedWord nT) =
+            error $ "Enum.fromEnum{" ++ showSizedWordTypeProxy n ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: " ++ showSizedWordTypeProxy n
+        | x < fromIntegral (minBound :: SizedWord nT) =
+            error $ "Enum.fromEnum{" ++ showSizedWordTypeProxy n ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: " ++ showSizedWordTypeProxy n
+        | otherwise =
+            fromInteger $ toInteger x
+            where n = Proxy :: Proxy nT
+
+instance Num.Natural nT => Num (SizedWord nT) where
+    (SizedWord a) + (SizedWord b) =
+        fromInteger $ a + b
+    (SizedWord a) * (SizedWord b) =
+        fromInteger $ a * b
+    negate s@(SizedWord n) =
+        fromInteger $ (n `xor` mask (sizeT s)) + 1
+    a - b =
+        a + (negate b)
+
+    fromInteger n =
+      let fromCardinal m = SizedWord $ m .&. mask (Proxy :: Proxy nT)
+      in  if n>=0
+            then fromCardinal n
+            else negate $ fromCardinal $ negate n
+
+    abs s = s
+    signum s
+      | s == 0 =
+          0
+      | otherwise =
+          1
+
+instance Num.Natural nT => Real (SizedWord nT) where
+    toRational n = toRational $ toInteger n
+
+instance Num.Natural nT => Integral (SizedWord nT) where
+    a `quot` b =
+        fromInteger $ toInteger a `quot` toInteger b
+    a `rem` b =
+        fromInteger $ toInteger a `rem` toInteger b
+    a `div` b =
+        fromInteger $ toInteger a `div` toInteger b
+    a `mod` b =
+        fromInteger $ toInteger a `mod` toInteger b
+    a `quotRem` b =
+        let (quot_, rem_) = toInteger a `quotRem` toInteger b
+        in (fromInteger quot_, fromInteger rem_)
+    a `divMod` b =
+        let (div_, mod_) = toInteger a `divMod` toInteger b
+        in (fromInteger div_, fromInteger mod_)
+    toInteger (SizedWord x) = x
+
+instance Num.Natural nT => Bits (SizedWord nT) where
+    (SizedWord a) .&. (SizedWord b) = SizedWord $ a .&. b
+    (SizedWord a) .|. (SizedWord b) = SizedWord $ a .|. b
+    (SizedWord a) `xor` SizedWord b = SizedWord $ a `xor` b
+    complement (SizedWord x) = SizedWord $ x `xor` mask (Proxy :: Proxy nT)
+    bit b =
+      case SizedWord $ bit b of
+        s | b < 0 -> error $ "Bits.bit{" ++ showSizedWordType s ++ "}: tried to set negative position"
+          | b >= bitSize s -> error $ "Bits.bit{" ++ showSizedWordType s ++ "}: tried to set too large position"
+          | otherwise -> s
+    s@(SizedWord x) `testBit` b
+      | b < 0 = error $ "Bits.testBit{" ++ showSizedWordType s ++ "}: tried to test negative position"
+      | b >= bitSize s = error $ "Bits.testBit{" ++ showSizedWordType s ++ "}: tried to test too large position"
+      | otherwise =
+         testBit x b
+    s@(SizedWord x) `shiftL` b
+      | b < 0 = error $ "Bits.shiftL{" ++ showSizedWordType s ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedWord $ mask (Proxy :: Proxy nT) .&. (x `shiftL` b)
+    s@(SizedWord x) `shiftR` b
+      | b < 0 = error $ "Bits.shiftR{" ++ showSizedWordType s ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedWord $ (x `shiftR` b)
+    s@(SizedWord x) `rotateL` b
+      | b < 0 =
+        error $ "Bits.rotateL{" ++ showSizedWordType s ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedWord $ mask (Proxy :: Proxy nT) .&.
+            ((x `shiftL` b) .|. (x `shiftR` (bitSize s - b)))
+    s@(SizedWord x) `rotateR` b
+      | b < 0 =
+        error $ "Bits.rotateR{" ++ showSizedWordType s ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedWord $ mask (Proxy :: Proxy nT) .&.
+            ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))
+    popCount (SizedWord x) = popCount x
+    bitSize _ = Num.fromInteger (Proxy :: Proxy nT)
+    isSigned _ = False
+
+showSizedWordTypeProxy :: forall nT. Num.Natural nT => Proxy nT -> String
+showSizedWordTypeProxy n =
+   "SizedWord " ++ show (Num.fromInteger n :: Integer)
+
+showSizedWordType :: forall nT. Num.Natural nT => SizedWord nT -> String
+showSizedWordType _ = showSizedWordTypeProxy (Proxy :: Proxy nT)
diff --git a/src/Type/Base/Proxy.hs b/src/Type/Base/Proxy.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Base/Proxy.hs
@@ -0,0 +1,24 @@
+module Type.Base.Proxy where
+
+import Control.Applicative (Applicative, pure, (<*>), )
+
+import qualified Prelude as P
+import Prelude (String, Eq, Functor, fmap)
+
+
+data Proxy a = Proxy
+   deriving (Eq)
+
+instance Functor Proxy where
+   fmap _f Proxy = Proxy
+
+instance Applicative Proxy where
+   pure _ = Proxy
+   Proxy <*> Proxy = Proxy
+
+
+class Show a where
+   showsPrec :: P.Int -> Proxy a -> P.ShowS
+
+instance Show a => P.Show (Proxy a) where
+   showsPrec = showsPrec
diff --git a/src/Type/Data/Bool.hs b/src/Type/Data/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Bool.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE GADTs #-}
+
+module Type.Data.Bool
+    ( C(switch)
+    , Singleton(False, True)
+    , singleton
+    , True
+    , true
+    , False
+    , false
+    , Not
+    , not
+    , (:&&:)
+    , and
+    , (:||:)
+    , or
+    , If
+    , if_
+    ) where
+
+import Type.Base.Proxy (Proxy(Proxy))
+import Data.Typeable (Typeable)
+
+import qualified Prelude
+
+
+class C bool where switch :: f False -> f True -> f bool
+instance C False where switch f _ = f
+instance C True where switch _ f = f
+
+data Singleton bool where
+    False :: Singleton False
+    True :: Singleton True
+
+singleton :: (C bool) => Singleton bool
+singleton = switch False True
+
+data True deriving (Typeable)
+true :: Proxy True
+true = Proxy
+instance Prelude.Show True where
+    show _ = "True"
+data False deriving (Typeable)
+false :: Proxy False
+false = Proxy
+instance Prelude.Show False where
+    show _ = "False"
+
+type family Not x
+type instance Not False = True
+type instance Not True  = False
+not :: Proxy x -> Proxy (Not x)
+not Proxy = Proxy
+
+type family x :&&: y
+type instance False :&&: _x = False
+type instance True  :&&: x = x
+and :: Proxy x -> Proxy y -> Proxy (x :&&: y)
+and Proxy Proxy = Proxy
+
+type family x :||: y
+type instance True  :||: _x = True
+type instance False :||: x = x
+or :: Proxy x -> Proxy y -> Proxy (x :||: y)
+or Proxy Proxy = Proxy
+
+type family If x y z
+type instance If True y _z = y
+type instance If False _y z = z
+if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z)
+if_ Proxy Proxy Proxy = Proxy
diff --git a/src/Type/Data/List.hs b/src/Type/Data/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/List.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+module Type.Data.List
+    ( Cons
+    , Null
+    , IsNull
+    , Head
+    , Tail
+    , Reverse
+    , Append
+    ) where
+
+import qualified Prelude
+
+import Data.Typeable
+
+import Type.Data.Bool
+
+data Cons car cdr deriving (Typeable)
+instance (Prelude.Show car, Prelude.Show cdr) => Prelude.Show (Cons car cdr) where
+    show = showCons
+
+showCons :: forall car cdr . (Prelude.Show car, Prelude.Show cdr) => Cons car cdr -> Prelude.String
+showCons _ = "Cons (" Prelude.++ Prelude.show (Prelude.undefined :: car) Prelude.++ ") (" Prelude.++ Prelude.show (Prelude.undefined :: cdr) Prelude.++ ")"
+
+data Null deriving (Typeable)
+instance Prelude.Show Null where
+    show _ = ""
+
+type family IsNull l
+type instance IsNull (Cons _car _cdr) = False
+type instance IsNull Null = True
+
+type family Head l
+type instance Head (Cons car _cdr) = car
+
+type family Tail l
+type instance Tail (Cons _car cdr) = cdr
+
+type family Reverse l
+type instance Reverse l = Reverse' l Null
+
+type family Reverse' l a
+type instance Reverse' Null a = a
+type instance Reverse' (Cons car cdr) a = Reverse' cdr (Cons car a)
+
+type family Append l1 l2
+type instance Append Null l2 = l2
+type instance Append (Cons car1 cdr2) l2 = Cons car1 (Append cdr2 l2)
diff --git a/src/Type/Data/Num.hs b/src/Type/Data/Num.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num.hs
@@ -0,0 +1,267 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Type.Data.Num
+    ( Negate
+    , negate
+    , IsPositive
+    , isPositive
+    , IsZero
+    , isZero
+    , IsNegative
+    , isNegative
+    , IsNatural
+    , isNatural
+    , One
+    , one
+    , Succ
+    , succ
+    , Pred
+    , pred
+    , IsEven
+    , isEven
+    , IsOdd
+    , isOdd
+    , (:+:)
+    , add
+    , (:-:)
+    , sub
+    , (:*:)
+    , mul
+    , Mul2
+    , mul2
+    , Pow2
+    , pow2
+    , Log2Ceil
+    , log2Ceil
+    , DivMod
+    , divMod
+    , Div
+    , div
+    , Mod
+    , mod
+    , Div2
+    , div2
+    , Fac
+    , fac
+    , Singleton(..)
+    , Representation (..)
+    , Integer (..)
+    , Natural
+    , Positive
+    , Negative
+    , integerFromSingleton
+    , integralFromSingleton
+    , singletonFromProxy
+    , integralFromProxy
+    , fromInteger
+    , reifyPositive
+    , reifyNegative
+    , reifyNatural
+    ) where
+
+import Type.Data.Bool (False, True, Not)
+import Type.Base.Proxy (Proxy(Proxy))
+import Data.Maybe.HT (toMaybe)
+
+import qualified Prelude as P
+import Prelude (Num, Maybe, (.), (<), (>), (>=))
+
+
+-- | @Negate x@ evaluates to the additive inverse of (i.e., minus) @x@.
+type family Negate x
+negate :: Proxy x -> Proxy (Negate x)
+negate Proxy = Proxy
+
+type family IsPositive x
+isPositive :: Proxy x -> Proxy (IsPositive x)
+isPositive Proxy = Proxy
+
+type family IsZero x
+isZero :: Proxy x -> Proxy (IsZero x)
+isZero Proxy = Proxy
+
+type family IsNegative x
+isNegative :: Proxy x -> Proxy (IsNegative x)
+isNegative Proxy = Proxy
+
+type family IsNatural x
+isNatural :: Proxy x -> Proxy (IsNatural x)
+isNatural Proxy = Proxy
+
+type family One repr
+one :: Proxy repr -> Proxy (One repr)
+one Proxy = Proxy
+
+type family Succ x
+succ :: Proxy x -> Proxy (Succ x)
+succ Proxy = Proxy
+
+type family Pred x
+pred :: Proxy x -> Proxy (Pred x)
+pred Proxy = Proxy
+
+type family IsEven x
+isEven :: Proxy x -> Proxy (IsEven x)
+isEven Proxy = Proxy
+
+type family IsOdd x
+type instance IsOdd x = Not (IsEven x)
+isOdd :: Proxy x -> Proxy (IsOdd x)
+isOdd Proxy = Proxy
+
+type family x :+: y
+add :: Proxy x -> Proxy y -> Proxy (x :+: y)
+add Proxy Proxy = Proxy
+
+type family x :-: y
+sub :: Proxy x -> Proxy y -> Proxy (x :-: y)
+sub Proxy Proxy = Proxy
+
+type family x :*: y
+mul :: Proxy x -> Proxy y -> Proxy (x :*: y)
+mul Proxy Proxy = Proxy
+
+type family Mul2 x
+mul2 :: Proxy x -> Proxy (Mul2 x)
+mul2 Proxy = Proxy
+
+type family DivMod x y
+divMod :: Proxy x -> Proxy y -> Proxy (DivMod x y)
+divMod Proxy Proxy = Proxy
+
+type family Div x y
+div :: Proxy x -> Proxy y -> Proxy (Div x y)
+div Proxy Proxy = Proxy
+
+type family Mod x y
+mod :: Proxy x -> Proxy y -> Proxy (Mod x y)
+mod Proxy Proxy = Proxy
+
+type family Div2 x
+div2 :: Proxy x -> Proxy (Div2 x)
+div2 Proxy = Proxy
+
+type family Fac x
+fac :: Proxy x -> Proxy (Fac x)
+fac Proxy = Proxy
+
+type instance Fac x = FacRec x (IsZero x)
+type family FacRec x is0
+type instance FacRec x True = One (Repr x)
+-- peasant multiplication is faster if second factor is small
+type instance FacRec x False = Fac (Pred x) :*: x
+
+
+
+type family Pow2 x
+pow2 :: Proxy x -> Proxy (Pow2 x)
+pow2 Proxy = Proxy
+
+type family Log2Ceil x
+log2Ceil :: Proxy x -> Proxy (Log2Ceil x)
+log2Ceil Proxy = Proxy
+
+class Integer x => Natural x
+instance (Integer x, IsNatural x  ~ True) => Natural x
+class Integer x => Positive x
+instance (Integer x, IsPositive x ~ True) => Positive x
+class Integer x => Negative x
+instance (Integer x, IsNegative x ~ True) => Negative x
+
+class (Representation (Repr x)) => Integer x where
+    singleton :: Singleton x
+    type Repr x
+
+class Representation r where
+    reifyIntegral ::
+        Proxy r -> P.Integer ->
+        (forall s. (Integer s, Repr s ~ r) => Proxy s -> a) ->
+        a
+
+
+newtype Singleton d = Singleton P.Integer
+
+
+integerFromSingleton :: (Integer x) => Singleton x -> P.Integer
+integerFromSingleton (Singleton n) = n
+
+integralFromSingleton :: (Integer x, Num y) => Singleton x -> y
+integralFromSingleton = P.fromInteger . integerFromSingleton
+
+singletonFromProxy :: (Integer x) => Proxy x -> Singleton x
+singletonFromProxy Proxy = singleton
+
+integralFromProxy :: (Integer x, Num y) => Proxy x -> y
+integralFromProxy = integralFromSingleton . singletonFromProxy
+
+-- | synonym for 'integralFromProxy', kept for backward compatibility
+fromInteger :: (Integer x, Num y) => Proxy x -> y
+fromInteger = integralFromProxy
+
+
+--- positive and negative assertions: unsafe, in a trusted kernel
+data AssertPos x
+data AssertNeg x
+data AssertNat x
+
+assertPos :: Proxy x -> Proxy (AssertPos x)
+assertPos Proxy = Proxy
+
+assertNeg :: Proxy x -> Proxy (AssertNeg x)
+assertNeg Proxy = Proxy
+
+assertNat :: Proxy x -> Proxy (AssertNat x)
+assertNat Proxy = Proxy
+
+type instance IsPositive (AssertPos _x) = True
+type instance IsPositive (AssertNeg _x) = False
+
+type instance IsNegative (AssertPos _x) = False
+type instance IsNegative (AssertNeg _x) = True
+type instance IsNegative (AssertNat _x) = False
+
+type instance IsNatural  (AssertPos _x) = True
+type instance IsNatural  (AssertNeg _x) = False
+type instance IsNatural  (AssertNat _x) = True
+
+instance Integer x => Integer (AssertPos x) where 
+    singleton = case singleton :: Singleton x of Singleton n -> Singleton n
+    type Repr (AssertPos x) = Repr x
+
+instance Integer x => Integer (AssertNeg x) where
+    singleton = case singleton :: Singleton x of Singleton n -> Singleton n
+    type Repr (AssertNeg x) = Repr x
+
+instance Integer x => Integer (AssertNat x) where
+    singleton = case singleton :: Singleton x of Singleton n -> Singleton n
+    type Repr (AssertNat x) = Repr x
+
+reifyPositive ::
+    Representation r =>
+    Proxy r -> P.Integer ->
+    (forall s. (Positive s, Repr s ~ r) => Proxy s -> a) ->
+    Maybe a
+reifyPositive r n k =
+    toMaybe (n > 0) (reifyIntegral r n (k . assertPos))
+
+reifyNegative ::
+    Representation r =>
+    Proxy r -> P.Integer ->
+    (forall s. (Negative s, Repr s ~ r) => Proxy s -> a) ->
+    Maybe a
+reifyNegative r n k =
+    toMaybe (n < 0) (reifyIntegral r n (k . assertNeg))
+
+reifyNatural ::
+    Representation r =>
+    Proxy r -> P.Integer ->
+    (forall s. (Natural s, Repr s ~ r) => Proxy s -> a) ->
+    Maybe a
+reifyNatural r n k =
+    toMaybe (n >= 0) (reifyIntegral r n (k . assertNat))
diff --git a/src/Type/Data/Num/Decimal.hs b/src/Type/Data/Num/Decimal.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal.hs
@@ -0,0 +1,7 @@
+module Type.Data.Num.Decimal
+    ( module Type.Data.Num.Decimal.Literal
+    , module Type.Data.Num.Decimal.Number
+    ) where
+
+import Type.Data.Num.Decimal.Literal
+import Type.Data.Num.Decimal.Number
diff --git a/src/Type/Data/Num/Decimal/Digit.hs b/src/Type/Data/Num/Decimal/Digit.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal/Digit.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Type.Data.Num.Decimal.Digit where
+
+import qualified Type.Data.Num.Unary.Literal as UnaryLit
+
+import Type.Base.Proxy (Proxy(Proxy))
+
+import Data.Typeable (Typeable)
+
+
+newtype Singleton d = Singleton Int
+
+singleton :: (C d) => Singleton d
+singleton =
+    switch
+        (Singleton 0)
+        (Singleton 1)
+        (Singleton 2)
+        (Singleton 3)
+        (Singleton 4)
+        (Singleton 5)
+        (Singleton 6)
+        (Singleton 7)
+        (Singleton 8)
+        (Singleton 9)
+
+class C d where
+    switch ::
+        f Dec0 ->
+        f Dec1 ->
+        f Dec2 ->
+        f Dec3 ->
+        f Dec4 ->
+        f Dec5 ->
+        f Dec6 ->
+        f Dec7 ->
+        f Dec8 ->
+        f Dec9 ->
+        f d
+
+class C d => Pos d where
+    switchPos ::
+        f Dec1 ->
+        f Dec2 ->
+        f Dec3 ->
+        f Dec4 ->
+        f Dec5 ->
+        f Dec6 ->
+        f Dec7 ->
+        f Dec8 ->
+        f Dec9 ->
+        f d
+
+data Dec0 deriving (Typeable)
+instance C    Dec0 where switch x _ _ _ _ _ _ _ _ _ = x
+instance Show Dec0 where show _ = "0"
+
+data Dec1 deriving (Typeable)
+instance Pos  Dec1 where switchPos x _ _ _ _ _ _ _ _ = x
+instance C    Dec1 where switch  _ x _ _ _ _ _ _ _ _ = x
+instance Show Dec1 where show _ = "1"
+
+data Dec2 deriving (Typeable)
+instance Pos  Dec2 where switchPos _ x _ _ _ _ _ _ _ = x
+instance C    Dec2 where switch  _ _ x _ _ _ _ _ _ _ = x
+instance Show Dec2 where show _ = "2"
+
+data Dec3 deriving (Typeable)
+instance Pos  Dec3 where switchPos _ _ x _ _ _ _ _ _ = x
+instance C    Dec3 where switch  _ _ _ x _ _ _ _ _ _ = x
+instance Show Dec3 where show _ = "3"
+
+data Dec4 deriving (Typeable)
+instance Pos  Dec4 where switchPos _ _ _ x _ _ _ _ _ = x
+instance C    Dec4 where switch  _ _ _ _ x _ _ _ _ _ = x
+instance Show Dec4 where show _ = "4"
+
+data Dec5 deriving (Typeable)
+instance Pos  Dec5 where switchPos _ _ _ _ x _ _ _ _ = x
+instance C    Dec5 where switch  _ _ _ _ _ x _ _ _ _ = x
+instance Show Dec5 where show _ = "5"
+
+data Dec6 deriving (Typeable)
+instance Pos  Dec6 where switchPos _ _ _ _ _ x _ _ _ = x
+instance C    Dec6 where switch  _ _ _ _ _ _ x _ _ _ = x
+instance Show Dec6 where show _ = "6"
+
+data Dec7 deriving (Typeable)
+instance Pos  Dec7 where switchPos _ _ _ _ _ _ x _ _ = x
+instance C    Dec7 where switch  _ _ _ _ _ _ _ x _ _ = x
+instance Show Dec7 where show _ = "7"
+
+data Dec8 deriving (Typeable)
+instance Pos  Dec8 where switchPos _ _ _ _ _ _ _ x _ = x
+instance C    Dec8 where switch  _ _ _ _ _ _ _ _ x _ = x
+instance Show Dec8 where show _ = "8"
+
+data Dec9 deriving (Typeable)
+instance Pos  Dec9 where switchPos _ _ _ _ _ _ _ _ x = x
+instance C    Dec9 where switch  _ _ _ _ _ _ _ _ _ x = x
+instance Show Dec9 where show _ = "9"
+
+
+reify :: Integer -> (forall d. C d => Proxy d -> w) -> w
+reify n f =
+   if n==0
+     then f (Proxy :: Proxy Dec0)
+     else reifyPos n f
+
+reifyPos :: Integer -> (forall d. Pos d => Proxy d -> w) -> w
+reifyPos n f =
+   case n of
+     1 -> f (Proxy :: Proxy Dec1)
+     2 -> f (Proxy :: Proxy Dec2)
+     3 -> f (Proxy :: Proxy Dec3)
+     4 -> f (Proxy :: Proxy Dec4)
+     5 -> f (Proxy :: Proxy Dec5)
+     6 -> f (Proxy :: Proxy Dec6)
+     7 -> f (Proxy :: Proxy Dec7)
+     8 -> f (Proxy :: Proxy Dec8)
+     9 -> f (Proxy :: Proxy Dec9)
+     _ -> error "digit must be a number from 0 to 9"
+
+
+type family ToUnary n
+type instance ToUnary Dec0 = UnaryLit.U0
+type instance ToUnary Dec1 = UnaryLit.U1
+type instance ToUnary Dec2 = UnaryLit.U2
+type instance ToUnary Dec3 = UnaryLit.U3
+type instance ToUnary Dec4 = UnaryLit.U4
+type instance ToUnary Dec5 = UnaryLit.U5
+type instance ToUnary Dec6 = UnaryLit.U6
+type instance ToUnary Dec7 = UnaryLit.U7
+type instance ToUnary Dec8 = UnaryLit.U8
+type instance ToUnary Dec9 = UnaryLit.U9
diff --git a/src/Type/Data/Num/Decimal/Digit/Proof.hs b/src/Type/Data/Num/Decimal/Digit/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal/Digit/Proof.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Type.Data.Num.Decimal.Digit.Proof (
+   Nat(Nat), Pos(Pos),
+   UnaryNat(UnaryNat), unaryNat, unaryNatImpl,
+   UnaryPos(UnaryPos), unaryPos, unaryPosImpl,
+   ) where
+
+import qualified Type.Data.Num.Unary as Unary
+import qualified Type.Data.Num.Unary.Proof as UnaryProof
+import qualified Type.Data.Num.Decimal.Digit as Digit
+
+
+data Nat d = (Digit.C d) => Nat
+data Pos d = (Digit.Pos d) => Pos
+
+newtype UnaryNatTheorem d =
+   UnaryNatTheorem {
+      runUnaryNatTheorem :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)
+   }
+
+unaryNatTheorem :: (Unary.Natural (Digit.ToUnary d)) => UnaryNatTheorem d
+unaryNatTheorem = UnaryNatTheorem (\Nat -> UnaryProof.Nat)
+
+unaryNatImpl :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)
+unaryNatImpl d@Nat =
+   runUnaryNatTheorem
+      (Digit.switch
+         unaryNatTheorem unaryNatTheorem unaryNatTheorem unaryNatTheorem
+         unaryNatTheorem unaryNatTheorem unaryNatTheorem unaryNatTheorem
+         unaryNatTheorem unaryNatTheorem)
+      d
+
+
+newtype UnaryPosTheorem d =
+   UnaryPosTheorem {
+      runUnaryPosTheorem :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)
+   }
+
+unaryPosTheorem :: (Unary.Positive (Digit.ToUnary d)) => UnaryPosTheorem d
+unaryPosTheorem = UnaryPosTheorem (\Pos -> UnaryProof.Pos)
+
+unaryPosImpl :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)
+unaryPosImpl d@Pos =
+   runUnaryPosTheorem
+      (Digit.switchPos
+         unaryPosTheorem unaryPosTheorem unaryPosTheorem unaryPosTheorem
+         unaryPosTheorem unaryPosTheorem unaryPosTheorem unaryPosTheorem
+         unaryPosTheorem)
+      d
+
+
+
+data UnaryNat d = Unary.Natural (Digit.ToUnary d) => UnaryNat
+
+unaryNat :: (Digit.C d) => UnaryNat d
+unaryNat =
+   Digit.switch
+      UnaryNat UnaryNat UnaryNat UnaryNat UnaryNat
+      UnaryNat UnaryNat UnaryNat UnaryNat UnaryNat
+
+
+data UnaryPos d = Unary.Positive (Digit.ToUnary d) => UnaryPos
+
+unaryPos :: (Digit.Pos d) => UnaryPos d
+unaryPos =
+   Digit.switchPos
+      UnaryPos UnaryPos UnaryPos UnaryPos
+      UnaryPos UnaryPos UnaryPos UnaryPos UnaryPos
diff --git a/src/Type/Data/Num/Decimal/Literal.hs b/src/Type/Data/Num/Decimal/Literal.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal/Literal.hs
@@ -0,0 +1,1061 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Type.Data.Num.Decimal.Literal where
+
+import Type.Data.Num.Decimal.Digit
+          (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)
+import Type.Data.Num.Decimal.Number (Zero, Pos, Neg, EndDesc, (:>))
+
+import Type.Base.Proxy (Proxy(Proxy))
+
+
+type Pos1 p0 = Pos p0 (EndDesc)
+type Pos2 p1 p0 = Pos p1 (p0 :> EndDesc)
+type Pos3 p2 p1 p0 = Pos p2 (p1 :> p0 :> EndDesc)
+type Pos4 p3 p2 p1 p0 = Pos p3 (p2 :> p1 :> p0 :> EndDesc)
+type Pos5 p4 p3 p2 p1 p0 = Pos p4 (p3 :> p2 :> p1 :> p0 :> EndDesc)
+type Pos6 p5 p4 p3 p2 p1 p0 = Pos p5 (p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)
+type Pos7 p6 p5 p4 p3 p2 p1 p0 = Pos p6 (p5 :> p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)
+
+type Neg1 p0 = Neg p0 (EndDesc)
+type Neg2 p1 p0 = Neg p1 (p0 :> EndDesc)
+type Neg3 p2 p1 p0 = Neg p2 (p1 :> p0 :> EndDesc)
+type Neg4 p3 p2 p1 p0 = Neg p3 (p2 :> p1 :> p0 :> EndDesc)
+type Neg5 p4 p3 p2 p1 p0 = Neg p4 (p3 :> p2 :> p1 :> p0 :> EndDesc)
+type Neg6 p5 p4 p3 p2 p1 p0 = Neg p5 (p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)
+type Neg7 p6 p5 p4 p3 p2 p1 p0 = Neg p6 (p5 :> p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)
+
+
+type D0 = Zero
+
+type D1 = Pos1 Dec1
+type D2 = Pos1 Dec2
+type D3 = Pos1 Dec3
+type D4 = Pos1 Dec4
+type D5 = Pos1 Dec5
+type D6 = Pos1 Dec6
+type D7 = Pos1 Dec7
+type D8 = Pos1 Dec8
+type D9 = Pos1 Dec9
+type D10 = Pos2 Dec1 Dec0
+type D11 = Pos2 Dec1 Dec1
+type D12 = Pos2 Dec1 Dec2
+type D13 = Pos2 Dec1 Dec3
+type D14 = Pos2 Dec1 Dec4
+type D15 = Pos2 Dec1 Dec5
+type D16 = Pos2 Dec1 Dec6
+type D17 = Pos2 Dec1 Dec7
+type D18 = Pos2 Dec1 Dec8
+type D19 = Pos2 Dec1 Dec9
+type D20 = Pos2 Dec2 Dec0
+type D21 = Pos2 Dec2 Dec1
+type D22 = Pos2 Dec2 Dec2
+type D23 = Pos2 Dec2 Dec3
+type D24 = Pos2 Dec2 Dec4
+type D25 = Pos2 Dec2 Dec5
+type D26 = Pos2 Dec2 Dec6
+type D27 = Pos2 Dec2 Dec7
+type D28 = Pos2 Dec2 Dec8
+type D29 = Pos2 Dec2 Dec9
+type D30 = Pos2 Dec3 Dec0
+type D31 = Pos2 Dec3 Dec1
+type D32 = Pos2 Dec3 Dec2
+type D33 = Pos2 Dec3 Dec3
+type D34 = Pos2 Dec3 Dec4
+type D35 = Pos2 Dec3 Dec5
+type D36 = Pos2 Dec3 Dec6
+type D37 = Pos2 Dec3 Dec7
+type D38 = Pos2 Dec3 Dec8
+type D39 = Pos2 Dec3 Dec9
+type D40 = Pos2 Dec4 Dec0
+type D41 = Pos2 Dec4 Dec1
+type D42 = Pos2 Dec4 Dec2
+type D43 = Pos2 Dec4 Dec3
+type D44 = Pos2 Dec4 Dec4
+type D45 = Pos2 Dec4 Dec5
+type D46 = Pos2 Dec4 Dec6
+type D47 = Pos2 Dec4 Dec7
+type D48 = Pos2 Dec4 Dec8
+type D49 = Pos2 Dec4 Dec9
+type D50 = Pos2 Dec5 Dec0
+type D51 = Pos2 Dec5 Dec1
+type D52 = Pos2 Dec5 Dec2
+type D53 = Pos2 Dec5 Dec3
+type D54 = Pos2 Dec5 Dec4
+type D55 = Pos2 Dec5 Dec5
+type D56 = Pos2 Dec5 Dec6
+type D57 = Pos2 Dec5 Dec7
+type D58 = Pos2 Dec5 Dec8
+type D59 = Pos2 Dec5 Dec9
+type D60 = Pos2 Dec6 Dec0
+type D61 = Pos2 Dec6 Dec1
+type D62 = Pos2 Dec6 Dec2
+type D63 = Pos2 Dec6 Dec3
+type D64 = Pos2 Dec6 Dec4
+type D65 = Pos2 Dec6 Dec5
+type D66 = Pos2 Dec6 Dec6
+type D67 = Pos2 Dec6 Dec7
+type D68 = Pos2 Dec6 Dec8
+type D69 = Pos2 Dec6 Dec9
+type D70 = Pos2 Dec7 Dec0
+type D71 = Pos2 Dec7 Dec1
+type D72 = Pos2 Dec7 Dec2
+type D73 = Pos2 Dec7 Dec3
+type D74 = Pos2 Dec7 Dec4
+type D75 = Pos2 Dec7 Dec5
+type D76 = Pos2 Dec7 Dec6
+type D77 = Pos2 Dec7 Dec7
+type D78 = Pos2 Dec7 Dec8
+type D79 = Pos2 Dec7 Dec9
+type D80 = Pos2 Dec8 Dec0
+type D81 = Pos2 Dec8 Dec1
+type D82 = Pos2 Dec8 Dec2
+type D83 = Pos2 Dec8 Dec3
+type D84 = Pos2 Dec8 Dec4
+type D85 = Pos2 Dec8 Dec5
+type D86 = Pos2 Dec8 Dec6
+type D87 = Pos2 Dec8 Dec7
+type D88 = Pos2 Dec8 Dec8
+type D89 = Pos2 Dec8 Dec9
+type D90 = Pos2 Dec9 Dec0
+type D91 = Pos2 Dec9 Dec1
+type D92 = Pos2 Dec9 Dec2
+type D93 = Pos2 Dec9 Dec3
+type D94 = Pos2 Dec9 Dec4
+type D95 = Pos2 Dec9 Dec5
+type D96 = Pos2 Dec9 Dec6
+type D97 = Pos2 Dec9 Dec7
+type D98 = Pos2 Dec9 Dec8
+type D99 = Pos2 Dec9 Dec9
+type D100 = Pos3 Dec1 Dec0 Dec0
+type D101 = Pos3 Dec1 Dec0 Dec1
+type D102 = Pos3 Dec1 Dec0 Dec2
+type D103 = Pos3 Dec1 Dec0 Dec3
+type D104 = Pos3 Dec1 Dec0 Dec4
+type D105 = Pos3 Dec1 Dec0 Dec5
+type D106 = Pos3 Dec1 Dec0 Dec6
+type D107 = Pos3 Dec1 Dec0 Dec7
+type D108 = Pos3 Dec1 Dec0 Dec8
+type D109 = Pos3 Dec1 Dec0 Dec9
+type D110 = Pos3 Dec1 Dec1 Dec0
+type D111 = Pos3 Dec1 Dec1 Dec1
+type D112 = Pos3 Dec1 Dec1 Dec2
+type D113 = Pos3 Dec1 Dec1 Dec3
+type D114 = Pos3 Dec1 Dec1 Dec4
+type D115 = Pos3 Dec1 Dec1 Dec5
+type D116 = Pos3 Dec1 Dec1 Dec6
+type D117 = Pos3 Dec1 Dec1 Dec7
+type D118 = Pos3 Dec1 Dec1 Dec8
+type D119 = Pos3 Dec1 Dec1 Dec9
+type D120 = Pos3 Dec1 Dec2 Dec0
+type D121 = Pos3 Dec1 Dec2 Dec1
+type D122 = Pos3 Dec1 Dec2 Dec2
+type D123 = Pos3 Dec1 Dec2 Dec3
+type D124 = Pos3 Dec1 Dec2 Dec4
+type D125 = Pos3 Dec1 Dec2 Dec5
+type D126 = Pos3 Dec1 Dec2 Dec6
+type D127 = Pos3 Dec1 Dec2 Dec7
+type D128 = Pos3 Dec1 Dec2 Dec8
+type D129 = Pos3 Dec1 Dec2 Dec9
+type D130 = Pos3 Dec1 Dec3 Dec0
+type D131 = Pos3 Dec1 Dec3 Dec1
+type D132 = Pos3 Dec1 Dec3 Dec2
+type D133 = Pos3 Dec1 Dec3 Dec3
+type D134 = Pos3 Dec1 Dec3 Dec4
+type D135 = Pos3 Dec1 Dec3 Dec5
+type D136 = Pos3 Dec1 Dec3 Dec6
+type D137 = Pos3 Dec1 Dec3 Dec7
+type D138 = Pos3 Dec1 Dec3 Dec8
+type D139 = Pos3 Dec1 Dec3 Dec9
+type D140 = Pos3 Dec1 Dec4 Dec0
+type D141 = Pos3 Dec1 Dec4 Dec1
+type D142 = Pos3 Dec1 Dec4 Dec2
+type D143 = Pos3 Dec1 Dec4 Dec3
+type D144 = Pos3 Dec1 Dec4 Dec4
+type D145 = Pos3 Dec1 Dec4 Dec5
+type D146 = Pos3 Dec1 Dec4 Dec6
+type D147 = Pos3 Dec1 Dec4 Dec7
+type D148 = Pos3 Dec1 Dec4 Dec8
+type D149 = Pos3 Dec1 Dec4 Dec9
+type D150 = Pos3 Dec1 Dec5 Dec0
+type D151 = Pos3 Dec1 Dec5 Dec1
+type D152 = Pos3 Dec1 Dec5 Dec2
+type D153 = Pos3 Dec1 Dec5 Dec3
+type D154 = Pos3 Dec1 Dec5 Dec4
+type D155 = Pos3 Dec1 Dec5 Dec5
+type D156 = Pos3 Dec1 Dec5 Dec6
+type D157 = Pos3 Dec1 Dec5 Dec7
+type D158 = Pos3 Dec1 Dec5 Dec8
+type D159 = Pos3 Dec1 Dec5 Dec9
+type D160 = Pos3 Dec1 Dec6 Dec0
+type D161 = Pos3 Dec1 Dec6 Dec1
+type D162 = Pos3 Dec1 Dec6 Dec2
+type D163 = Pos3 Dec1 Dec6 Dec3
+type D164 = Pos3 Dec1 Dec6 Dec4
+type D165 = Pos3 Dec1 Dec6 Dec5
+type D166 = Pos3 Dec1 Dec6 Dec6
+type D167 = Pos3 Dec1 Dec6 Dec7
+type D168 = Pos3 Dec1 Dec6 Dec8
+type D169 = Pos3 Dec1 Dec6 Dec9
+type D170 = Pos3 Dec1 Dec7 Dec0
+type D171 = Pos3 Dec1 Dec7 Dec1
+type D172 = Pos3 Dec1 Dec7 Dec2
+type D173 = Pos3 Dec1 Dec7 Dec3
+type D174 = Pos3 Dec1 Dec7 Dec4
+type D175 = Pos3 Dec1 Dec7 Dec5
+type D176 = Pos3 Dec1 Dec7 Dec6
+type D177 = Pos3 Dec1 Dec7 Dec7
+type D178 = Pos3 Dec1 Dec7 Dec8
+type D179 = Pos3 Dec1 Dec7 Dec9
+type D180 = Pos3 Dec1 Dec8 Dec0
+type D181 = Pos3 Dec1 Dec8 Dec1
+type D182 = Pos3 Dec1 Dec8 Dec2
+type D183 = Pos3 Dec1 Dec8 Dec3
+type D184 = Pos3 Dec1 Dec8 Dec4
+type D185 = Pos3 Dec1 Dec8 Dec5
+type D186 = Pos3 Dec1 Dec8 Dec6
+type D187 = Pos3 Dec1 Dec8 Dec7
+type D188 = Pos3 Dec1 Dec8 Dec8
+type D189 = Pos3 Dec1 Dec8 Dec9
+type D190 = Pos3 Dec1 Dec9 Dec0
+type D191 = Pos3 Dec1 Dec9 Dec1
+type D192 = Pos3 Dec1 Dec9 Dec2
+type D193 = Pos3 Dec1 Dec9 Dec3
+type D194 = Pos3 Dec1 Dec9 Dec4
+type D195 = Pos3 Dec1 Dec9 Dec5
+type D196 = Pos3 Dec1 Dec9 Dec6
+type D197 = Pos3 Dec1 Dec9 Dec7
+type D198 = Pos3 Dec1 Dec9 Dec8
+type D199 = Pos3 Dec1 Dec9 Dec9
+type D200 = Pos3 Dec2 Dec0 Dec0
+type D201 = Pos3 Dec2 Dec0 Dec1
+type D202 = Pos3 Dec2 Dec0 Dec2
+type D203 = Pos3 Dec2 Dec0 Dec3
+type D204 = Pos3 Dec2 Dec0 Dec4
+type D205 = Pos3 Dec2 Dec0 Dec5
+type D206 = Pos3 Dec2 Dec0 Dec6
+type D207 = Pos3 Dec2 Dec0 Dec7
+type D208 = Pos3 Dec2 Dec0 Dec8
+type D209 = Pos3 Dec2 Dec0 Dec9
+type D210 = Pos3 Dec2 Dec1 Dec0
+type D211 = Pos3 Dec2 Dec1 Dec1
+type D212 = Pos3 Dec2 Dec1 Dec2
+type D213 = Pos3 Dec2 Dec1 Dec3
+type D214 = Pos3 Dec2 Dec1 Dec4
+type D215 = Pos3 Dec2 Dec1 Dec5
+type D216 = Pos3 Dec2 Dec1 Dec6
+type D217 = Pos3 Dec2 Dec1 Dec7
+type D218 = Pos3 Dec2 Dec1 Dec8
+type D219 = Pos3 Dec2 Dec1 Dec9
+type D220 = Pos3 Dec2 Dec2 Dec0
+type D221 = Pos3 Dec2 Dec2 Dec1
+type D222 = Pos3 Dec2 Dec2 Dec2
+type D223 = Pos3 Dec2 Dec2 Dec3
+type D224 = Pos3 Dec2 Dec2 Dec4
+type D225 = Pos3 Dec2 Dec2 Dec5
+type D226 = Pos3 Dec2 Dec2 Dec6
+type D227 = Pos3 Dec2 Dec2 Dec7
+type D228 = Pos3 Dec2 Dec2 Dec8
+type D229 = Pos3 Dec2 Dec2 Dec9
+type D230 = Pos3 Dec2 Dec3 Dec0
+type D231 = Pos3 Dec2 Dec3 Dec1
+type D232 = Pos3 Dec2 Dec3 Dec2
+type D233 = Pos3 Dec2 Dec3 Dec3
+type D234 = Pos3 Dec2 Dec3 Dec4
+type D235 = Pos3 Dec2 Dec3 Dec5
+type D236 = Pos3 Dec2 Dec3 Dec6
+type D237 = Pos3 Dec2 Dec3 Dec7
+type D238 = Pos3 Dec2 Dec3 Dec8
+type D239 = Pos3 Dec2 Dec3 Dec9
+type D240 = Pos3 Dec2 Dec4 Dec0
+type D241 = Pos3 Dec2 Dec4 Dec1
+type D242 = Pos3 Dec2 Dec4 Dec2
+type D243 = Pos3 Dec2 Dec4 Dec3
+type D244 = Pos3 Dec2 Dec4 Dec4
+type D245 = Pos3 Dec2 Dec4 Dec5
+type D246 = Pos3 Dec2 Dec4 Dec6
+type D247 = Pos3 Dec2 Dec4 Dec7
+type D248 = Pos3 Dec2 Dec4 Dec8
+type D249 = Pos3 Dec2 Dec4 Dec9
+type D250 = Pos3 Dec2 Dec5 Dec0
+type D251 = Pos3 Dec2 Dec5 Dec1
+type D252 = Pos3 Dec2 Dec5 Dec2
+type D253 = Pos3 Dec2 Dec5 Dec3
+type D254 = Pos3 Dec2 Dec5 Dec4
+type D255 = Pos3 Dec2 Dec5 Dec5
+type D256 = Pos3 Dec2 Dec5 Dec6
+
+type DN1 = Neg1 Dec1
+type DN2 = Neg1 Dec2
+type DN3 = Neg1 Dec3
+type DN4 = Neg1 Dec4
+type DN5 = Neg1 Dec5
+type DN6 = Neg1 Dec6
+type DN7 = Neg1 Dec7
+type DN8 = Neg1 Dec8
+type DN9 = Neg1 Dec9
+type DN10 = Neg2 Dec1 Dec0
+type DN11 = Neg2 Dec1 Dec1
+type DN12 = Neg2 Dec1 Dec2
+type DN13 = Neg2 Dec1 Dec3
+type DN14 = Neg2 Dec1 Dec4
+type DN15 = Neg2 Dec1 Dec5
+type DN16 = Neg2 Dec1 Dec6
+type DN17 = Neg2 Dec1 Dec7
+type DN18 = Neg2 Dec1 Dec8
+type DN19 = Neg2 Dec1 Dec9
+type DN20 = Neg2 Dec2 Dec0
+type DN21 = Neg2 Dec2 Dec1
+type DN22 = Neg2 Dec2 Dec2
+type DN23 = Neg2 Dec2 Dec3
+type DN24 = Neg2 Dec2 Dec4
+type DN25 = Neg2 Dec2 Dec5
+type DN26 = Neg2 Dec2 Dec6
+type DN27 = Neg2 Dec2 Dec7
+type DN28 = Neg2 Dec2 Dec8
+type DN29 = Neg2 Dec2 Dec9
+type DN30 = Neg2 Dec3 Dec0
+type DN31 = Neg2 Dec3 Dec1
+type DN32 = Neg2 Dec3 Dec2
+type DN33 = Neg2 Dec3 Dec3
+type DN34 = Neg2 Dec3 Dec4
+type DN35 = Neg2 Dec3 Dec5
+type DN36 = Neg2 Dec3 Dec6
+type DN37 = Neg2 Dec3 Dec7
+type DN38 = Neg2 Dec3 Dec8
+type DN39 = Neg2 Dec3 Dec9
+type DN40 = Neg2 Dec4 Dec0
+type DN41 = Neg2 Dec4 Dec1
+type DN42 = Neg2 Dec4 Dec2
+type DN43 = Neg2 Dec4 Dec3
+type DN44 = Neg2 Dec4 Dec4
+type DN45 = Neg2 Dec4 Dec5
+type DN46 = Neg2 Dec4 Dec6
+type DN47 = Neg2 Dec4 Dec7
+type DN48 = Neg2 Dec4 Dec8
+type DN49 = Neg2 Dec4 Dec9
+type DN50 = Neg2 Dec5 Dec0
+type DN51 = Neg2 Dec5 Dec1
+type DN52 = Neg2 Dec5 Dec2
+type DN53 = Neg2 Dec5 Dec3
+type DN54 = Neg2 Dec5 Dec4
+type DN55 = Neg2 Dec5 Dec5
+type DN56 = Neg2 Dec5 Dec6
+type DN57 = Neg2 Dec5 Dec7
+type DN58 = Neg2 Dec5 Dec8
+type DN59 = Neg2 Dec5 Dec9
+type DN60 = Neg2 Dec6 Dec0
+type DN61 = Neg2 Dec6 Dec1
+type DN62 = Neg2 Dec6 Dec2
+type DN63 = Neg2 Dec6 Dec3
+type DN64 = Neg2 Dec6 Dec4
+type DN65 = Neg2 Dec6 Dec5
+type DN66 = Neg2 Dec6 Dec6
+type DN67 = Neg2 Dec6 Dec7
+type DN68 = Neg2 Dec6 Dec8
+type DN69 = Neg2 Dec6 Dec9
+type DN70 = Neg2 Dec7 Dec0
+type DN71 = Neg2 Dec7 Dec1
+type DN72 = Neg2 Dec7 Dec2
+type DN73 = Neg2 Dec7 Dec3
+type DN74 = Neg2 Dec7 Dec4
+type DN75 = Neg2 Dec7 Dec5
+type DN76 = Neg2 Dec7 Dec6
+type DN77 = Neg2 Dec7 Dec7
+type DN78 = Neg2 Dec7 Dec8
+type DN79 = Neg2 Dec7 Dec9
+type DN80 = Neg2 Dec8 Dec0
+type DN81 = Neg2 Dec8 Dec1
+type DN82 = Neg2 Dec8 Dec2
+type DN83 = Neg2 Dec8 Dec3
+type DN84 = Neg2 Dec8 Dec4
+type DN85 = Neg2 Dec8 Dec5
+type DN86 = Neg2 Dec8 Dec6
+type DN87 = Neg2 Dec8 Dec7
+type DN88 = Neg2 Dec8 Dec8
+type DN89 = Neg2 Dec8 Dec9
+type DN90 = Neg2 Dec9 Dec0
+type DN91 = Neg2 Dec9 Dec1
+type DN92 = Neg2 Dec9 Dec2
+type DN93 = Neg2 Dec9 Dec3
+type DN94 = Neg2 Dec9 Dec4
+type DN95 = Neg2 Dec9 Dec5
+type DN96 = Neg2 Dec9 Dec6
+type DN97 = Neg2 Dec9 Dec7
+type DN98 = Neg2 Dec9 Dec8
+type DN99 = Neg2 Dec9 Dec9
+type DN100 = Neg3 Dec1 Dec0 Dec0
+type DN101 = Neg3 Dec1 Dec0 Dec1
+type DN102 = Neg3 Dec1 Dec0 Dec2
+type DN103 = Neg3 Dec1 Dec0 Dec3
+type DN104 = Neg3 Dec1 Dec0 Dec4
+type DN105 = Neg3 Dec1 Dec0 Dec5
+type DN106 = Neg3 Dec1 Dec0 Dec6
+type DN107 = Neg3 Dec1 Dec0 Dec7
+type DN108 = Neg3 Dec1 Dec0 Dec8
+type DN109 = Neg3 Dec1 Dec0 Dec9
+type DN110 = Neg3 Dec1 Dec1 Dec0
+type DN111 = Neg3 Dec1 Dec1 Dec1
+type DN112 = Neg3 Dec1 Dec1 Dec2
+type DN113 = Neg3 Dec1 Dec1 Dec3
+type DN114 = Neg3 Dec1 Dec1 Dec4
+type DN115 = Neg3 Dec1 Dec1 Dec5
+type DN116 = Neg3 Dec1 Dec1 Dec6
+type DN117 = Neg3 Dec1 Dec1 Dec7
+type DN118 = Neg3 Dec1 Dec1 Dec8
+type DN119 = Neg3 Dec1 Dec1 Dec9
+type DN120 = Neg3 Dec1 Dec2 Dec0
+type DN121 = Neg3 Dec1 Dec2 Dec1
+type DN122 = Neg3 Dec1 Dec2 Dec2
+type DN123 = Neg3 Dec1 Dec2 Dec3
+type DN124 = Neg3 Dec1 Dec2 Dec4
+type DN125 = Neg3 Dec1 Dec2 Dec5
+type DN126 = Neg3 Dec1 Dec2 Dec6
+type DN127 = Neg3 Dec1 Dec2 Dec7
+type DN128 = Neg3 Dec1 Dec2 Dec8
+type DN129 = Neg3 Dec1 Dec2 Dec9
+type DN130 = Neg3 Dec1 Dec3 Dec0
+type DN131 = Neg3 Dec1 Dec3 Dec1
+type DN132 = Neg3 Dec1 Dec3 Dec2
+type DN133 = Neg3 Dec1 Dec3 Dec3
+type DN134 = Neg3 Dec1 Dec3 Dec4
+type DN135 = Neg3 Dec1 Dec3 Dec5
+type DN136 = Neg3 Dec1 Dec3 Dec6
+type DN137 = Neg3 Dec1 Dec3 Dec7
+type DN138 = Neg3 Dec1 Dec3 Dec8
+type DN139 = Neg3 Dec1 Dec3 Dec9
+type DN140 = Neg3 Dec1 Dec4 Dec0
+type DN141 = Neg3 Dec1 Dec4 Dec1
+type DN142 = Neg3 Dec1 Dec4 Dec2
+type DN143 = Neg3 Dec1 Dec4 Dec3
+type DN144 = Neg3 Dec1 Dec4 Dec4
+type DN145 = Neg3 Dec1 Dec4 Dec5
+type DN146 = Neg3 Dec1 Dec4 Dec6
+type DN147 = Neg3 Dec1 Dec4 Dec7
+type DN148 = Neg3 Dec1 Dec4 Dec8
+type DN149 = Neg3 Dec1 Dec4 Dec9
+type DN150 = Neg3 Dec1 Dec5 Dec0
+type DN151 = Neg3 Dec1 Dec5 Dec1
+type DN152 = Neg3 Dec1 Dec5 Dec2
+type DN153 = Neg3 Dec1 Dec5 Dec3
+type DN154 = Neg3 Dec1 Dec5 Dec4
+type DN155 = Neg3 Dec1 Dec5 Dec5
+type DN156 = Neg3 Dec1 Dec5 Dec6
+type DN157 = Neg3 Dec1 Dec5 Dec7
+type DN158 = Neg3 Dec1 Dec5 Dec8
+type DN159 = Neg3 Dec1 Dec5 Dec9
+type DN160 = Neg3 Dec1 Dec6 Dec0
+type DN161 = Neg3 Dec1 Dec6 Dec1
+type DN162 = Neg3 Dec1 Dec6 Dec2
+type DN163 = Neg3 Dec1 Dec6 Dec3
+type DN164 = Neg3 Dec1 Dec6 Dec4
+type DN165 = Neg3 Dec1 Dec6 Dec5
+type DN166 = Neg3 Dec1 Dec6 Dec6
+type DN167 = Neg3 Dec1 Dec6 Dec7
+type DN168 = Neg3 Dec1 Dec6 Dec8
+type DN169 = Neg3 Dec1 Dec6 Dec9
+type DN170 = Neg3 Dec1 Dec7 Dec0
+type DN171 = Neg3 Dec1 Dec7 Dec1
+type DN172 = Neg3 Dec1 Dec7 Dec2
+type DN173 = Neg3 Dec1 Dec7 Dec3
+type DN174 = Neg3 Dec1 Dec7 Dec4
+type DN175 = Neg3 Dec1 Dec7 Dec5
+type DN176 = Neg3 Dec1 Dec7 Dec6
+type DN177 = Neg3 Dec1 Dec7 Dec7
+type DN178 = Neg3 Dec1 Dec7 Dec8
+type DN179 = Neg3 Dec1 Dec7 Dec9
+type DN180 = Neg3 Dec1 Dec8 Dec0
+type DN181 = Neg3 Dec1 Dec8 Dec1
+type DN182 = Neg3 Dec1 Dec8 Dec2
+type DN183 = Neg3 Dec1 Dec8 Dec3
+type DN184 = Neg3 Dec1 Dec8 Dec4
+type DN185 = Neg3 Dec1 Dec8 Dec5
+type DN186 = Neg3 Dec1 Dec8 Dec6
+type DN187 = Neg3 Dec1 Dec8 Dec7
+type DN188 = Neg3 Dec1 Dec8 Dec8
+type DN189 = Neg3 Dec1 Dec8 Dec9
+type DN190 = Neg3 Dec1 Dec9 Dec0
+type DN191 = Neg3 Dec1 Dec9 Dec1
+type DN192 = Neg3 Dec1 Dec9 Dec2
+type DN193 = Neg3 Dec1 Dec9 Dec3
+type DN194 = Neg3 Dec1 Dec9 Dec4
+type DN195 = Neg3 Dec1 Dec9 Dec5
+type DN196 = Neg3 Dec1 Dec9 Dec6
+type DN197 = Neg3 Dec1 Dec9 Dec7
+type DN198 = Neg3 Dec1 Dec9 Dec8
+type DN199 = Neg3 Dec1 Dec9 Dec9
+type DN200 = Neg3 Dec2 Dec0 Dec0
+type DN201 = Neg3 Dec2 Dec0 Dec1
+type DN202 = Neg3 Dec2 Dec0 Dec2
+type DN203 = Neg3 Dec2 Dec0 Dec3
+type DN204 = Neg3 Dec2 Dec0 Dec4
+type DN205 = Neg3 Dec2 Dec0 Dec5
+type DN206 = Neg3 Dec2 Dec0 Dec6
+type DN207 = Neg3 Dec2 Dec0 Dec7
+type DN208 = Neg3 Dec2 Dec0 Dec8
+type DN209 = Neg3 Dec2 Dec0 Dec9
+type DN210 = Neg3 Dec2 Dec1 Dec0
+type DN211 = Neg3 Dec2 Dec1 Dec1
+type DN212 = Neg3 Dec2 Dec1 Dec2
+type DN213 = Neg3 Dec2 Dec1 Dec3
+type DN214 = Neg3 Dec2 Dec1 Dec4
+type DN215 = Neg3 Dec2 Dec1 Dec5
+type DN216 = Neg3 Dec2 Dec1 Dec6
+type DN217 = Neg3 Dec2 Dec1 Dec7
+type DN218 = Neg3 Dec2 Dec1 Dec8
+type DN219 = Neg3 Dec2 Dec1 Dec9
+type DN220 = Neg3 Dec2 Dec2 Dec0
+type DN221 = Neg3 Dec2 Dec2 Dec1
+type DN222 = Neg3 Dec2 Dec2 Dec2
+type DN223 = Neg3 Dec2 Dec2 Dec3
+type DN224 = Neg3 Dec2 Dec2 Dec4
+type DN225 = Neg3 Dec2 Dec2 Dec5
+type DN226 = Neg3 Dec2 Dec2 Dec6
+type DN227 = Neg3 Dec2 Dec2 Dec7
+type DN228 = Neg3 Dec2 Dec2 Dec8
+type DN229 = Neg3 Dec2 Dec2 Dec9
+type DN230 = Neg3 Dec2 Dec3 Dec0
+type DN231 = Neg3 Dec2 Dec3 Dec1
+type DN232 = Neg3 Dec2 Dec3 Dec2
+type DN233 = Neg3 Dec2 Dec3 Dec3
+type DN234 = Neg3 Dec2 Dec3 Dec4
+type DN235 = Neg3 Dec2 Dec3 Dec5
+type DN236 = Neg3 Dec2 Dec3 Dec6
+type DN237 = Neg3 Dec2 Dec3 Dec7
+type DN238 = Neg3 Dec2 Dec3 Dec8
+type DN239 = Neg3 Dec2 Dec3 Dec9
+type DN240 = Neg3 Dec2 Dec4 Dec0
+type DN241 = Neg3 Dec2 Dec4 Dec1
+type DN242 = Neg3 Dec2 Dec4 Dec2
+type DN243 = Neg3 Dec2 Dec4 Dec3
+type DN244 = Neg3 Dec2 Dec4 Dec4
+type DN245 = Neg3 Dec2 Dec4 Dec5
+type DN246 = Neg3 Dec2 Dec4 Dec6
+type DN247 = Neg3 Dec2 Dec4 Dec7
+type DN248 = Neg3 Dec2 Dec4 Dec8
+type DN249 = Neg3 Dec2 Dec4 Dec9
+type DN250 = Neg3 Dec2 Dec5 Dec0
+type DN251 = Neg3 Dec2 Dec5 Dec1
+type DN252 = Neg3 Dec2 Dec5 Dec2
+type DN253 = Neg3 Dec2 Dec5 Dec3
+type DN254 = Neg3 Dec2 Dec5 Dec4
+type DN255 = Neg3 Dec2 Dec5 Dec5
+type DN256 = Neg3 Dec2 Dec5 Dec6
+
+
+d0 :: Proxy D0; d0 = Proxy
+
+d1 :: Proxy D1; d1 = Proxy
+d2 :: Proxy D2; d2 = Proxy
+d3 :: Proxy D3; d3 = Proxy
+d4 :: Proxy D4; d4 = Proxy
+d5 :: Proxy D5; d5 = Proxy
+d6 :: Proxy D6; d6 = Proxy
+d7 :: Proxy D7; d7 = Proxy
+d8 :: Proxy D8; d8 = Proxy
+d9 :: Proxy D9; d9 = Proxy
+d10 :: Proxy D10; d10 = Proxy
+d11 :: Proxy D11; d11 = Proxy
+d12 :: Proxy D12; d12 = Proxy
+d13 :: Proxy D13; d13 = Proxy
+d14 :: Proxy D14; d14 = Proxy
+d15 :: Proxy D15; d15 = Proxy
+d16 :: Proxy D16; d16 = Proxy
+d17 :: Proxy D17; d17 = Proxy
+d18 :: Proxy D18; d18 = Proxy
+d19 :: Proxy D19; d19 = Proxy
+d20 :: Proxy D20; d20 = Proxy
+d21 :: Proxy D21; d21 = Proxy
+d22 :: Proxy D22; d22 = Proxy
+d23 :: Proxy D23; d23 = Proxy
+d24 :: Proxy D24; d24 = Proxy
+d25 :: Proxy D25; d25 = Proxy
+d26 :: Proxy D26; d26 = Proxy
+d27 :: Proxy D27; d27 = Proxy
+d28 :: Proxy D28; d28 = Proxy
+d29 :: Proxy D29; d29 = Proxy
+d30 :: Proxy D30; d30 = Proxy
+d31 :: Proxy D31; d31 = Proxy
+d32 :: Proxy D32; d32 = Proxy
+d33 :: Proxy D33; d33 = Proxy
+d34 :: Proxy D34; d34 = Proxy
+d35 :: Proxy D35; d35 = Proxy
+d36 :: Proxy D36; d36 = Proxy
+d37 :: Proxy D37; d37 = Proxy
+d38 :: Proxy D38; d38 = Proxy
+d39 :: Proxy D39; d39 = Proxy
+d40 :: Proxy D40; d40 = Proxy
+d41 :: Proxy D41; d41 = Proxy
+d42 :: Proxy D42; d42 = Proxy
+d43 :: Proxy D43; d43 = Proxy
+d44 :: Proxy D44; d44 = Proxy
+d45 :: Proxy D45; d45 = Proxy
+d46 :: Proxy D46; d46 = Proxy
+d47 :: Proxy D47; d47 = Proxy
+d48 :: Proxy D48; d48 = Proxy
+d49 :: Proxy D49; d49 = Proxy
+d50 :: Proxy D50; d50 = Proxy
+d51 :: Proxy D51; d51 = Proxy
+d52 :: Proxy D52; d52 = Proxy
+d53 :: Proxy D53; d53 = Proxy
+d54 :: Proxy D54; d54 = Proxy
+d55 :: Proxy D55; d55 = Proxy
+d56 :: Proxy D56; d56 = Proxy
+d57 :: Proxy D57; d57 = Proxy
+d58 :: Proxy D58; d58 = Proxy
+d59 :: Proxy D59; d59 = Proxy
+d60 :: Proxy D60; d60 = Proxy
+d61 :: Proxy D61; d61 = Proxy
+d62 :: Proxy D62; d62 = Proxy
+d63 :: Proxy D63; d63 = Proxy
+d64 :: Proxy D64; d64 = Proxy
+d65 :: Proxy D65; d65 = Proxy
+d66 :: Proxy D66; d66 = Proxy
+d67 :: Proxy D67; d67 = Proxy
+d68 :: Proxy D68; d68 = Proxy
+d69 :: Proxy D69; d69 = Proxy
+d70 :: Proxy D70; d70 = Proxy
+d71 :: Proxy D71; d71 = Proxy
+d72 :: Proxy D72; d72 = Proxy
+d73 :: Proxy D73; d73 = Proxy
+d74 :: Proxy D74; d74 = Proxy
+d75 :: Proxy D75; d75 = Proxy
+d76 :: Proxy D76; d76 = Proxy
+d77 :: Proxy D77; d77 = Proxy
+d78 :: Proxy D78; d78 = Proxy
+d79 :: Proxy D79; d79 = Proxy
+d80 :: Proxy D80; d80 = Proxy
+d81 :: Proxy D81; d81 = Proxy
+d82 :: Proxy D82; d82 = Proxy
+d83 :: Proxy D83; d83 = Proxy
+d84 :: Proxy D84; d84 = Proxy
+d85 :: Proxy D85; d85 = Proxy
+d86 :: Proxy D86; d86 = Proxy
+d87 :: Proxy D87; d87 = Proxy
+d88 :: Proxy D88; d88 = Proxy
+d89 :: Proxy D89; d89 = Proxy
+d90 :: Proxy D90; d90 = Proxy
+d91 :: Proxy D91; d91 = Proxy
+d92 :: Proxy D92; d92 = Proxy
+d93 :: Proxy D93; d93 = Proxy
+d94 :: Proxy D94; d94 = Proxy
+d95 :: Proxy D95; d95 = Proxy
+d96 :: Proxy D96; d96 = Proxy
+d97 :: Proxy D97; d97 = Proxy
+d98 :: Proxy D98; d98 = Proxy
+d99 :: Proxy D99; d99 = Proxy
+d100 :: Proxy D100; d100 = Proxy
+d101 :: Proxy D101; d101 = Proxy
+d102 :: Proxy D102; d102 = Proxy
+d103 :: Proxy D103; d103 = Proxy
+d104 :: Proxy D104; d104 = Proxy
+d105 :: Proxy D105; d105 = Proxy
+d106 :: Proxy D106; d106 = Proxy
+d107 :: Proxy D107; d107 = Proxy
+d108 :: Proxy D108; d108 = Proxy
+d109 :: Proxy D109; d109 = Proxy
+d110 :: Proxy D110; d110 = Proxy
+d111 :: Proxy D111; d111 = Proxy
+d112 :: Proxy D112; d112 = Proxy
+d113 :: Proxy D113; d113 = Proxy
+d114 :: Proxy D114; d114 = Proxy
+d115 :: Proxy D115; d115 = Proxy
+d116 :: Proxy D116; d116 = Proxy
+d117 :: Proxy D117; d117 = Proxy
+d118 :: Proxy D118; d118 = Proxy
+d119 :: Proxy D119; d119 = Proxy
+d120 :: Proxy D120; d120 = Proxy
+d121 :: Proxy D121; d121 = Proxy
+d122 :: Proxy D122; d122 = Proxy
+d123 :: Proxy D123; d123 = Proxy
+d124 :: Proxy D124; d124 = Proxy
+d125 :: Proxy D125; d125 = Proxy
+d126 :: Proxy D126; d126 = Proxy
+d127 :: Proxy D127; d127 = Proxy
+d128 :: Proxy D128; d128 = Proxy
+d129 :: Proxy D129; d129 = Proxy
+d130 :: Proxy D130; d130 = Proxy
+d131 :: Proxy D131; d131 = Proxy
+d132 :: Proxy D132; d132 = Proxy
+d133 :: Proxy D133; d133 = Proxy
+d134 :: Proxy D134; d134 = Proxy
+d135 :: Proxy D135; d135 = Proxy
+d136 :: Proxy D136; d136 = Proxy
+d137 :: Proxy D137; d137 = Proxy
+d138 :: Proxy D138; d138 = Proxy
+d139 :: Proxy D139; d139 = Proxy
+d140 :: Proxy D140; d140 = Proxy
+d141 :: Proxy D141; d141 = Proxy
+d142 :: Proxy D142; d142 = Proxy
+d143 :: Proxy D143; d143 = Proxy
+d144 :: Proxy D144; d144 = Proxy
+d145 :: Proxy D145; d145 = Proxy
+d146 :: Proxy D146; d146 = Proxy
+d147 :: Proxy D147; d147 = Proxy
+d148 :: Proxy D148; d148 = Proxy
+d149 :: Proxy D149; d149 = Proxy
+d150 :: Proxy D150; d150 = Proxy
+d151 :: Proxy D151; d151 = Proxy
+d152 :: Proxy D152; d152 = Proxy
+d153 :: Proxy D153; d153 = Proxy
+d154 :: Proxy D154; d154 = Proxy
+d155 :: Proxy D155; d155 = Proxy
+d156 :: Proxy D156; d156 = Proxy
+d157 :: Proxy D157; d157 = Proxy
+d158 :: Proxy D158; d158 = Proxy
+d159 :: Proxy D159; d159 = Proxy
+d160 :: Proxy D160; d160 = Proxy
+d161 :: Proxy D161; d161 = Proxy
+d162 :: Proxy D162; d162 = Proxy
+d163 :: Proxy D163; d163 = Proxy
+d164 :: Proxy D164; d164 = Proxy
+d165 :: Proxy D165; d165 = Proxy
+d166 :: Proxy D166; d166 = Proxy
+d167 :: Proxy D167; d167 = Proxy
+d168 :: Proxy D168; d168 = Proxy
+d169 :: Proxy D169; d169 = Proxy
+d170 :: Proxy D170; d170 = Proxy
+d171 :: Proxy D171; d171 = Proxy
+d172 :: Proxy D172; d172 = Proxy
+d173 :: Proxy D173; d173 = Proxy
+d174 :: Proxy D174; d174 = Proxy
+d175 :: Proxy D175; d175 = Proxy
+d176 :: Proxy D176; d176 = Proxy
+d177 :: Proxy D177; d177 = Proxy
+d178 :: Proxy D178; d178 = Proxy
+d179 :: Proxy D179; d179 = Proxy
+d180 :: Proxy D180; d180 = Proxy
+d181 :: Proxy D181; d181 = Proxy
+d182 :: Proxy D182; d182 = Proxy
+d183 :: Proxy D183; d183 = Proxy
+d184 :: Proxy D184; d184 = Proxy
+d185 :: Proxy D185; d185 = Proxy
+d186 :: Proxy D186; d186 = Proxy
+d187 :: Proxy D187; d187 = Proxy
+d188 :: Proxy D188; d188 = Proxy
+d189 :: Proxy D189; d189 = Proxy
+d190 :: Proxy D190; d190 = Proxy
+d191 :: Proxy D191; d191 = Proxy
+d192 :: Proxy D192; d192 = Proxy
+d193 :: Proxy D193; d193 = Proxy
+d194 :: Proxy D194; d194 = Proxy
+d195 :: Proxy D195; d195 = Proxy
+d196 :: Proxy D196; d196 = Proxy
+d197 :: Proxy D197; d197 = Proxy
+d198 :: Proxy D198; d198 = Proxy
+d199 :: Proxy D199; d199 = Proxy
+d200 :: Proxy D200; d200 = Proxy
+d201 :: Proxy D201; d201 = Proxy
+d202 :: Proxy D202; d202 = Proxy
+d203 :: Proxy D203; d203 = Proxy
+d204 :: Proxy D204; d204 = Proxy
+d205 :: Proxy D205; d205 = Proxy
+d206 :: Proxy D206; d206 = Proxy
+d207 :: Proxy D207; d207 = Proxy
+d208 :: Proxy D208; d208 = Proxy
+d209 :: Proxy D209; d209 = Proxy
+d210 :: Proxy D210; d210 = Proxy
+d211 :: Proxy D211; d211 = Proxy
+d212 :: Proxy D212; d212 = Proxy
+d213 :: Proxy D213; d213 = Proxy
+d214 :: Proxy D214; d214 = Proxy
+d215 :: Proxy D215; d215 = Proxy
+d216 :: Proxy D216; d216 = Proxy
+d217 :: Proxy D217; d217 = Proxy
+d218 :: Proxy D218; d218 = Proxy
+d219 :: Proxy D219; d219 = Proxy
+d220 :: Proxy D220; d220 = Proxy
+d221 :: Proxy D221; d221 = Proxy
+d222 :: Proxy D222; d222 = Proxy
+d223 :: Proxy D223; d223 = Proxy
+d224 :: Proxy D224; d224 = Proxy
+d225 :: Proxy D225; d225 = Proxy
+d226 :: Proxy D226; d226 = Proxy
+d227 :: Proxy D227; d227 = Proxy
+d228 :: Proxy D228; d228 = Proxy
+d229 :: Proxy D229; d229 = Proxy
+d230 :: Proxy D230; d230 = Proxy
+d231 :: Proxy D231; d231 = Proxy
+d232 :: Proxy D232; d232 = Proxy
+d233 :: Proxy D233; d233 = Proxy
+d234 :: Proxy D234; d234 = Proxy
+d235 :: Proxy D235; d235 = Proxy
+d236 :: Proxy D236; d236 = Proxy
+d237 :: Proxy D237; d237 = Proxy
+d238 :: Proxy D238; d238 = Proxy
+d239 :: Proxy D239; d239 = Proxy
+d240 :: Proxy D240; d240 = Proxy
+d241 :: Proxy D241; d241 = Proxy
+d242 :: Proxy D242; d242 = Proxy
+d243 :: Proxy D243; d243 = Proxy
+d244 :: Proxy D244; d244 = Proxy
+d245 :: Proxy D245; d245 = Proxy
+d246 :: Proxy D246; d246 = Proxy
+d247 :: Proxy D247; d247 = Proxy
+d248 :: Proxy D248; d248 = Proxy
+d249 :: Proxy D249; d249 = Proxy
+d250 :: Proxy D250; d250 = Proxy
+d251 :: Proxy D251; d251 = Proxy
+d252 :: Proxy D252; d252 = Proxy
+d253 :: Proxy D253; d253 = Proxy
+d254 :: Proxy D254; d254 = Proxy
+d255 :: Proxy D255; d255 = Proxy
+d256 :: Proxy D256; d256 = Proxy
+
+dn1 :: Proxy DN1; dn1 = Proxy
+dn2 :: Proxy DN2; dn2 = Proxy
+dn3 :: Proxy DN3; dn3 = Proxy
+dn4 :: Proxy DN4; dn4 = Proxy
+dn5 :: Proxy DN5; dn5 = Proxy
+dn6 :: Proxy DN6; dn6 = Proxy
+dn7 :: Proxy DN7; dn7 = Proxy
+dn8 :: Proxy DN8; dn8 = Proxy
+dn9 :: Proxy DN9; dn9 = Proxy
+dn10 :: Proxy DN10; dn10 = Proxy
+dn11 :: Proxy DN11; dn11 = Proxy
+dn12 :: Proxy DN12; dn12 = Proxy
+dn13 :: Proxy DN13; dn13 = Proxy
+dn14 :: Proxy DN14; dn14 = Proxy
+dn15 :: Proxy DN15; dn15 = Proxy
+dn16 :: Proxy DN16; dn16 = Proxy
+dn17 :: Proxy DN17; dn17 = Proxy
+dn18 :: Proxy DN18; dn18 = Proxy
+dn19 :: Proxy DN19; dn19 = Proxy
+dn20 :: Proxy DN20; dn20 = Proxy
+dn21 :: Proxy DN21; dn21 = Proxy
+dn22 :: Proxy DN22; dn22 = Proxy
+dn23 :: Proxy DN23; dn23 = Proxy
+dn24 :: Proxy DN24; dn24 = Proxy
+dn25 :: Proxy DN25; dn25 = Proxy
+dn26 :: Proxy DN26; dn26 = Proxy
+dn27 :: Proxy DN27; dn27 = Proxy
+dn28 :: Proxy DN28; dn28 = Proxy
+dn29 :: Proxy DN29; dn29 = Proxy
+dn30 :: Proxy DN30; dn30 = Proxy
+dn31 :: Proxy DN31; dn31 = Proxy
+dn32 :: Proxy DN32; dn32 = Proxy
+dn33 :: Proxy DN33; dn33 = Proxy
+dn34 :: Proxy DN34; dn34 = Proxy
+dn35 :: Proxy DN35; dn35 = Proxy
+dn36 :: Proxy DN36; dn36 = Proxy
+dn37 :: Proxy DN37; dn37 = Proxy
+dn38 :: Proxy DN38; dn38 = Proxy
+dn39 :: Proxy DN39; dn39 = Proxy
+dn40 :: Proxy DN40; dn40 = Proxy
+dn41 :: Proxy DN41; dn41 = Proxy
+dn42 :: Proxy DN42; dn42 = Proxy
+dn43 :: Proxy DN43; dn43 = Proxy
+dn44 :: Proxy DN44; dn44 = Proxy
+dn45 :: Proxy DN45; dn45 = Proxy
+dn46 :: Proxy DN46; dn46 = Proxy
+dn47 :: Proxy DN47; dn47 = Proxy
+dn48 :: Proxy DN48; dn48 = Proxy
+dn49 :: Proxy DN49; dn49 = Proxy
+dn50 :: Proxy DN50; dn50 = Proxy
+dn51 :: Proxy DN51; dn51 = Proxy
+dn52 :: Proxy DN52; dn52 = Proxy
+dn53 :: Proxy DN53; dn53 = Proxy
+dn54 :: Proxy DN54; dn54 = Proxy
+dn55 :: Proxy DN55; dn55 = Proxy
+dn56 :: Proxy DN56; dn56 = Proxy
+dn57 :: Proxy DN57; dn57 = Proxy
+dn58 :: Proxy DN58; dn58 = Proxy
+dn59 :: Proxy DN59; dn59 = Proxy
+dn60 :: Proxy DN60; dn60 = Proxy
+dn61 :: Proxy DN61; dn61 = Proxy
+dn62 :: Proxy DN62; dn62 = Proxy
+dn63 :: Proxy DN63; dn63 = Proxy
+dn64 :: Proxy DN64; dn64 = Proxy
+dn65 :: Proxy DN65; dn65 = Proxy
+dn66 :: Proxy DN66; dn66 = Proxy
+dn67 :: Proxy DN67; dn67 = Proxy
+dn68 :: Proxy DN68; dn68 = Proxy
+dn69 :: Proxy DN69; dn69 = Proxy
+dn70 :: Proxy DN70; dn70 = Proxy
+dn71 :: Proxy DN71; dn71 = Proxy
+dn72 :: Proxy DN72; dn72 = Proxy
+dn73 :: Proxy DN73; dn73 = Proxy
+dn74 :: Proxy DN74; dn74 = Proxy
+dn75 :: Proxy DN75; dn75 = Proxy
+dn76 :: Proxy DN76; dn76 = Proxy
+dn77 :: Proxy DN77; dn77 = Proxy
+dn78 :: Proxy DN78; dn78 = Proxy
+dn79 :: Proxy DN79; dn79 = Proxy
+dn80 :: Proxy DN80; dn80 = Proxy
+dn81 :: Proxy DN81; dn81 = Proxy
+dn82 :: Proxy DN82; dn82 = Proxy
+dn83 :: Proxy DN83; dn83 = Proxy
+dn84 :: Proxy DN84; dn84 = Proxy
+dn85 :: Proxy DN85; dn85 = Proxy
+dn86 :: Proxy DN86; dn86 = Proxy
+dn87 :: Proxy DN87; dn87 = Proxy
+dn88 :: Proxy DN88; dn88 = Proxy
+dn89 :: Proxy DN89; dn89 = Proxy
+dn90 :: Proxy DN90; dn90 = Proxy
+dn91 :: Proxy DN91; dn91 = Proxy
+dn92 :: Proxy DN92; dn92 = Proxy
+dn93 :: Proxy DN93; dn93 = Proxy
+dn94 :: Proxy DN94; dn94 = Proxy
+dn95 :: Proxy DN95; dn95 = Proxy
+dn96 :: Proxy DN96; dn96 = Proxy
+dn97 :: Proxy DN97; dn97 = Proxy
+dn98 :: Proxy DN98; dn98 = Proxy
+dn99 :: Proxy DN99; dn99 = Proxy
+dn100 :: Proxy DN100; dn100 = Proxy
+dn101 :: Proxy DN101; dn101 = Proxy
+dn102 :: Proxy DN102; dn102 = Proxy
+dn103 :: Proxy DN103; dn103 = Proxy
+dn104 :: Proxy DN104; dn104 = Proxy
+dn105 :: Proxy DN105; dn105 = Proxy
+dn106 :: Proxy DN106; dn106 = Proxy
+dn107 :: Proxy DN107; dn107 = Proxy
+dn108 :: Proxy DN108; dn108 = Proxy
+dn109 :: Proxy DN109; dn109 = Proxy
+dn110 :: Proxy DN110; dn110 = Proxy
+dn111 :: Proxy DN111; dn111 = Proxy
+dn112 :: Proxy DN112; dn112 = Proxy
+dn113 :: Proxy DN113; dn113 = Proxy
+dn114 :: Proxy DN114; dn114 = Proxy
+dn115 :: Proxy DN115; dn115 = Proxy
+dn116 :: Proxy DN116; dn116 = Proxy
+dn117 :: Proxy DN117; dn117 = Proxy
+dn118 :: Proxy DN118; dn118 = Proxy
+dn119 :: Proxy DN119; dn119 = Proxy
+dn120 :: Proxy DN120; dn120 = Proxy
+dn121 :: Proxy DN121; dn121 = Proxy
+dn122 :: Proxy DN122; dn122 = Proxy
+dn123 :: Proxy DN123; dn123 = Proxy
+dn124 :: Proxy DN124; dn124 = Proxy
+dn125 :: Proxy DN125; dn125 = Proxy
+dn126 :: Proxy DN126; dn126 = Proxy
+dn127 :: Proxy DN127; dn127 = Proxy
+dn128 :: Proxy DN128; dn128 = Proxy
+dn129 :: Proxy DN129; dn129 = Proxy
+dn130 :: Proxy DN130; dn130 = Proxy
+dn131 :: Proxy DN131; dn131 = Proxy
+dn132 :: Proxy DN132; dn132 = Proxy
+dn133 :: Proxy DN133; dn133 = Proxy
+dn134 :: Proxy DN134; dn134 = Proxy
+dn135 :: Proxy DN135; dn135 = Proxy
+dn136 :: Proxy DN136; dn136 = Proxy
+dn137 :: Proxy DN137; dn137 = Proxy
+dn138 :: Proxy DN138; dn138 = Proxy
+dn139 :: Proxy DN139; dn139 = Proxy
+dn140 :: Proxy DN140; dn140 = Proxy
+dn141 :: Proxy DN141; dn141 = Proxy
+dn142 :: Proxy DN142; dn142 = Proxy
+dn143 :: Proxy DN143; dn143 = Proxy
+dn144 :: Proxy DN144; dn144 = Proxy
+dn145 :: Proxy DN145; dn145 = Proxy
+dn146 :: Proxy DN146; dn146 = Proxy
+dn147 :: Proxy DN147; dn147 = Proxy
+dn148 :: Proxy DN148; dn148 = Proxy
+dn149 :: Proxy DN149; dn149 = Proxy
+dn150 :: Proxy DN150; dn150 = Proxy
+dn151 :: Proxy DN151; dn151 = Proxy
+dn152 :: Proxy DN152; dn152 = Proxy
+dn153 :: Proxy DN153; dn153 = Proxy
+dn154 :: Proxy DN154; dn154 = Proxy
+dn155 :: Proxy DN155; dn155 = Proxy
+dn156 :: Proxy DN156; dn156 = Proxy
+dn157 :: Proxy DN157; dn157 = Proxy
+dn158 :: Proxy DN158; dn158 = Proxy
+dn159 :: Proxy DN159; dn159 = Proxy
+dn160 :: Proxy DN160; dn160 = Proxy
+dn161 :: Proxy DN161; dn161 = Proxy
+dn162 :: Proxy DN162; dn162 = Proxy
+dn163 :: Proxy DN163; dn163 = Proxy
+dn164 :: Proxy DN164; dn164 = Proxy
+dn165 :: Proxy DN165; dn165 = Proxy
+dn166 :: Proxy DN166; dn166 = Proxy
+dn167 :: Proxy DN167; dn167 = Proxy
+dn168 :: Proxy DN168; dn168 = Proxy
+dn169 :: Proxy DN169; dn169 = Proxy
+dn170 :: Proxy DN170; dn170 = Proxy
+dn171 :: Proxy DN171; dn171 = Proxy
+dn172 :: Proxy DN172; dn172 = Proxy
+dn173 :: Proxy DN173; dn173 = Proxy
+dn174 :: Proxy DN174; dn174 = Proxy
+dn175 :: Proxy DN175; dn175 = Proxy
+dn176 :: Proxy DN176; dn176 = Proxy
+dn177 :: Proxy DN177; dn177 = Proxy
+dn178 :: Proxy DN178; dn178 = Proxy
+dn179 :: Proxy DN179; dn179 = Proxy
+dn180 :: Proxy DN180; dn180 = Proxy
+dn181 :: Proxy DN181; dn181 = Proxy
+dn182 :: Proxy DN182; dn182 = Proxy
+dn183 :: Proxy DN183; dn183 = Proxy
+dn184 :: Proxy DN184; dn184 = Proxy
+dn185 :: Proxy DN185; dn185 = Proxy
+dn186 :: Proxy DN186; dn186 = Proxy
+dn187 :: Proxy DN187; dn187 = Proxy
+dn188 :: Proxy DN188; dn188 = Proxy
+dn189 :: Proxy DN189; dn189 = Proxy
+dn190 :: Proxy DN190; dn190 = Proxy
+dn191 :: Proxy DN191; dn191 = Proxy
+dn192 :: Proxy DN192; dn192 = Proxy
+dn193 :: Proxy DN193; dn193 = Proxy
+dn194 :: Proxy DN194; dn194 = Proxy
+dn195 :: Proxy DN195; dn195 = Proxy
+dn196 :: Proxy DN196; dn196 = Proxy
+dn197 :: Proxy DN197; dn197 = Proxy
+dn198 :: Proxy DN198; dn198 = Proxy
+dn199 :: Proxy DN199; dn199 = Proxy
+dn200 :: Proxy DN200; dn200 = Proxy
+dn201 :: Proxy DN201; dn201 = Proxy
+dn202 :: Proxy DN202; dn202 = Proxy
+dn203 :: Proxy DN203; dn203 = Proxy
+dn204 :: Proxy DN204; dn204 = Proxy
+dn205 :: Proxy DN205; dn205 = Proxy
+dn206 :: Proxy DN206; dn206 = Proxy
+dn207 :: Proxy DN207; dn207 = Proxy
+dn208 :: Proxy DN208; dn208 = Proxy
+dn209 :: Proxy DN209; dn209 = Proxy
+dn210 :: Proxy DN210; dn210 = Proxy
+dn211 :: Proxy DN211; dn211 = Proxy
+dn212 :: Proxy DN212; dn212 = Proxy
+dn213 :: Proxy DN213; dn213 = Proxy
+dn214 :: Proxy DN214; dn214 = Proxy
+dn215 :: Proxy DN215; dn215 = Proxy
+dn216 :: Proxy DN216; dn216 = Proxy
+dn217 :: Proxy DN217; dn217 = Proxy
+dn218 :: Proxy DN218; dn218 = Proxy
+dn219 :: Proxy DN219; dn219 = Proxy
+dn220 :: Proxy DN220; dn220 = Proxy
+dn221 :: Proxy DN221; dn221 = Proxy
+dn222 :: Proxy DN222; dn222 = Proxy
+dn223 :: Proxy DN223; dn223 = Proxy
+dn224 :: Proxy DN224; dn224 = Proxy
+dn225 :: Proxy DN225; dn225 = Proxy
+dn226 :: Proxy DN226; dn226 = Proxy
+dn227 :: Proxy DN227; dn227 = Proxy
+dn228 :: Proxy DN228; dn228 = Proxy
+dn229 :: Proxy DN229; dn229 = Proxy
+dn230 :: Proxy DN230; dn230 = Proxy
+dn231 :: Proxy DN231; dn231 = Proxy
+dn232 :: Proxy DN232; dn232 = Proxy
+dn233 :: Proxy DN233; dn233 = Proxy
+dn234 :: Proxy DN234; dn234 = Proxy
+dn235 :: Proxy DN235; dn235 = Proxy
+dn236 :: Proxy DN236; dn236 = Proxy
+dn237 :: Proxy DN237; dn237 = Proxy
+dn238 :: Proxy DN238; dn238 = Proxy
+dn239 :: Proxy DN239; dn239 = Proxy
+dn240 :: Proxy DN240; dn240 = Proxy
+dn241 :: Proxy DN241; dn241 = Proxy
+dn242 :: Proxy DN242; dn242 = Proxy
+dn243 :: Proxy DN243; dn243 = Proxy
+dn244 :: Proxy DN244; dn244 = Proxy
+dn245 :: Proxy DN245; dn245 = Proxy
+dn246 :: Proxy DN246; dn246 = Proxy
+dn247 :: Proxy DN247; dn247 = Proxy
+dn248 :: Proxy DN248; dn248 = Proxy
+dn249 :: Proxy DN249; dn249 = Proxy
+dn250 :: Proxy DN250; dn250 = Proxy
+dn251 :: Proxy DN251; dn251 = Proxy
+dn252 :: Proxy DN252; dn252 = Proxy
+dn253 :: Proxy DN253; dn253 = Proxy
+dn254 :: Proxy DN254; dn254 = Proxy
+dn255 :: Proxy DN255; dn255 = Proxy
+dn256 :: Proxy DN256; dn256 = Proxy
diff --git a/src/Type/Data/Num/Decimal/Number.hs b/src/Type/Data/Num/Decimal/Number.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal/Number.hs
@@ -0,0 +1,1516 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Rank2Types #-}
+
+module Type.Data.Num.Decimal.Number (
+    Decimal, decimal,
+    Dec, Zero, Pos, Neg, EndAsc, (:<), EndDesc, (:>),
+    Singleton(..), singleton, singletonFromProxy,
+    integerFromSingleton, integralFromSingleton,
+    integralFromProxy,
+
+    Integer(..), Natural(..),
+    Positive(..), Negative(..),
+
+    reifyIntegral, reifyNatural,
+    reifyPositive, reifyNegative,
+    reifyPos, reifyNeg,
+
+    Digits(..),
+
+    (:+:), (:-:), (:*:),
+    Pred, Succ, Compare, IsEven, Pow2, Log2Ceil,
+
+    (:<:), (:<=:), (:==:),
+    (:>:), (:>=:), (:/=:),
+
+    FromUnary, ToUnary,
+    ToUnaryAcc, UnaryAcc, -- for Proof
+    ) where
+
+import qualified Type.Data.Num.Decimal.Digit as Digit
+import qualified Type.Data.Num.Unary.Literal as UnaryLit
+import qualified Type.Data.Num.Unary as Unary
+import qualified Type.Data.Num as Op
+import qualified Type.Data.Ord as Ord
+import qualified Type.Base.Proxy as Proxy
+
+import Type.Data.Num.Decimal.Digit
+          (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)
+import Type.Data.Bool (If, False, True)
+import Type.Data.Ord (LT, GT, EQ)
+import Type.Base.Proxy (Proxy(Proxy))
+
+import Data.Maybe.HT (toMaybe)
+import Data.Tuple.HT (swap)
+import qualified Data.List as List
+
+import Text.Printf (printf)
+
+import qualified Prelude as P
+import Prelude hiding (Integer)
+
+
+-- | Representation name for decimal type level numbers.
+data Decimal
+
+-- | The wrapper type for decimal type level numbers.
+data Dec x
+data Zero
+data Neg x xs
+data Pos x xs
+
+
+infixl 9 :<
+
+data ds :< d
+{-
+instance (Show ds, Show d) => Show (ds :< d) where
+    show _ = show (undefined :: ds) ++ show (undefined :: d)
+-}
+
+infixr 9 :>
+
+data d :> ds
+{-
+instance (Show ds, Show d) => Show (d :> ds) where
+    show _ = show (undefined :: d) ++ show (undefined :: ds)
+-}
+
+
+-- | The terminator type for ascending decimal digit lists.
+{-
+we could add a type parameter to EndAsc
+in order to assert non-empty ascending lists
+-}
+data EndAsc
+instance Show EndAsc where
+    show _ = ""
+
+-- | The terminator type for descending decimal digit lists.
+data EndDesc
+instance Show EndDesc where
+    show _ = ""
+
+
+instance Op.Representation Decimal where
+    reifyIntegral _ i k = reifyIntegral i (k . decimal)
+
+decimal :: Proxy n -> Proxy (Dec n)
+decimal Proxy = Proxy
+
+stripDec :: Proxy (Dec n) -> Proxy n
+stripDec Proxy = Proxy
+
+
+instance Integer a => Proxy.Show (Dec a) where
+   showsPrec prec =
+      (\n -> showParen (prec>10) (showString (printf "decimal d%d" n)))
+       . integerFromSingleton . singletonFromProxy . stripDec
+
+
+reifyIntegral :: P.Integer -> (forall s. Integer s => Proxy s -> w) -> w
+reifyIntegral n f =
+    if n < 0
+      then
+          case reverse $ digits $ negate n of
+              [] -> error "negative means non-zero"
+              x:xs ->
+                  Digit.reifyPos x (\d -> go xs (\ds -> f (negDigits d ds)))
+      else
+          case reverse $ digits n of
+              [] -> f (Proxy :: Proxy Zero)
+              x:xs ->
+                  Digit.reifyPos x (\d -> go xs (\ds -> f (posDigits d ds)))
+  where
+   go :: [P.Integer] -> (forall s. Digits s => Proxy s -> w) -> w
+   go [] k = k (Proxy :: Proxy EndDesc)
+   go (j:js) k = Digit.reify j (\d -> go js (\ds -> k (consDigits d ds)))
+
+
+negDigits :: Proxy d -> Proxy ds -> Proxy (Neg d ds)
+negDigits Proxy Proxy = Proxy
+
+posDigits :: Proxy d -> Proxy ds -> Proxy (Pos d ds)
+posDigits Proxy Proxy = Proxy
+
+consDigits :: Proxy d -> Proxy ds -> Proxy (d :> ds)
+consDigits Proxy Proxy = Proxy
+
+
+digits :: P.Integer -> [P.Integer]
+digits =
+    List.unfoldr (\n -> toMaybe (n/=0) (swap $ quotRem n 10))
+
+
+reifyPos ::
+    P.Integer ->
+    (forall x xs. (Digit.Pos x, Digits xs) => Proxy (Pos x xs) -> a) ->
+    Maybe a
+reifyPos n f =
+    reifyIntegral n
+        (runCont $ switch reject reject (accept f))
+
+reifyNeg ::
+    P.Integer ->
+    (forall x xs. (Digit.Pos x, Digits xs) => Proxy (Neg x xs) -> a) ->
+    Maybe a
+reifyNeg n f =
+    reifyIntegral n
+        (runCont $ switch reject (accept f) reject)
+
+reifyPositive ::
+    P.Integer -> (forall s. (Positive s) => Proxy s -> a) -> Maybe a
+reifyPositive n f = reifyPos n f
+
+reifyNegative ::
+    P.Integer -> (forall s. (Negative s) => Proxy s -> a) -> Maybe a
+reifyNegative n f = reifyNeg n f
+
+reifyNatural ::
+    P.Integer -> (forall s. (Natural s) => Proxy s -> a) -> Maybe a
+reifyNatural n f =
+    reifyIntegral n
+        (runCont $ switch (accept f) reject (accept f))
+
+newtype Cont a s = Cont {runCont :: Proxy s -> Maybe a}
+
+accept :: (Proxy s -> a) -> Cont a s
+accept f = Cont (Just . f)
+
+reject :: Cont a s
+reject = Cont (const Nothing)
+
+
+instance Integer x => Op.Integer (Dec x) where
+    singleton = singletonToGeneric singleton
+    type Repr (Dec x) = Decimal
+
+singletonToGeneric :: Singleton x -> Op.Singleton (Dec x)
+singletonToGeneric (Singleton n) = Op.Singleton n
+
+
+class Integer n where
+    switch ::
+        f Zero ->
+        (forall x xs. (Digit.Pos x, Digits xs) => f (Neg x xs)) ->
+        (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->
+        f n
+
+instance Integer Zero where
+    switch x _ _ = x
+instance (Digit.Pos x, Digits xs) => Integer (Neg x xs) where
+    switch _ x _ = x
+instance (Digit.Pos x, Digits xs) => Integer (Pos x xs) where
+    switch _ _ x = x
+
+
+class Integer n => Natural n where
+    switchNat ::
+        f Zero ->
+        (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->
+        f n
+
+instance Natural Zero where
+    switchNat x _ = x
+instance (Digit.Pos x, Digits xs) => Natural (Pos x xs) where
+    switchNat _ x = x
+
+
+class Natural n => Positive n where
+    switchPos ::
+        (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->
+        f n
+
+instance (Digit.Pos x, Digits xs) => Positive (Pos x xs) where
+    switchPos x = x
+
+
+class Integer n => Negative n where
+    switchNeg ::
+        (forall x xs. (Digit.Pos x, Digits xs) => f (Neg x xs)) ->
+        f n
+
+instance (Digit.Pos x, Digits xs) => Negative (Neg x xs) where
+    switchNeg x = x
+
+
+newtype Singleton x = Singleton P.Integer
+
+singleton :: (Integer x) => Singleton x
+singleton =
+    switch
+        (Singleton 0)
+        (withProxy $ \(Digit.Singleton n) proxy ->
+             negate (fromDigits (fromIntegral n) proxy))
+        (withProxy $ \(Digit.Singleton n) proxy ->
+             fromDigits (fromIntegral n) proxy)
+
+withProxy ::
+    (Digit.C x) =>
+    (Digit.Singleton x -> Proxy xs -> P.Integer) -> Singleton (cons x xs)
+withProxy f = Singleton $ f Digit.singleton Proxy
+
+integerFromSingleton :: (Integer n) => Singleton n -> P.Integer
+integerFromSingleton (Singleton n) = n
+
+integralFromSingleton :: (Integer n, Num a) => Singleton n -> a
+integralFromSingleton = fromInteger . integerFromSingleton
+
+singletonFromProxy :: (Integer n) => Proxy n -> Singleton n
+singletonFromProxy Proxy = singleton
+
+integralFromProxy :: (Integer n, Num a) => Proxy n -> a
+integralFromProxy = integralFromSingleton . singletonFromProxy
+
+
+class Digits xs where
+    switchDigits ::
+        f EndDesc ->
+        (forall xh xl. (Digit.C xh, Digits xl) => f (xh :> xl)) ->
+        f xs
+instance Digits EndDesc where
+    switchDigits x _ = x
+instance (Digit.C xh, Digits xl) => Digits (xh :> xl) where
+    switchDigits _ x = x
+
+newtype
+    FromDigits y xs =
+        FromDigits {runFromDigits :: y -> Proxy xs -> y}
+
+fromDigits :: (Num y, Digits xs) => y -> Proxy xs -> y
+fromDigits =
+    runFromDigits $
+    switchDigits
+        (FromDigits $ \acc _ -> acc)
+        (FromDigits $ \acc ->
+         withDigits $ \(Digit.Singleton n) xl ->
+             fromDigits (10*acc + fromIntegral n) xl)
+
+withDigits ::
+    (Digit.C xh) =>
+    (Digit.Singleton xh -> Proxy xl -> a) -> Proxy (xh :> xl) -> a
+withDigits f Proxy = f Digit.singleton Proxy
+
+
+type Id x = x
+
+type family NormalizePos x
+type instance NormalizePos EndDesc = Zero
+type instance NormalizePos (Dec0 :> xl) = NormalizePos xl
+type instance NormalizePos (Dec1 :> xl) = Pos Dec1 xl
+type instance NormalizePos (Dec2 :> xl) = Pos Dec2 xl
+type instance NormalizePos (Dec3 :> xl) = Pos Dec3 xl
+type instance NormalizePos (Dec4 :> xl) = Pos Dec4 xl
+type instance NormalizePos (Dec5 :> xl) = Pos Dec5 xl
+type instance NormalizePos (Dec6 :> xl) = Pos Dec6 xl
+type instance NormalizePos (Dec7 :> xl) = Pos Dec7 xl
+type instance NormalizePos (Dec8 :> xl) = Pos Dec8 xl
+type instance NormalizePos (Dec9 :> xl) = Pos Dec9 xl
+
+type family NormalizeNeg x
+type instance NormalizeNeg EndDesc = Zero
+type instance NormalizeNeg (Dec0 :> xl) = NormalizeNeg xl
+type instance NormalizeNeg (Dec1 :> xl) = Neg Dec1 xl
+type instance NormalizeNeg (Dec2 :> xl) = Neg Dec2 xl
+type instance NormalizeNeg (Dec3 :> xl) = Neg Dec3 xl
+type instance NormalizeNeg (Dec4 :> xl) = Neg Dec4 xl
+type instance NormalizeNeg (Dec5 :> xl) = Neg Dec5 xl
+type instance NormalizeNeg (Dec6 :> xl) = Neg Dec6 xl
+type instance NormalizeNeg (Dec7 :> xl) = Neg Dec7 xl
+type instance NormalizeNeg (Dec8 :> xl) = Neg Dec8 xl
+type instance NormalizeNeg (Dec9 :> xl) = Neg Dec9 xl
+
+type family Ascending x y
+type instance Ascending y EndDesc = y
+type instance Ascending y (xh :> xl) = Ascending (y :< xh) xl
+
+type AscendingNonEmpty x xs = Ascending (EndAsc:<x) xs
+
+type family Descending x y
+type instance Descending EndAsc y = y
+type instance Descending (xh :< xl) y = Descending xh (xl :> y)
+
+type NormalizePosDesc xs = NormalizePos (Descending xs EndDesc)
+type NormalizeNegDesc xs = NormalizeNeg (Descending xs EndDesc)
+
+
+-- type family Op.IsPositive x
+type instance Op.IsPositive (Dec x) = IsPositive x
+type family IsPositive x
+type instance IsPositive (Neg _x _xs) = False
+type instance IsPositive Zero         = False
+type instance IsPositive (Pos _x _xs) = True
+
+-- type family Op.IsZero x
+type instance Op.IsZero (Dec x) = IsZero x
+type family IsZero x
+type instance IsZero (Neg _x _xs) = False
+type instance IsZero Zero         = True
+type instance IsZero (Pos _x _xs) = False
+
+-- type family Op.IsNegative x
+type instance Op.IsNegative (Dec x) = IsNegative x
+type family IsNegative x
+type instance IsNegative (Neg _x _xs) = True
+type instance IsNegative Zero         = False
+type instance IsNegative (Pos _x _xs) = False
+
+-- type family Op.IsNatural x
+type instance Op.IsNatural (Dec x) = IsNatural x
+type family IsNatural x
+type instance IsNatural (Neg _x _xs) = False
+type instance IsNatural Zero         = True
+type instance IsNatural (Pos _x _xs) = True
+
+-- type family Op.Negate x
+type instance Op.Negate (Dec x) = Dec (Negate x)
+
+type family Negate x
+type instance Negate Zero       = Zero
+type instance Negate (Neg x xs) = Pos x xs
+type instance Negate (Pos x xs) = Neg x xs
+
+-- type family Op.One r
+type instance Op.One Decimal = Dec One
+type One = Pos Dec1 EndDesc
+
+-- type family Op.Succ x
+type instance Op.Succ (Dec x) = Dec (Succ x)
+
+type family Succ x
+type instance Succ Zero = One
+type instance Succ (Pos x xs) =
+        NormalizePosDesc (SuccAsc (AscendingNonEmpty x xs))
+type instance Succ (Neg x xs) =
+        NormalizeNegDesc (PredAsc (AscendingNonEmpty x xs))
+
+type family SuccAsc x
+type instance SuccAsc EndAsc = EndAsc :< Dec1
+type instance SuccAsc (x :< Dec0) = x :< Dec1
+type instance SuccAsc (x :< Dec1) = x :< Dec2
+type instance SuccAsc (x :< Dec2) = x :< Dec3
+type instance SuccAsc (x :< Dec3) = x :< Dec4
+type instance SuccAsc (x :< Dec4) = x :< Dec5
+type instance SuccAsc (x :< Dec5) = x :< Dec6
+type instance SuccAsc (x :< Dec6) = x :< Dec7
+type instance SuccAsc (x :< Dec7) = x :< Dec8
+type instance SuccAsc (x :< Dec8) = x :< Dec9
+type instance SuccAsc (x :< Dec9) = SuccAsc x :< Dec0
+
+-- type family Op.Pred x
+type instance Op.Pred (Dec x) = Dec (Pred x)
+
+type family Pred x
+type instance Pred Zero = Neg Dec1 EndDesc
+type instance Pred (Neg x xs) =
+        NormalizeNegDesc (SuccAsc (AscendingNonEmpty x xs))
+type instance Pred (Pos x xs) =
+        NormalizePosDesc (PredAsc (AscendingNonEmpty x xs))
+
+type family PredAsc x
+type instance PredAsc (x :< Dec0) = PredAsc x :< Dec9
+type instance PredAsc (x :< Dec1) = x :< Dec0
+type instance PredAsc (x :< Dec2) = x :< Dec1
+type instance PredAsc (x :< Dec3) = x :< Dec2
+type instance PredAsc (x :< Dec4) = x :< Dec3
+type instance PredAsc (x :< Dec5) = x :< Dec4
+type instance PredAsc (x :< Dec6) = x :< Dec5
+type instance PredAsc (x :< Dec7) = x :< Dec6
+type instance PredAsc (x :< Dec8) = x :< Dec7
+type instance PredAsc (x :< Dec9) = x :< Dec8
+
+--------------------
+-- Addition
+
+type family AddDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance AddDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x+y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance AddDigit Dec0 Dec0 = Dec0
+type instance AddDigit Dec0 Dec1 = Dec1
+type instance AddDigit Dec0 Dec2 = Dec2
+type instance AddDigit Dec0 Dec3 = Dec3
+type instance AddDigit Dec0 Dec4 = Dec4
+type instance AddDigit Dec0 Dec5 = Dec5
+type instance AddDigit Dec0 Dec6 = Dec6
+type instance AddDigit Dec0 Dec7 = Dec7
+type instance AddDigit Dec0 Dec8 = Dec8
+type instance AddDigit Dec0 Dec9 = Dec9
+
+type instance AddDigit Dec1 Dec0 = Dec1
+type instance AddDigit Dec1 Dec1 = Dec2
+type instance AddDigit Dec1 Dec2 = Dec3
+type instance AddDigit Dec1 Dec3 = Dec4
+type instance AddDigit Dec1 Dec4 = Dec5
+type instance AddDigit Dec1 Dec5 = Dec6
+type instance AddDigit Dec1 Dec6 = Dec7
+type instance AddDigit Dec1 Dec7 = Dec8
+type instance AddDigit Dec1 Dec8 = Dec9
+type instance AddDigit Dec1 Dec9 = Dec0
+
+type instance AddDigit Dec2 Dec0 = Dec2
+type instance AddDigit Dec2 Dec1 = Dec3
+type instance AddDigit Dec2 Dec2 = Dec4
+type instance AddDigit Dec2 Dec3 = Dec5
+type instance AddDigit Dec2 Dec4 = Dec6
+type instance AddDigit Dec2 Dec5 = Dec7
+type instance AddDigit Dec2 Dec6 = Dec8
+type instance AddDigit Dec2 Dec7 = Dec9
+type instance AddDigit Dec2 Dec8 = Dec0
+type instance AddDigit Dec2 Dec9 = Dec1
+
+type instance AddDigit Dec3 Dec0 = Dec3
+type instance AddDigit Dec3 Dec1 = Dec4
+type instance AddDigit Dec3 Dec2 = Dec5
+type instance AddDigit Dec3 Dec3 = Dec6
+type instance AddDigit Dec3 Dec4 = Dec7
+type instance AddDigit Dec3 Dec5 = Dec8
+type instance AddDigit Dec3 Dec6 = Dec9
+type instance AddDigit Dec3 Dec7 = Dec0
+type instance AddDigit Dec3 Dec8 = Dec1
+type instance AddDigit Dec3 Dec9 = Dec2
+
+type instance AddDigit Dec4 Dec0 = Dec4
+type instance AddDigit Dec4 Dec1 = Dec5
+type instance AddDigit Dec4 Dec2 = Dec6
+type instance AddDigit Dec4 Dec3 = Dec7
+type instance AddDigit Dec4 Dec4 = Dec8
+type instance AddDigit Dec4 Dec5 = Dec9
+type instance AddDigit Dec4 Dec6 = Dec0
+type instance AddDigit Dec4 Dec7 = Dec1
+type instance AddDigit Dec4 Dec8 = Dec2
+type instance AddDigit Dec4 Dec9 = Dec3
+
+type instance AddDigit Dec5 Dec0 = Dec5
+type instance AddDigit Dec5 Dec1 = Dec6
+type instance AddDigit Dec5 Dec2 = Dec7
+type instance AddDigit Dec5 Dec3 = Dec8
+type instance AddDigit Dec5 Dec4 = Dec9
+type instance AddDigit Dec5 Dec5 = Dec0
+type instance AddDigit Dec5 Dec6 = Dec1
+type instance AddDigit Dec5 Dec7 = Dec2
+type instance AddDigit Dec5 Dec8 = Dec3
+type instance AddDigit Dec5 Dec9 = Dec4
+
+type instance AddDigit Dec6 Dec0 = Dec6
+type instance AddDigit Dec6 Dec1 = Dec7
+type instance AddDigit Dec6 Dec2 = Dec8
+type instance AddDigit Dec6 Dec3 = Dec9
+type instance AddDigit Dec6 Dec4 = Dec0
+type instance AddDigit Dec6 Dec5 = Dec1
+type instance AddDigit Dec6 Dec6 = Dec2
+type instance AddDigit Dec6 Dec7 = Dec3
+type instance AddDigit Dec6 Dec8 = Dec4
+type instance AddDigit Dec6 Dec9 = Dec5
+
+type instance AddDigit Dec7 Dec0 = Dec7
+type instance AddDigit Dec7 Dec1 = Dec8
+type instance AddDigit Dec7 Dec2 = Dec9
+type instance AddDigit Dec7 Dec3 = Dec0
+type instance AddDigit Dec7 Dec4 = Dec1
+type instance AddDigit Dec7 Dec5 = Dec2
+type instance AddDigit Dec7 Dec6 = Dec3
+type instance AddDigit Dec7 Dec7 = Dec4
+type instance AddDigit Dec7 Dec8 = Dec5
+type instance AddDigit Dec7 Dec9 = Dec6
+
+type instance AddDigit Dec8 Dec0 = Dec8
+type instance AddDigit Dec8 Dec1 = Dec9
+type instance AddDigit Dec8 Dec2 = Dec0
+type instance AddDigit Dec8 Dec3 = Dec1
+type instance AddDigit Dec8 Dec4 = Dec2
+type instance AddDigit Dec8 Dec5 = Dec3
+type instance AddDigit Dec8 Dec6 = Dec4
+type instance AddDigit Dec8 Dec7 = Dec5
+type instance AddDigit Dec8 Dec8 = Dec6
+type instance AddDigit Dec8 Dec9 = Dec7
+
+type instance AddDigit Dec9 Dec0 = Dec9
+type instance AddDigit Dec9 Dec1 = Dec0
+type instance AddDigit Dec9 Dec2 = Dec1
+type instance AddDigit Dec9 Dec3 = Dec2
+type instance AddDigit Dec9 Dec4 = Dec3
+type instance AddDigit Dec9 Dec5 = Dec4
+type instance AddDigit Dec9 Dec6 = Dec5
+type instance AddDigit Dec9 Dec7 = Dec6
+type instance AddDigit Dec9 Dec8 = Dec7
+type instance AddDigit Dec9 Dec9 = Dec8
+
+-- | If adding @x@ and @y@ would not carry, then
+--   @AddCarry x y z@ evaluates to @z@.  Otherwise,
+--   @AddCarry x y z@ evaluates to @SuccAsc z@
+type family AddCarry x y z
+-- putStr $ unlines $ concat $ [ [ "type instance AddCarry Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x + y >= 10 then "SuccAsc" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance AddCarry Dec0 Dec0 x = Id x
+type instance AddCarry Dec0 Dec1 x = Id x
+type instance AddCarry Dec0 Dec2 x = Id x
+type instance AddCarry Dec0 Dec3 x = Id x
+type instance AddCarry Dec0 Dec4 x = Id x
+type instance AddCarry Dec0 Dec5 x = Id x
+type instance AddCarry Dec0 Dec6 x = Id x
+type instance AddCarry Dec0 Dec7 x = Id x
+type instance AddCarry Dec0 Dec8 x = Id x
+type instance AddCarry Dec0 Dec9 x = Id x
+
+type instance AddCarry Dec1 Dec0 x = Id x
+type instance AddCarry Dec1 Dec1 x = Id x
+type instance AddCarry Dec1 Dec2 x = Id x
+type instance AddCarry Dec1 Dec3 x = Id x
+type instance AddCarry Dec1 Dec4 x = Id x
+type instance AddCarry Dec1 Dec5 x = Id x
+type instance AddCarry Dec1 Dec6 x = Id x
+type instance AddCarry Dec1 Dec7 x = Id x
+type instance AddCarry Dec1 Dec8 x = Id x
+type instance AddCarry Dec1 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec2 Dec0 x = Id x
+type instance AddCarry Dec2 Dec1 x = Id x
+type instance AddCarry Dec2 Dec2 x = Id x
+type instance AddCarry Dec2 Dec3 x = Id x
+type instance AddCarry Dec2 Dec4 x = Id x
+type instance AddCarry Dec2 Dec5 x = Id x
+type instance AddCarry Dec2 Dec6 x = Id x
+type instance AddCarry Dec2 Dec7 x = Id x
+type instance AddCarry Dec2 Dec8 x = SuccAsc x
+type instance AddCarry Dec2 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec3 Dec0 x = Id x
+type instance AddCarry Dec3 Dec1 x = Id x
+type instance AddCarry Dec3 Dec2 x = Id x
+type instance AddCarry Dec3 Dec3 x = Id x
+type instance AddCarry Dec3 Dec4 x = Id x
+type instance AddCarry Dec3 Dec5 x = Id x
+type instance AddCarry Dec3 Dec6 x = Id x
+type instance AddCarry Dec3 Dec7 x = SuccAsc x
+type instance AddCarry Dec3 Dec8 x = SuccAsc x
+type instance AddCarry Dec3 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec4 Dec0 x = Id x
+type instance AddCarry Dec4 Dec1 x = Id x
+type instance AddCarry Dec4 Dec2 x = Id x
+type instance AddCarry Dec4 Dec3 x = Id x
+type instance AddCarry Dec4 Dec4 x = Id x
+type instance AddCarry Dec4 Dec5 x = Id x
+type instance AddCarry Dec4 Dec6 x = SuccAsc x
+type instance AddCarry Dec4 Dec7 x = SuccAsc x
+type instance AddCarry Dec4 Dec8 x = SuccAsc x
+type instance AddCarry Dec4 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec5 Dec0 x = Id x
+type instance AddCarry Dec5 Dec1 x = Id x
+type instance AddCarry Dec5 Dec2 x = Id x
+type instance AddCarry Dec5 Dec3 x = Id x
+type instance AddCarry Dec5 Dec4 x = Id x
+type instance AddCarry Dec5 Dec5 x = SuccAsc x
+type instance AddCarry Dec5 Dec6 x = SuccAsc x
+type instance AddCarry Dec5 Dec7 x = SuccAsc x
+type instance AddCarry Dec5 Dec8 x = SuccAsc x
+type instance AddCarry Dec5 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec6 Dec0 x = Id x
+type instance AddCarry Dec6 Dec1 x = Id x
+type instance AddCarry Dec6 Dec2 x = Id x
+type instance AddCarry Dec6 Dec3 x = Id x
+type instance AddCarry Dec6 Dec4 x = SuccAsc x
+type instance AddCarry Dec6 Dec5 x = SuccAsc x
+type instance AddCarry Dec6 Dec6 x = SuccAsc x
+type instance AddCarry Dec6 Dec7 x = SuccAsc x
+type instance AddCarry Dec6 Dec8 x = SuccAsc x
+type instance AddCarry Dec6 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec7 Dec0 x = Id x
+type instance AddCarry Dec7 Dec1 x = Id x
+type instance AddCarry Dec7 Dec2 x = Id x
+type instance AddCarry Dec7 Dec3 x = SuccAsc x
+type instance AddCarry Dec7 Dec4 x = SuccAsc x
+type instance AddCarry Dec7 Dec5 x = SuccAsc x
+type instance AddCarry Dec7 Dec6 x = SuccAsc x
+type instance AddCarry Dec7 Dec7 x = SuccAsc x
+type instance AddCarry Dec7 Dec8 x = SuccAsc x
+type instance AddCarry Dec7 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec8 Dec0 x = Id x
+type instance AddCarry Dec8 Dec1 x = Id x
+type instance AddCarry Dec8 Dec2 x = SuccAsc x
+type instance AddCarry Dec8 Dec3 x = SuccAsc x
+type instance AddCarry Dec8 Dec4 x = SuccAsc x
+type instance AddCarry Dec8 Dec5 x = SuccAsc x
+type instance AddCarry Dec8 Dec6 x = SuccAsc x
+type instance AddCarry Dec8 Dec7 x = SuccAsc x
+type instance AddCarry Dec8 Dec8 x = SuccAsc x
+type instance AddCarry Dec8 Dec9 x = SuccAsc x
+
+type instance AddCarry Dec9 Dec0 x = Id x
+type instance AddCarry Dec9 Dec1 x = SuccAsc x
+type instance AddCarry Dec9 Dec2 x = SuccAsc x
+type instance AddCarry Dec9 Dec3 x = SuccAsc x
+type instance AddCarry Dec9 Dec4 x = SuccAsc x
+type instance AddCarry Dec9 Dec5 x = SuccAsc x
+type instance AddCarry Dec9 Dec6 x = SuccAsc x
+type instance AddCarry Dec9 Dec7 x = SuccAsc x
+type instance AddCarry Dec9 Dec8 x = SuccAsc x
+type instance AddCarry Dec9 Dec9 x = SuccAsc x
+
+type family AddAsc x y
+type instance AddAsc EndAsc y = y
+type instance AddAsc (xh :< xl) EndAsc = xh :< xl
+type instance AddAsc (xh :< xl) (yh :< yl) =
+        AddCarry xl yl (AddAsc xh yh) :< AddDigit xl yl
+
+type AddPos x xs y ys =
+        NormalizePosDesc
+           (AddAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys))
+
+-- type family x Op.:+: y
+type instance Dec x Op.:+: Dec y = Dec (x :+: y)
+
+type family x :+: y
+type instance (Zero    ) :+: y          = y
+type instance (Pos x xs) :+: (Zero    ) = Pos x xs
+type instance (Neg x xs) :+: (Zero    ) = Neg x xs
+type instance (Pos x xs) :+: (Pos y ys) = AddPos x xs y ys
+type instance (Neg x xs) :+: (Neg y ys) = Negate (AddPos x xs y ys)
+type instance (Pos x xs) :+: (Neg y ys) = SubPos x xs y ys
+type instance (Neg x xs) :+: (Pos y ys) = SubPos y ys x xs
+
+--------------------
+-- Subtraction
+
+type family SubDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance SubDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x-y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance SubDigit Dec0 Dec0 = Dec0
+type instance SubDigit Dec0 Dec1 = Dec9
+type instance SubDigit Dec0 Dec2 = Dec8
+type instance SubDigit Dec0 Dec3 = Dec7
+type instance SubDigit Dec0 Dec4 = Dec6
+type instance SubDigit Dec0 Dec5 = Dec5
+type instance SubDigit Dec0 Dec6 = Dec4
+type instance SubDigit Dec0 Dec7 = Dec3
+type instance SubDigit Dec0 Dec8 = Dec2
+type instance SubDigit Dec0 Dec9 = Dec1
+
+type instance SubDigit Dec1 Dec0 = Dec1
+type instance SubDigit Dec1 Dec1 = Dec0
+type instance SubDigit Dec1 Dec2 = Dec9
+type instance SubDigit Dec1 Dec3 = Dec8
+type instance SubDigit Dec1 Dec4 = Dec7
+type instance SubDigit Dec1 Dec5 = Dec6
+type instance SubDigit Dec1 Dec6 = Dec5
+type instance SubDigit Dec1 Dec7 = Dec4
+type instance SubDigit Dec1 Dec8 = Dec3
+type instance SubDigit Dec1 Dec9 = Dec2
+
+type instance SubDigit Dec2 Dec0 = Dec2
+type instance SubDigit Dec2 Dec1 = Dec1
+type instance SubDigit Dec2 Dec2 = Dec0
+type instance SubDigit Dec2 Dec3 = Dec9
+type instance SubDigit Dec2 Dec4 = Dec8
+type instance SubDigit Dec2 Dec5 = Dec7
+type instance SubDigit Dec2 Dec6 = Dec6
+type instance SubDigit Dec2 Dec7 = Dec5
+type instance SubDigit Dec2 Dec8 = Dec4
+type instance SubDigit Dec2 Dec9 = Dec3
+
+type instance SubDigit Dec3 Dec0 = Dec3
+type instance SubDigit Dec3 Dec1 = Dec2
+type instance SubDigit Dec3 Dec2 = Dec1
+type instance SubDigit Dec3 Dec3 = Dec0
+type instance SubDigit Dec3 Dec4 = Dec9
+type instance SubDigit Dec3 Dec5 = Dec8
+type instance SubDigit Dec3 Dec6 = Dec7
+type instance SubDigit Dec3 Dec7 = Dec6
+type instance SubDigit Dec3 Dec8 = Dec5
+type instance SubDigit Dec3 Dec9 = Dec4
+
+type instance SubDigit Dec4 Dec0 = Dec4
+type instance SubDigit Dec4 Dec1 = Dec3
+type instance SubDigit Dec4 Dec2 = Dec2
+type instance SubDigit Dec4 Dec3 = Dec1
+type instance SubDigit Dec4 Dec4 = Dec0
+type instance SubDigit Dec4 Dec5 = Dec9
+type instance SubDigit Dec4 Dec6 = Dec8
+type instance SubDigit Dec4 Dec7 = Dec7
+type instance SubDigit Dec4 Dec8 = Dec6
+type instance SubDigit Dec4 Dec9 = Dec5
+
+type instance SubDigit Dec5 Dec0 = Dec5
+type instance SubDigit Dec5 Dec1 = Dec4
+type instance SubDigit Dec5 Dec2 = Dec3
+type instance SubDigit Dec5 Dec3 = Dec2
+type instance SubDigit Dec5 Dec4 = Dec1
+type instance SubDigit Dec5 Dec5 = Dec0
+type instance SubDigit Dec5 Dec6 = Dec9
+type instance SubDigit Dec5 Dec7 = Dec8
+type instance SubDigit Dec5 Dec8 = Dec7
+type instance SubDigit Dec5 Dec9 = Dec6
+
+type instance SubDigit Dec6 Dec0 = Dec6
+type instance SubDigit Dec6 Dec1 = Dec5
+type instance SubDigit Dec6 Dec2 = Dec4
+type instance SubDigit Dec6 Dec3 = Dec3
+type instance SubDigit Dec6 Dec4 = Dec2
+type instance SubDigit Dec6 Dec5 = Dec1
+type instance SubDigit Dec6 Dec6 = Dec0
+type instance SubDigit Dec6 Dec7 = Dec9
+type instance SubDigit Dec6 Dec8 = Dec8
+type instance SubDigit Dec6 Dec9 = Dec7
+
+type instance SubDigit Dec7 Dec0 = Dec7
+type instance SubDigit Dec7 Dec1 = Dec6
+type instance SubDigit Dec7 Dec2 = Dec5
+type instance SubDigit Dec7 Dec3 = Dec4
+type instance SubDigit Dec7 Dec4 = Dec3
+type instance SubDigit Dec7 Dec5 = Dec2
+type instance SubDigit Dec7 Dec6 = Dec1
+type instance SubDigit Dec7 Dec7 = Dec0
+type instance SubDigit Dec7 Dec8 = Dec9
+type instance SubDigit Dec7 Dec9 = Dec8
+
+type instance SubDigit Dec8 Dec0 = Dec8
+type instance SubDigit Dec8 Dec1 = Dec7
+type instance SubDigit Dec8 Dec2 = Dec6
+type instance SubDigit Dec8 Dec3 = Dec5
+type instance SubDigit Dec8 Dec4 = Dec4
+type instance SubDigit Dec8 Dec5 = Dec3
+type instance SubDigit Dec8 Dec6 = Dec2
+type instance SubDigit Dec8 Dec7 = Dec1
+type instance SubDigit Dec8 Dec8 = Dec0
+type instance SubDigit Dec8 Dec9 = Dec9
+
+type instance SubDigit Dec9 Dec0 = Dec9
+type instance SubDigit Dec9 Dec1 = Dec8
+type instance SubDigit Dec9 Dec2 = Dec7
+type instance SubDigit Dec9 Dec3 = Dec6
+type instance SubDigit Dec9 Dec4 = Dec5
+type instance SubDigit Dec9 Dec5 = Dec4
+type instance SubDigit Dec9 Dec6 = Dec3
+type instance SubDigit Dec9 Dec7 = Dec2
+type instance SubDigit Dec9 Dec8 = Dec1
+type instance SubDigit Dec9 Dec9 = Dec0
+
+-- | If subtracting @y@ from @x@ would not borrow, then
+--   @Borrow x y z@ evaluates to @z@.  Otherwise,
+--   @Borrow x y z@ evaluates to @PredAsc z@
+type family Borrow x y z
+-- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "PredAsc" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance Borrow Dec0 Dec0 x = Id x
+type instance Borrow Dec0 Dec1 x = PredAsc x
+type instance Borrow Dec0 Dec2 x = PredAsc x
+type instance Borrow Dec0 Dec3 x = PredAsc x
+type instance Borrow Dec0 Dec4 x = PredAsc x
+type instance Borrow Dec0 Dec5 x = PredAsc x
+type instance Borrow Dec0 Dec6 x = PredAsc x
+type instance Borrow Dec0 Dec7 x = PredAsc x
+type instance Borrow Dec0 Dec8 x = PredAsc x
+type instance Borrow Dec0 Dec9 x = PredAsc x
+
+type instance Borrow Dec1 Dec0 x = Id x
+type instance Borrow Dec1 Dec1 x = Id x
+type instance Borrow Dec1 Dec2 x = PredAsc x
+type instance Borrow Dec1 Dec3 x = PredAsc x
+type instance Borrow Dec1 Dec4 x = PredAsc x
+type instance Borrow Dec1 Dec5 x = PredAsc x
+type instance Borrow Dec1 Dec6 x = PredAsc x
+type instance Borrow Dec1 Dec7 x = PredAsc x
+type instance Borrow Dec1 Dec8 x = PredAsc x
+type instance Borrow Dec1 Dec9 x = PredAsc x
+
+type instance Borrow Dec2 Dec0 x = Id x
+type instance Borrow Dec2 Dec1 x = Id x
+type instance Borrow Dec2 Dec2 x = Id x
+type instance Borrow Dec2 Dec3 x = PredAsc x
+type instance Borrow Dec2 Dec4 x = PredAsc x
+type instance Borrow Dec2 Dec5 x = PredAsc x
+type instance Borrow Dec2 Dec6 x = PredAsc x
+type instance Borrow Dec2 Dec7 x = PredAsc x
+type instance Borrow Dec2 Dec8 x = PredAsc x
+type instance Borrow Dec2 Dec9 x = PredAsc x
+
+type instance Borrow Dec3 Dec0 x = Id x
+type instance Borrow Dec3 Dec1 x = Id x
+type instance Borrow Dec3 Dec2 x = Id x
+type instance Borrow Dec3 Dec3 x = Id x
+type instance Borrow Dec3 Dec4 x = PredAsc x
+type instance Borrow Dec3 Dec5 x = PredAsc x
+type instance Borrow Dec3 Dec6 x = PredAsc x
+type instance Borrow Dec3 Dec7 x = PredAsc x
+type instance Borrow Dec3 Dec8 x = PredAsc x
+type instance Borrow Dec3 Dec9 x = PredAsc x
+
+type instance Borrow Dec4 Dec0 x = Id x
+type instance Borrow Dec4 Dec1 x = Id x
+type instance Borrow Dec4 Dec2 x = Id x
+type instance Borrow Dec4 Dec3 x = Id x
+type instance Borrow Dec4 Dec4 x = Id x
+type instance Borrow Dec4 Dec5 x = PredAsc x
+type instance Borrow Dec4 Dec6 x = PredAsc x
+type instance Borrow Dec4 Dec7 x = PredAsc x
+type instance Borrow Dec4 Dec8 x = PredAsc x
+type instance Borrow Dec4 Dec9 x = PredAsc x
+
+type instance Borrow Dec5 Dec0 x = Id x
+type instance Borrow Dec5 Dec1 x = Id x
+type instance Borrow Dec5 Dec2 x = Id x
+type instance Borrow Dec5 Dec3 x = Id x
+type instance Borrow Dec5 Dec4 x = Id x
+type instance Borrow Dec5 Dec5 x = Id x
+type instance Borrow Dec5 Dec6 x = PredAsc x
+type instance Borrow Dec5 Dec7 x = PredAsc x
+type instance Borrow Dec5 Dec8 x = PredAsc x
+type instance Borrow Dec5 Dec9 x = PredAsc x
+
+type instance Borrow Dec6 Dec0 x = Id x
+type instance Borrow Dec6 Dec1 x = Id x
+type instance Borrow Dec6 Dec2 x = Id x
+type instance Borrow Dec6 Dec3 x = Id x
+type instance Borrow Dec6 Dec4 x = Id x
+type instance Borrow Dec6 Dec5 x = Id x
+type instance Borrow Dec6 Dec6 x = Id x
+type instance Borrow Dec6 Dec7 x = PredAsc x
+type instance Borrow Dec6 Dec8 x = PredAsc x
+type instance Borrow Dec6 Dec9 x = PredAsc x
+
+type instance Borrow Dec7 Dec0 x = Id x
+type instance Borrow Dec7 Dec1 x = Id x
+type instance Borrow Dec7 Dec2 x = Id x
+type instance Borrow Dec7 Dec3 x = Id x
+type instance Borrow Dec7 Dec4 x = Id x
+type instance Borrow Dec7 Dec5 x = Id x
+type instance Borrow Dec7 Dec6 x = Id x
+type instance Borrow Dec7 Dec7 x = Id x
+type instance Borrow Dec7 Dec8 x = PredAsc x
+type instance Borrow Dec7 Dec9 x = PredAsc x
+
+type instance Borrow Dec8 Dec0 x = Id x
+type instance Borrow Dec8 Dec1 x = Id x
+type instance Borrow Dec8 Dec2 x = Id x
+type instance Borrow Dec8 Dec3 x = Id x
+type instance Borrow Dec8 Dec4 x = Id x
+type instance Borrow Dec8 Dec5 x = Id x
+type instance Borrow Dec8 Dec6 x = Id x
+type instance Borrow Dec8 Dec7 x = Id x
+type instance Borrow Dec8 Dec8 x = Id x
+type instance Borrow Dec8 Dec9 x = PredAsc x
+
+type instance Borrow Dec9 Dec0 x = Id x
+type instance Borrow Dec9 Dec1 x = Id x
+type instance Borrow Dec9 Dec2 x = Id x
+type instance Borrow Dec9 Dec3 x = Id x
+type instance Borrow Dec9 Dec4 x = Id x
+type instance Borrow Dec9 Dec5 x = Id x
+type instance Borrow Dec9 Dec6 x = Id x
+type instance Borrow Dec9 Dec7 x = Id x
+type instance Borrow Dec9 Dec8 x = Id x
+type instance Borrow Dec9 Dec9 x = Id x
+
+type family SubAsc x y
+type instance SubAsc x EndAsc = x
+type instance SubAsc (xh :< xl) (yh :< yl) =
+        SubAsc (Borrow xl yl xh) yh :< SubDigit xl yl
+
+type family SubOrd c x y
+type instance SubOrd GT  x  y = NormalizePosDesc (SubAsc x y)
+type instance SubOrd EQ _x _y = Zero
+type instance SubOrd LT  x  y = NormalizeNegDesc (SubAsc y x)
+
+type SubCmp x y = SubOrd (CompareAsc x y EQ) x y
+
+type SubPos x xs y ys =
+        SubCmp (AscendingNonEmpty x xs) (AscendingNonEmpty y ys)
+
+
+-- type family x Op.:-: y
+type instance Dec x Op.:-: Dec y = Dec (x :-: y)
+
+type x :-: y = x :+: Negate y
+
+
+--------------------
+-- Multiplication
+
+-- type family Mul2 x
+type instance Op.Mul2 (Dec x) = Dec (x :+: x)
+type Mul2Asc x = AddAsc x x
+
+-- type family x Op.:*: y
+type instance (Dec x) Op.:*: (Dec y) = Dec (x :*: y)
+
+type family x :*: y
+type instance Zero         :*: _y   = Zero
+type instance (Pos _x _xs) :*: Zero = Zero
+type instance (Neg _x _xs) :*: Zero = Zero
+type instance (Pos x xs) :*: (Pos y ys) = NormalizePosDesc (MulPos x xs y ys)
+type instance (Neg x xs) :*: (Neg y ys) = NormalizePosDesc (MulPos x xs y ys)
+type instance (Pos x xs) :*: (Neg y ys) = NormalizeNegDesc (MulPos x xs y ys)
+type instance (Neg x xs) :*: (Pos y ys) = NormalizeNegDesc (MulPos x xs y ys)
+
+type MulPos x xs y ys =
+        MulScaleAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys)
+
+{-
+type MulPos x xs y ys =
+        MulAsc (AscendingNonEmpty x xs) (Pos y ys) EndAsc
+-}
+
+type family MulAsc x y z
+type instance MulAsc _x Zero       z = z
+type instance MulAsc  x (Pos y ys) z =
+         MulAsc (Mul2Asc x) (Div2 (Pos y ys))
+            (If (IsEven (Pos y ys)) z (AddAsc z x))
+
+
+
+-----------
+-- Scale
+
+type family MulLo x y
+-- putStr $ unlines $ concat $ [ [ "type instance MulLo Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x*y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+
+type instance MulLo Dec0 Dec0 = Dec0
+type instance MulLo Dec0 Dec1 = Dec0
+type instance MulLo Dec0 Dec2 = Dec0
+type instance MulLo Dec0 Dec3 = Dec0
+type instance MulLo Dec0 Dec4 = Dec0
+type instance MulLo Dec0 Dec5 = Dec0
+type instance MulLo Dec0 Dec6 = Dec0
+type instance MulLo Dec0 Dec7 = Dec0
+type instance MulLo Dec0 Dec8 = Dec0
+type instance MulLo Dec0 Dec9 = Dec0
+
+type instance MulLo Dec1 Dec0 = Dec0
+type instance MulLo Dec1 Dec1 = Dec1
+type instance MulLo Dec1 Dec2 = Dec2
+type instance MulLo Dec1 Dec3 = Dec3
+type instance MulLo Dec1 Dec4 = Dec4
+type instance MulLo Dec1 Dec5 = Dec5
+type instance MulLo Dec1 Dec6 = Dec6
+type instance MulLo Dec1 Dec7 = Dec7
+type instance MulLo Dec1 Dec8 = Dec8
+type instance MulLo Dec1 Dec9 = Dec9
+
+type instance MulLo Dec2 Dec0 = Dec0
+type instance MulLo Dec2 Dec1 = Dec2
+type instance MulLo Dec2 Dec2 = Dec4
+type instance MulLo Dec2 Dec3 = Dec6
+type instance MulLo Dec2 Dec4 = Dec8
+type instance MulLo Dec2 Dec5 = Dec0
+type instance MulLo Dec2 Dec6 = Dec2
+type instance MulLo Dec2 Dec7 = Dec4
+type instance MulLo Dec2 Dec8 = Dec6
+type instance MulLo Dec2 Dec9 = Dec8
+
+type instance MulLo Dec3 Dec0 = Dec0
+type instance MulLo Dec3 Dec1 = Dec3
+type instance MulLo Dec3 Dec2 = Dec6
+type instance MulLo Dec3 Dec3 = Dec9
+type instance MulLo Dec3 Dec4 = Dec2
+type instance MulLo Dec3 Dec5 = Dec5
+type instance MulLo Dec3 Dec6 = Dec8
+type instance MulLo Dec3 Dec7 = Dec1
+type instance MulLo Dec3 Dec8 = Dec4
+type instance MulLo Dec3 Dec9 = Dec7
+
+type instance MulLo Dec4 Dec0 = Dec0
+type instance MulLo Dec4 Dec1 = Dec4
+type instance MulLo Dec4 Dec2 = Dec8
+type instance MulLo Dec4 Dec3 = Dec2
+type instance MulLo Dec4 Dec4 = Dec6
+type instance MulLo Dec4 Dec5 = Dec0
+type instance MulLo Dec4 Dec6 = Dec4
+type instance MulLo Dec4 Dec7 = Dec8
+type instance MulLo Dec4 Dec8 = Dec2
+type instance MulLo Dec4 Dec9 = Dec6
+
+type instance MulLo Dec5 Dec0 = Dec0
+type instance MulLo Dec5 Dec1 = Dec5
+type instance MulLo Dec5 Dec2 = Dec0
+type instance MulLo Dec5 Dec3 = Dec5
+type instance MulLo Dec5 Dec4 = Dec0
+type instance MulLo Dec5 Dec5 = Dec5
+type instance MulLo Dec5 Dec6 = Dec0
+type instance MulLo Dec5 Dec7 = Dec5
+type instance MulLo Dec5 Dec8 = Dec0
+type instance MulLo Dec5 Dec9 = Dec5
+
+type instance MulLo Dec6 Dec0 = Dec0
+type instance MulLo Dec6 Dec1 = Dec6
+type instance MulLo Dec6 Dec2 = Dec2
+type instance MulLo Dec6 Dec3 = Dec8
+type instance MulLo Dec6 Dec4 = Dec4
+type instance MulLo Dec6 Dec5 = Dec0
+type instance MulLo Dec6 Dec6 = Dec6
+type instance MulLo Dec6 Dec7 = Dec2
+type instance MulLo Dec6 Dec8 = Dec8
+type instance MulLo Dec6 Dec9 = Dec4
+
+type instance MulLo Dec7 Dec0 = Dec0
+type instance MulLo Dec7 Dec1 = Dec7
+type instance MulLo Dec7 Dec2 = Dec4
+type instance MulLo Dec7 Dec3 = Dec1
+type instance MulLo Dec7 Dec4 = Dec8
+type instance MulLo Dec7 Dec5 = Dec5
+type instance MulLo Dec7 Dec6 = Dec2
+type instance MulLo Dec7 Dec7 = Dec9
+type instance MulLo Dec7 Dec8 = Dec6
+type instance MulLo Dec7 Dec9 = Dec3
+
+type instance MulLo Dec8 Dec0 = Dec0
+type instance MulLo Dec8 Dec1 = Dec8
+type instance MulLo Dec8 Dec2 = Dec6
+type instance MulLo Dec8 Dec3 = Dec4
+type instance MulLo Dec8 Dec4 = Dec2
+type instance MulLo Dec8 Dec5 = Dec0
+type instance MulLo Dec8 Dec6 = Dec8
+type instance MulLo Dec8 Dec7 = Dec6
+type instance MulLo Dec8 Dec8 = Dec4
+type instance MulLo Dec8 Dec9 = Dec2
+
+type instance MulLo Dec9 Dec0 = Dec0
+type instance MulLo Dec9 Dec1 = Dec9
+type instance MulLo Dec9 Dec2 = Dec8
+type instance MulLo Dec9 Dec3 = Dec7
+type instance MulLo Dec9 Dec4 = Dec6
+type instance MulLo Dec9 Dec5 = Dec5
+type instance MulLo Dec9 Dec6 = Dec4
+type instance MulLo Dec9 Dec7 = Dec3
+type instance MulLo Dec9 Dec8 = Dec2
+type instance MulLo Dec9 Dec9 = Dec1
+
+
+type family MulHi x y
+-- putStr $ unlines $ concat $ [ [ "type instance MulHi Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x*y) `div` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+
+type instance MulHi Dec0 Dec0 = Dec0
+type instance MulHi Dec0 Dec1 = Dec0
+type instance MulHi Dec0 Dec2 = Dec0
+type instance MulHi Dec0 Dec3 = Dec0
+type instance MulHi Dec0 Dec4 = Dec0
+type instance MulHi Dec0 Dec5 = Dec0
+type instance MulHi Dec0 Dec6 = Dec0
+type instance MulHi Dec0 Dec7 = Dec0
+type instance MulHi Dec0 Dec8 = Dec0
+type instance MulHi Dec0 Dec9 = Dec0
+
+type instance MulHi Dec1 Dec0 = Dec0
+type instance MulHi Dec1 Dec1 = Dec0
+type instance MulHi Dec1 Dec2 = Dec0
+type instance MulHi Dec1 Dec3 = Dec0
+type instance MulHi Dec1 Dec4 = Dec0
+type instance MulHi Dec1 Dec5 = Dec0
+type instance MulHi Dec1 Dec6 = Dec0
+type instance MulHi Dec1 Dec7 = Dec0
+type instance MulHi Dec1 Dec8 = Dec0
+type instance MulHi Dec1 Dec9 = Dec0
+
+type instance MulHi Dec2 Dec0 = Dec0
+type instance MulHi Dec2 Dec1 = Dec0
+type instance MulHi Dec2 Dec2 = Dec0
+type instance MulHi Dec2 Dec3 = Dec0
+type instance MulHi Dec2 Dec4 = Dec0
+type instance MulHi Dec2 Dec5 = Dec1
+type instance MulHi Dec2 Dec6 = Dec1
+type instance MulHi Dec2 Dec7 = Dec1
+type instance MulHi Dec2 Dec8 = Dec1
+type instance MulHi Dec2 Dec9 = Dec1
+
+type instance MulHi Dec3 Dec0 = Dec0
+type instance MulHi Dec3 Dec1 = Dec0
+type instance MulHi Dec3 Dec2 = Dec0
+type instance MulHi Dec3 Dec3 = Dec0
+type instance MulHi Dec3 Dec4 = Dec1
+type instance MulHi Dec3 Dec5 = Dec1
+type instance MulHi Dec3 Dec6 = Dec1
+type instance MulHi Dec3 Dec7 = Dec2
+type instance MulHi Dec3 Dec8 = Dec2
+type instance MulHi Dec3 Dec9 = Dec2
+
+type instance MulHi Dec4 Dec0 = Dec0
+type instance MulHi Dec4 Dec1 = Dec0
+type instance MulHi Dec4 Dec2 = Dec0
+type instance MulHi Dec4 Dec3 = Dec1
+type instance MulHi Dec4 Dec4 = Dec1
+type instance MulHi Dec4 Dec5 = Dec2
+type instance MulHi Dec4 Dec6 = Dec2
+type instance MulHi Dec4 Dec7 = Dec2
+type instance MulHi Dec4 Dec8 = Dec3
+type instance MulHi Dec4 Dec9 = Dec3
+
+type instance MulHi Dec5 Dec0 = Dec0
+type instance MulHi Dec5 Dec1 = Dec0
+type instance MulHi Dec5 Dec2 = Dec1
+type instance MulHi Dec5 Dec3 = Dec1
+type instance MulHi Dec5 Dec4 = Dec2
+type instance MulHi Dec5 Dec5 = Dec2
+type instance MulHi Dec5 Dec6 = Dec3
+type instance MulHi Dec5 Dec7 = Dec3
+type instance MulHi Dec5 Dec8 = Dec4
+type instance MulHi Dec5 Dec9 = Dec4
+
+type instance MulHi Dec6 Dec0 = Dec0
+type instance MulHi Dec6 Dec1 = Dec0
+type instance MulHi Dec6 Dec2 = Dec1
+type instance MulHi Dec6 Dec3 = Dec1
+type instance MulHi Dec6 Dec4 = Dec2
+type instance MulHi Dec6 Dec5 = Dec3
+type instance MulHi Dec6 Dec6 = Dec3
+type instance MulHi Dec6 Dec7 = Dec4
+type instance MulHi Dec6 Dec8 = Dec4
+type instance MulHi Dec6 Dec9 = Dec5
+
+type instance MulHi Dec7 Dec0 = Dec0
+type instance MulHi Dec7 Dec1 = Dec0
+type instance MulHi Dec7 Dec2 = Dec1
+type instance MulHi Dec7 Dec3 = Dec2
+type instance MulHi Dec7 Dec4 = Dec2
+type instance MulHi Dec7 Dec5 = Dec3
+type instance MulHi Dec7 Dec6 = Dec4
+type instance MulHi Dec7 Dec7 = Dec4
+type instance MulHi Dec7 Dec8 = Dec5
+type instance MulHi Dec7 Dec9 = Dec6
+
+type instance MulHi Dec8 Dec0 = Dec0
+type instance MulHi Dec8 Dec1 = Dec0
+type instance MulHi Dec8 Dec2 = Dec1
+type instance MulHi Dec8 Dec3 = Dec2
+type instance MulHi Dec8 Dec4 = Dec3
+type instance MulHi Dec8 Dec5 = Dec4
+type instance MulHi Dec8 Dec6 = Dec4
+type instance MulHi Dec8 Dec7 = Dec5
+type instance MulHi Dec8 Dec8 = Dec6
+type instance MulHi Dec8 Dec9 = Dec7
+
+type instance MulHi Dec9 Dec0 = Dec0
+type instance MulHi Dec9 Dec1 = Dec0
+type instance MulHi Dec9 Dec2 = Dec1
+type instance MulHi Dec9 Dec3 = Dec2
+type instance MulHi Dec9 Dec4 = Dec3
+type instance MulHi Dec9 Dec5 = Dec4
+type instance MulHi Dec9 Dec6 = Dec5
+type instance MulHi Dec9 Dec7 = Dec6
+type instance MulHi Dec9 Dec8 = Dec7
+type instance MulHi Dec9 Dec9 = Dec8
+
+
+type family ScaleLo x ys
+type instance ScaleLo _x EndAsc = EndAsc
+type instance ScaleLo  x (yh :< yl) = ScaleLo x yh :< MulLo x yl
+
+type family ScaleHi x ys
+type instance ScaleHi _x EndAsc = EndAsc
+type instance ScaleHi  x (yh :< yl) = ScaleHi x yh :< MulHi x yl
+
+type family MulScaleAsc xs ys
+type instance MulScaleAsc EndAsc _ys = EndAsc
+type instance MulScaleAsc (xh :< xl) ys =
+         AddAsc
+            (ScaleLo xl ys)
+            (AddAsc (MulScaleAsc xh ys) (ScaleHi xl ys) :< Dec0)
+
+
+-----------
+-- Division / Modulus
+
+-- type family Op.IsEven x
+type instance Op.IsEven (Dec x) = IsEven x
+
+type family IsEven x
+type instance IsEven Zero = True
+type instance IsEven (Neg x xs) = IsEvenAsc (AscendingNonEmpty x xs)
+type instance IsEven (Pos x xs) = IsEvenAsc (AscendingNonEmpty x xs)
+
+type family IsEvenAsc x
+type instance IsEvenAsc EndAsc = True
+type instance IsEvenAsc (_xh :< xl) = IsEvenDigit xl
+
+type family IsEvenDigit x
+type instance IsEvenDigit Dec0 = True
+type instance IsEvenDigit Dec1 = False
+type instance IsEvenDigit Dec2 = True
+type instance IsEvenDigit Dec3 = False
+type instance IsEvenDigit Dec4 = True
+type instance IsEvenDigit Dec5 = False
+type instance IsEvenDigit Dec6 = True
+type instance IsEvenDigit Dec7 = False
+type instance IsEvenDigit Dec8 = True
+type instance IsEvenDigit Dec9 = False
+
+-- type family Op.Div2 x
+type instance Op.Div2 (Dec x) = Dec (Div2 x)
+
+type family Div2 x
+type instance Div2 Zero = Zero
+type instance Div2 (Neg x xs) =
+        NormalizeNegDesc (Div2Asc (AscendingNonEmpty x xs))
+type instance Div2 (Pos x xs) =
+        NormalizePosDesc (Div2Asc (AscendingNonEmpty x xs))
+
+type family Div2Digit x
+type instance Div2Digit Dec0 = Dec0
+type instance Div2Digit Dec1 = Dec0
+type instance Div2Digit Dec2 = Dec1
+type instance Div2Digit Dec3 = Dec1
+type instance Div2Digit Dec4 = Dec2
+type instance Div2Digit Dec5 = Dec2
+type instance Div2Digit Dec6 = Dec3
+type instance Div2Digit Dec7 = Dec3
+type instance Div2Digit Dec8 = Dec4
+type instance Div2Digit Dec9 = Dec4
+
+type family Div2Asc x
+type instance Div2Asc EndAsc = EndAsc
+type instance Div2Asc (xh :< xl) =
+        Div2Pos xh (Div2Digit xl) (If (IsEvenAsc xh) Dec0 Dec5)
+
+type Div2Pos xh xl rem =
+        AddCarry xl rem (Div2Asc xh) :< AddDigit xl rem
+
+---------------
+-- Exponentiation
+
+type instance Op.Pow2 (Dec x) = Dec (Pow2 x)
+
+type family Pow2 x
+type instance Pow2 Zero = One
+type instance Pow2 (Pos x xs) =
+        NormalizePosDesc (Pow2Asc (Pos x xs) (EndAsc :< Dec1))
+
+type family Pow2Asc x y
+type instance Pow2Asc Zero y = y
+type instance Pow2Asc (Pos x xs) y =
+        Pow2Asc (Pred (Pos x xs)) (Mul2Asc y)
+
+---------------
+-- Logarithm
+type instance Op.Log2Ceil (Dec x) = Dec (Log2Ceil x)
+
+type family Log2Ceil x
+type instance Log2Ceil (Pos x xs) =
+        NormalizePosDesc (Log2C (Pred (Pos x xs)) EndAsc)
+
+type family Log2C x y
+type instance Log2C Zero y = y
+type instance Log2C (Pos x xs) y = Log2C (Div2 (Pos x xs)) (SuccAsc y)
+
+---------------
+-- Comparison
+
+type family CompareDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance CompareDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = " ++ (if x < y then "LT" else (if x > y then "GT" else "EQ")) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance CompareDigit Dec0 Dec0 = EQ
+type instance CompareDigit Dec0 Dec1 = LT
+type instance CompareDigit Dec0 Dec2 = LT
+type instance CompareDigit Dec0 Dec3 = LT
+type instance CompareDigit Dec0 Dec4 = LT
+type instance CompareDigit Dec0 Dec5 = LT
+type instance CompareDigit Dec0 Dec6 = LT
+type instance CompareDigit Dec0 Dec7 = LT
+type instance CompareDigit Dec0 Dec8 = LT
+type instance CompareDigit Dec0 Dec9 = LT
+
+type instance CompareDigit Dec1 Dec0 = GT
+type instance CompareDigit Dec1 Dec1 = EQ
+type instance CompareDigit Dec1 Dec2 = LT
+type instance CompareDigit Dec1 Dec3 = LT
+type instance CompareDigit Dec1 Dec4 = LT
+type instance CompareDigit Dec1 Dec5 = LT
+type instance CompareDigit Dec1 Dec6 = LT
+type instance CompareDigit Dec1 Dec7 = LT
+type instance CompareDigit Dec1 Dec8 = LT
+type instance CompareDigit Dec1 Dec9 = LT
+
+type instance CompareDigit Dec2 Dec0 = GT
+type instance CompareDigit Dec2 Dec1 = GT
+type instance CompareDigit Dec2 Dec2 = EQ
+type instance CompareDigit Dec2 Dec3 = LT
+type instance CompareDigit Dec2 Dec4 = LT
+type instance CompareDigit Dec2 Dec5 = LT
+type instance CompareDigit Dec2 Dec6 = LT
+type instance CompareDigit Dec2 Dec7 = LT
+type instance CompareDigit Dec2 Dec8 = LT
+type instance CompareDigit Dec2 Dec9 = LT
+
+type instance CompareDigit Dec3 Dec0 = GT
+type instance CompareDigit Dec3 Dec1 = GT
+type instance CompareDigit Dec3 Dec2 = GT
+type instance CompareDigit Dec3 Dec3 = EQ
+type instance CompareDigit Dec3 Dec4 = LT
+type instance CompareDigit Dec3 Dec5 = LT
+type instance CompareDigit Dec3 Dec6 = LT
+type instance CompareDigit Dec3 Dec7 = LT
+type instance CompareDigit Dec3 Dec8 = LT
+type instance CompareDigit Dec3 Dec9 = LT
+
+type instance CompareDigit Dec4 Dec0 = GT
+type instance CompareDigit Dec4 Dec1 = GT
+type instance CompareDigit Dec4 Dec2 = GT
+type instance CompareDigit Dec4 Dec3 = GT
+type instance CompareDigit Dec4 Dec4 = EQ
+type instance CompareDigit Dec4 Dec5 = LT
+type instance CompareDigit Dec4 Dec6 = LT
+type instance CompareDigit Dec4 Dec7 = LT
+type instance CompareDigit Dec4 Dec8 = LT
+type instance CompareDigit Dec4 Dec9 = LT
+
+type instance CompareDigit Dec5 Dec0 = GT
+type instance CompareDigit Dec5 Dec1 = GT
+type instance CompareDigit Dec5 Dec2 = GT
+type instance CompareDigit Dec5 Dec3 = GT
+type instance CompareDigit Dec5 Dec4 = GT
+type instance CompareDigit Dec5 Dec5 = EQ
+type instance CompareDigit Dec5 Dec6 = LT
+type instance CompareDigit Dec5 Dec7 = LT
+type instance CompareDigit Dec5 Dec8 = LT
+type instance CompareDigit Dec5 Dec9 = LT
+
+type instance CompareDigit Dec6 Dec0 = GT
+type instance CompareDigit Dec6 Dec1 = GT
+type instance CompareDigit Dec6 Dec2 = GT
+type instance CompareDigit Dec6 Dec3 = GT
+type instance CompareDigit Dec6 Dec4 = GT
+type instance CompareDigit Dec6 Dec5 = GT
+type instance CompareDigit Dec6 Dec6 = EQ
+type instance CompareDigit Dec6 Dec7 = LT
+type instance CompareDigit Dec6 Dec8 = LT
+type instance CompareDigit Dec6 Dec9 = LT
+
+type instance CompareDigit Dec7 Dec0 = GT
+type instance CompareDigit Dec7 Dec1 = GT
+type instance CompareDigit Dec7 Dec2 = GT
+type instance CompareDigit Dec7 Dec3 = GT
+type instance CompareDigit Dec7 Dec4 = GT
+type instance CompareDigit Dec7 Dec5 = GT
+type instance CompareDigit Dec7 Dec6 = GT
+type instance CompareDigit Dec7 Dec7 = EQ
+type instance CompareDigit Dec7 Dec8 = LT
+type instance CompareDigit Dec7 Dec9 = LT
+
+type instance CompareDigit Dec8 Dec0 = GT
+type instance CompareDigit Dec8 Dec1 = GT
+type instance CompareDigit Dec8 Dec2 = GT
+type instance CompareDigit Dec8 Dec3 = GT
+type instance CompareDigit Dec8 Dec4 = GT
+type instance CompareDigit Dec8 Dec5 = GT
+type instance CompareDigit Dec8 Dec6 = GT
+type instance CompareDigit Dec8 Dec7 = GT
+type instance CompareDigit Dec8 Dec8 = EQ
+type instance CompareDigit Dec8 Dec9 = LT
+
+type instance CompareDigit Dec9 Dec0 = GT
+type instance CompareDigit Dec9 Dec1 = GT
+type instance CompareDigit Dec9 Dec2 = GT
+type instance CompareDigit Dec9 Dec3 = GT
+type instance CompareDigit Dec9 Dec4 = GT
+type instance CompareDigit Dec9 Dec5 = GT
+type instance CompareDigit Dec9 Dec6 = GT
+type instance CompareDigit Dec9 Dec7 = GT
+type instance CompareDigit Dec9 Dec8 = GT
+type instance CompareDigit Dec9 Dec9 = EQ
+
+type instance Ord.Compare (Dec x) (Dec y) = Compare x y
+type family Compare x y
+type instance Compare (Pos  x  xs) (Pos  y  ys) = ComparePos x xs y ys
+type instance Compare (Neg  x  xs) (Neg  y  ys) = ComparePos y ys x xs
+type instance Compare (Pos _x _xs) (Neg _y _ys) = GT
+type instance Compare (Neg _x _xs) (Pos _y _ys) = LT
+type instance Compare (Pos _x _xs) (Zero      ) = GT
+type instance Compare (Neg _x _xs) (Zero      ) = LT
+type instance Compare (Zero      ) (Neg _y _ys) = GT
+type instance Compare (Zero      ) (Pos _y _ys) = LT
+type instance Compare (Zero      ) (Zero      ) = EQ
+
+type ComparePos x xs y ys =
+        CompareAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys) EQ
+
+type family CompareAsc x y c
+type instance CompareAsc EndAsc     EndAsc      c = c
+type instance CompareAsc EndAsc     (_h :< _l) _c = LT
+type instance CompareAsc (_h :< _l) EndAsc     _c = GT
+type instance CompareAsc (xh :< xl) (yh :< yl) GT =
+                 CompareDiff xh yh (CompareDigit xl yl) GT
+type instance CompareAsc (xh :< xl) (yh :< yl) EQ =
+                 CompareAsc xh yh (CompareDigit xl yl)
+type instance CompareAsc (xh :< xl) (yh :< yl) LT =
+                 CompareDiff xh yh (CompareDigit xl yl) LT
+
+type family CompareDiff x y c l
+type instance CompareDiff x y LT _c = CompareAsc x y LT
+type instance CompareDiff x y EQ  c = CompareAsc x y c
+type instance CompareDiff x y GT _c = CompareAsc x y GT
+
+
+class x :<:  y; instance (x Ord.:<:  y) => Dec x :<:  Dec y
+class x :<=: y; instance (x Ord.:<=: y) => Dec x :<=: Dec y
+class x :>=: y; instance (x Ord.:>=: y) => Dec x :>=: Dec y
+class x :>:  y; instance (x Ord.:>:  y) => Dec x :>:  Dec y
+class x :==: y; instance (x Ord.:==: y) => Dec x :==: Dec y
+class x :/=: y; instance (x Ord.:/=: y) => Dec x :/=: Dec y
+
+
+type GreaterPos x xs y ys = Ord.IsGT (ComparePos x xs y ys)
+
+instance Neg x xs :<: Zero
+instance Neg x xs :<: Pos y ys
+instance Zero     :<: Pos y ys
+
+instance (ComparePos x xs y ys ~ GT) => Neg x xs :<: Neg y ys
+instance (ComparePos x xs y ys ~ LT) => Pos x xs :<: Pos y ys
+
+
+instance Neg x xs :<=: Zero
+instance Neg x xs :<=: Pos y ys
+instance Zero     :<=: Zero
+instance Zero     :<=: Pos y ys
+
+instance (GreaterPos y ys x xs ~ False) => Neg x xs :<=: Neg y ys
+instance (GreaterPos x xs y ys ~ False) => Pos x xs :<=: Pos y ys
+
+
+instance Zero     :>: Neg y ys
+instance Pos x xs :>: Neg y ys
+instance Pos x xs :>: Zero
+
+instance (ComparePos x xs y ys ~ LT) => Neg x xs :>: Neg y ys
+instance (ComparePos x xs y ys ~ GT) => Pos x xs :>: Pos y ys
+
+
+instance Zero     :>=: Neg y ys
+instance Pos x xs :>=: Neg y ys
+instance Zero     :>=: Zero
+instance Pos x xs :>=: Zero
+
+instance (GreaterPos x xs y ys ~ False) => Neg x xs :>=: Neg y ys
+instance (GreaterPos y ys x xs ~ False) => Pos x xs :>=: Pos y ys
+
+
+instance Zero     :==: Zero
+
+instance (ComparePos x xs y ys ~ EQ) => Neg x xs :==: Neg y ys
+instance (ComparePos x xs y ys ~ EQ) => Pos x xs :==: Pos y ys
+
+
+instance Zero     :/=: Neg y ys
+instance Pos x xs :/=: Neg y ys
+instance Neg x xs :/=: Zero
+instance Pos x xs :/=: Zero
+instance Neg x xs :/=: Pos y ys
+instance Zero     :/=: Pos y ys
+
+instance (Ord.IsEQ (ComparePos x xs y ys) ~ False) => Neg x xs :/=: Neg y ys
+instance (Ord.IsEQ (ComparePos x xs y ys) ~ False) => Pos x xs :/=: Pos y ys
+
+
+type family FromUnary n
+type instance FromUnary Unary.Zero = Zero
+type instance FromUnary (Unary.Succ n) = Succ (FromUnary n)
+
+type family ToUnary n
+type instance ToUnary Zero = Unary.Zero
+type instance ToUnary (Pos x xs) = ToUnaryAcc (Digit.ToUnary x) xs
+
+type family ToUnaryAcc m n
+type instance ToUnaryAcc m EndDesc = m
+type instance ToUnaryAcc m (x :> xs) =
+                 ToUnaryAcc (UnaryAcc m x) xs
+
+type UnaryAcc m x = Digit.ToUnary x Unary.:+: (m Unary.:*: UnaryLit.U10)
diff --git a/src/Type/Data/Num/Decimal/Proof.hs b/src/Type/Data/Num/Decimal/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Decimal/Proof.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Type.Data.Num.Decimal.Proof (
+    Digits(Digits),
+    UnaryNat(UnaryNat), unaryNat,
+    UnaryPos(UnaryPos), unaryPos,
+    ) where
+
+import qualified Type.Data.Num.Decimal.Digit.Proof as DigitProof
+import qualified Type.Data.Num.Decimal.Digit as Digit
+import qualified Type.Data.Num.Decimal.Number as Dec
+import qualified Type.Data.Num.Unary.Literal as UnaryLit
+import qualified Type.Data.Num.Unary.Proof as UnaryProof
+import qualified Type.Data.Num.Unary as Unary
+
+import Type.Data.Num.Decimal.Number (Pos, (:>), Natural, Positive, )
+
+
+data UnaryNat n = Unary.Natural (Dec.ToUnary n) => UnaryNat
+
+unaryNat :: (Natural n) => UnaryNat n
+unaryNat = Dec.switchNat UnaryNat (unaryUnPos unaryPosPos)
+
+unaryUnPos :: UnaryPos n -> UnaryNat n
+unaryUnPos UnaryPos = UnaryNat
+
+
+data UnaryPos n = Unary.Positive (Dec.ToUnary n) => UnaryPos
+
+unaryPos :: (Positive n) => UnaryPos n
+unaryPos = Dec.switchPos unaryPosPos
+
+unaryPosPos :: (Digit.Pos x, Dec.Digits xs) => UnaryPos (Pos x xs)
+unaryPosPos =
+    withUnaryPosPos $ \x xs ->
+        case toUnaryAcc (digitUnaryPos x) xs of
+            UnaryProof.Pos -> UnaryPos
+
+
+withUnaryPosPos ::
+    (Digit.Pos x, Dec.Digits xs) =>
+    (DigitProof.UnaryPos x -> Digits xs ->
+     UnaryPos (Pos x xs)) ->
+    UnaryPos (Pos x xs)
+withUnaryPosPos f =
+    f DigitProof.unaryPos Digits
+
+digitUnaryPos ::
+    DigitProof.UnaryPos x -> UnaryProof.Pos (Digit.ToUnary x)
+digitUnaryPos DigitProof.UnaryPos = UnaryProof.Pos
+
+
+data Digits xs = (Dec.Digits xs) => Digits
+
+newtype
+    ToUnaryAcc m xs =
+        ToUnaryAcc {runToUnaryAcc ::
+            UnaryProof.Pos m -> Digits xs ->
+            UnaryProof.Pos (Dec.ToUnaryAcc m xs)}
+
+toUnaryAcc ::
+    UnaryProof.Pos m -> Digits xs ->
+    UnaryProof.Pos (Dec.ToUnaryAcc m xs)
+toUnaryAcc m y@Digits =
+    runToUnaryAcc
+        (Dec.switchDigits
+            (ToUnaryAcc $ \ UnaryProof.Pos _ -> UnaryProof.Pos)
+            (ToUnaryAcc $ \ acc xt ->
+                toUnaryAcc
+                    (unaryAcc acc (DigitProof.unaryNatImpl (headDigits xt))
+                        UnaryProof.Pos)
+                    (tailDigits xt)))
+        m y
+
+
+headDigits :: (Digit.C x) => Digits (x :> xs) -> DigitProof.Nat x
+headDigits Digits = DigitProof.Nat
+
+tailDigits :: Dec.Digits xs => Digits (x :> xs) -> Digits xs
+tailDigits Digits = Digits
+
+
+unaryAcc ::
+    UnaryProof.Pos m -> UnaryProof.Nat x -> UnaryProof.Pos UnaryLit.U10 ->
+    UnaryProof.Pos (x Unary.:+: (m Unary.:*: UnaryLit.U10))
+unaryAcc m x ten =
+    UnaryProof.addPosR x $ UnaryProof.mulPos m ten
diff --git a/src/Type/Data/Num/Unary.hs b/src/Type/Data/Num/Unary.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Unary.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GADTs #-}
+module Type.Data.Num.Unary (
+    Unary, unary, Un, Zero, Succ, zero, succ,
+    HeadSingleton(Zero, Succ), headSingleton,
+    Singleton(..), singleton, singletonFromProxy,
+    integerFromSingleton, integralFromSingleton,
+    integralFromProxy,
+    Natural(..), Positive(..),
+    (:+:), (:*:),
+    reifyNatural,
+    ) where
+
+import qualified Type.Data.Num as Num
+import qualified Type.Base.Proxy as Proxy
+import Type.Base.Proxy (Proxy(Proxy))
+
+import Text.Printf (printf)
+
+import Prelude hiding (succ)
+
+
+-- | Representation name for unary type level numbers.
+data Unary
+
+data Un x
+data Zero
+data Succ x
+{-
+Negative numbers could be represented by Pred
+but this would complicate our proofs.
+We would require that a number contains only Succ or Pred.
+Alternative:
+Int = Zero | Neg Nat | Pos Nat
+Nat = None | Succ Nat
+-}
+
+zero :: Proxy Zero
+zero = Proxy
+
+succ :: Proxy n -> Proxy (Succ n)
+succ Proxy = Proxy
+
+
+class Natural n where
+    switchNat ::
+        f Zero ->
+        (forall m. (Natural m) => f (Succ m)) ->
+        f n
+
+instance Natural Zero where switchNat x _ = x
+instance Natural n => Natural (Succ n) where switchNat _ x = x
+
+
+class (Natural n) => Positive n where
+    switchPos ::
+        (forall m. (Natural m) => f (Succ m)) ->
+        f n
+
+instance Natural n => Positive (Succ n) where switchPos x = x
+
+
+type family x :+: y
+type instance x :+: Zero = x
+type instance x :+: Succ y = Succ (x :+: y)
+
+type family x :*: y
+type instance _x :*: Zero = Zero
+type instance x :*: Succ y = x :+: (x :*: y)
+
+
+
+data HeadSingleton n where
+    Zero :: HeadSingleton Zero
+    Succ :: (Natural n) => HeadSingleton (Succ n)
+
+headSingleton :: (Natural n) => HeadSingleton n
+headSingleton = switchNat Zero Succ
+
+
+newtype Singleton n = Singleton Integer
+
+instance (Natural n) => Num.Integer (Un n) where
+    singleton = singletonToGeneric singleton
+    type Repr (Un n) = Unary
+
+singletonToGeneric :: Singleton n -> Num.Singleton (Un n)
+singletonToGeneric (Singleton n) = Num.Singleton n
+
+singleton :: (Natural n) => Singleton n
+singleton =
+    switchNat
+        (Singleton 0)
+        (succSingleton singleton)
+
+succSingleton ::
+    (Natural n) =>
+    Singleton n -> Singleton (Succ n)
+succSingleton (Singleton n) = Singleton $ n+1
+
+
+integerFromSingleton :: (Natural n) => Singleton n -> Integer
+integerFromSingleton (Singleton n) = n
+
+integralFromSingleton :: (Natural n, Num a) => Singleton n -> a
+integralFromSingleton = fromInteger . integerFromSingleton
+
+singletonFromProxy :: (Natural n) => Proxy n -> Singleton n
+singletonFromProxy Proxy = singleton
+
+integralFromProxy :: (Natural n, Num a) => Proxy n -> a
+integralFromProxy = integralFromSingleton . singletonFromProxy
+
+
+instance Num.Representation Unary where
+    reifyIntegral _ i k = reifyIntegral i (k . unary)
+
+unary :: Proxy n -> Proxy (Un n)
+unary Proxy = Proxy
+
+stripUn :: Proxy (Un n) -> Proxy n
+stripUn Proxy = Proxy
+
+reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
+reifyIntegral n f =
+    if n < 0
+      then error "negative unary numbers not supported so far"
+      else reifyNatural n f
+
+reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
+reifyNatural n f =
+   if n>0
+     then reifyNatural (n-1) (f . succ)
+     else f zero
+
+
+type instance Un x Num.:+: Un y = Un (x :+: y)
+type instance Un x Num.:*: Un y = Un (x :*: y)
+
+
+instance Natural a => Proxy.Show (Un a) where
+   showsPrec prec =
+      (\n -> showParen (prec>10) (showString (printf "unary u%d" n)))
+       . integerFromSingleton . singletonFromProxy . stripUn
diff --git a/src/Type/Data/Num/Unary/Literal.hs b/src/Type/Data/Num/Unary/Literal.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Unary/Literal.hs
@@ -0,0 +1,138 @@
+module Type.Data.Num.Unary.Literal where
+
+import Type.Data.Num.Unary (Zero, Succ)
+import Type.Base.Proxy (Proxy(Proxy))
+
+
+type U0 = Zero
+type U1 = Succ U0
+type U2 = Succ U1
+type U3 = Succ U2
+type U4 = Succ U3
+type U5 = Succ U4
+type U6 = Succ U5
+type U7 = Succ U6
+type U8 = Succ U7
+type U9 = Succ U8
+type U10 = Succ U9
+type U11 = Succ U10
+type U12 = Succ U11
+type U13 = Succ U12
+type U14 = Succ U13
+type U15 = Succ U14
+type U16 = Succ U15
+type U17 = Succ U16
+type U18 = Succ U17
+type U19 = Succ U18
+type U20 = Succ U19
+type U21 = Succ U20
+type U22 = Succ U21
+type U23 = Succ U22
+type U24 = Succ U23
+type U25 = Succ U24
+type U26 = Succ U25
+type U27 = Succ U26
+type U28 = Succ U27
+type U29 = Succ U28
+type U30 = Succ U29
+type U31 = Succ U30
+type U32 = Succ U31
+type U33 = Succ U32
+type U34 = Succ U33
+type U35 = Succ U34
+type U36 = Succ U35
+type U37 = Succ U36
+type U38 = Succ U37
+type U39 = Succ U38
+type U40 = Succ U39
+type U41 = Succ U40
+type U42 = Succ U41
+type U43 = Succ U42
+type U44 = Succ U43
+type U45 = Succ U44
+type U46 = Succ U45
+type U47 = Succ U46
+type U48 = Succ U47
+type U49 = Succ U48
+type U50 = Succ U49
+type U51 = Succ U50
+type U52 = Succ U51
+type U53 = Succ U52
+type U54 = Succ U53
+type U55 = Succ U54
+type U56 = Succ U55
+type U57 = Succ U56
+type U58 = Succ U57
+type U59 = Succ U58
+type U60 = Succ U59
+type U61 = Succ U60
+type U62 = Succ U61
+type U63 = Succ U62
+type U64 = Succ U63
+
+
+u0 :: Proxy U0; u0 = Proxy
+u1 :: Proxy U1; u1 = Proxy
+u2 :: Proxy U2; u2 = Proxy
+u3 :: Proxy U3; u3 = Proxy
+u4 :: Proxy U4; u4 = Proxy
+u5 :: Proxy U5; u5 = Proxy
+u6 :: Proxy U6; u6 = Proxy
+u7 :: Proxy U7; u7 = Proxy
+u8 :: Proxy U8; u8 = Proxy
+u9 :: Proxy U9; u9 = Proxy
+u10 :: Proxy U10; u10 = Proxy
+u11 :: Proxy U11; u11 = Proxy
+u12 :: Proxy U12; u12 = Proxy
+u13 :: Proxy U13; u13 = Proxy
+u14 :: Proxy U14; u14 = Proxy
+u15 :: Proxy U15; u15 = Proxy
+u16 :: Proxy U16; u16 = Proxy
+u17 :: Proxy U17; u17 = Proxy
+u18 :: Proxy U18; u18 = Proxy
+u19 :: Proxy U19; u19 = Proxy
+u20 :: Proxy U20; u20 = Proxy
+u21 :: Proxy U21; u21 = Proxy
+u22 :: Proxy U22; u22 = Proxy
+u23 :: Proxy U23; u23 = Proxy
+u24 :: Proxy U24; u24 = Proxy
+u25 :: Proxy U25; u25 = Proxy
+u26 :: Proxy U26; u26 = Proxy
+u27 :: Proxy U27; u27 = Proxy
+u28 :: Proxy U28; u28 = Proxy
+u29 :: Proxy U29; u29 = Proxy
+u30 :: Proxy U30; u30 = Proxy
+u31 :: Proxy U31; u31 = Proxy
+u32 :: Proxy U32; u32 = Proxy
+u33 :: Proxy U33; u33 = Proxy
+u34 :: Proxy U34; u34 = Proxy
+u35 :: Proxy U35; u35 = Proxy
+u36 :: Proxy U36; u36 = Proxy
+u37 :: Proxy U37; u37 = Proxy
+u38 :: Proxy U38; u38 = Proxy
+u39 :: Proxy U39; u39 = Proxy
+u40 :: Proxy U40; u40 = Proxy
+u41 :: Proxy U41; u41 = Proxy
+u42 :: Proxy U42; u42 = Proxy
+u43 :: Proxy U43; u43 = Proxy
+u44 :: Proxy U44; u44 = Proxy
+u45 :: Proxy U45; u45 = Proxy
+u46 :: Proxy U46; u46 = Proxy
+u47 :: Proxy U47; u47 = Proxy
+u48 :: Proxy U48; u48 = Proxy
+u49 :: Proxy U49; u49 = Proxy
+u50 :: Proxy U50; u50 = Proxy
+u51 :: Proxy U51; u51 = Proxy
+u52 :: Proxy U52; u52 = Proxy
+u53 :: Proxy U53; u53 = Proxy
+u54 :: Proxy U54; u54 = Proxy
+u55 :: Proxy U55; u55 = Proxy
+u56 :: Proxy U56; u56 = Proxy
+u57 :: Proxy U57; u57 = Proxy
+u58 :: Proxy U58; u58 = Proxy
+u59 :: Proxy U59; u59 = Proxy
+u60 :: Proxy U60; u60 = Proxy
+u61 :: Proxy U61; u61 = Proxy
+u62 :: Proxy U62; u62 = Proxy
+u63 :: Proxy U63; u63 = Proxy
+u64 :: Proxy U64; u64 = Proxy
diff --git a/src/Type/Data/Num/Unary/Proof.hs b/src/Type/Data/Num/Unary/Proof.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Num/Unary/Proof.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Type.Data.Num.Unary.Proof (
+    Nat(..), Pos(..),
+    natFromPos,
+    addNat, addPosL, addPosR,
+    AddZeroL(..), addZeroL,
+    AddComm(..), addComm,
+    AddAssoc(..), addAssoc,
+    mulNat, mulPos,
+    ) where
+
+import Type.Data.Num.Unary
+          (Natural, Positive, Zero, Succ, switchNat, switchPos, (:+:), (:*:))
+
+data Nat x = Natural x => Nat
+data Pos x = Positive x => Pos
+
+
+succNat :: Nat x -> Nat (Succ x)
+succNat Nat = Nat
+
+prevNat :: (Natural x) => Nat (Succ x) -> Nat x
+prevNat Nat = Nat
+
+posSucc :: Nat x -> Pos (Succ x)
+posSucc Nat = Pos
+
+prevPos :: (Natural x) => Pos (Succ x) -> Nat x
+prevPos Pos = Nat
+
+
+natFromPos :: Pos x -> Nat x
+natFromPos Pos = Nat
+
+
+newtype
+   QuantifiedAdd condx condy prop x y =
+      QuantifiedAdd {runQuantifiedAdd :: condx x -> condy y -> prop (x :+: y)}
+
+addNat :: Nat x -> Nat y -> Nat (x :+: y)
+addNat x0 y0@Nat =
+   runQuantifiedAdd
+      (switchNat
+         (QuantifiedAdd const)
+         (QuantifiedAdd $ \x -> succNat . addNat x . prevNat))
+      x0 y0
+
+addPosR :: Nat x -> Pos y -> Pos (x :+: y)
+addPosR x0 y0@Pos =
+   runQuantifiedAdd
+      (switchPos (QuantifiedAdd $ \x -> posSucc . addNat x . prevPos))
+      x0 y0
+
+addPosL :: Pos x -> Nat y -> Pos (x :+: y)
+addPosL x0 y0@Nat =
+   runQuantifiedAdd
+      (switchNat
+         (QuantifiedAdd const)
+         (QuantifiedAdd $ \x -> posSucc . addNat (natFromPos x) . prevNat))
+      x0 y0
+
+
+newtype Quantified prop x = Quantified {runQuantified :: Nat x -> prop x}
+
+induction ::
+   quant Zero -> (forall x. Nat x -> quant (Succ x)) ->
+   Nat y -> quant y
+induction base step y@Nat =
+   runQuantified
+      (switchNat
+         (Quantified $ const base)
+         (Quantified $ step . prevNat))
+      y
+
+
+data AddZeroL x = (Zero:+:x) ~ x => AddZeroL
+
+succZeroL :: AddZeroL x -> AddZeroL (Succ x)
+succZeroL AddZeroL = AddZeroL
+
+addZeroL :: Nat x -> AddZeroL x
+addZeroL = induction AddZeroL (succZeroL . addZeroL)
+
+
+{-
+induction step:
+
+Succ x :+: Succ y
+Succ (x :+: Succ y)
+Succ (Succ (x:+:y))
+Succ (Succ x :+: y)
+-}
+data AddSuccL x y = (Succ x :+: y) ~ Succ (x:+:y) => AddSuccL
+
+succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)
+succSuccL AddSuccL = AddSuccL
+
+addSuccL :: Nat x -> Nat y -> AddSuccL x y
+addSuccL x =
+   induction
+      (case addZeroL x of AddZeroL -> AddSuccL)
+      (succSuccL . addSuccL x)
+
+
+{-
+induction step:
+
+y :+: Succ x
+Succ (y :+: x)
+Succ (x :+: y)
+Succ x :+: y
+-}
+data AddComm x y = (x:+:y) ~ (y:+:x) => AddComm
+
+succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)
+succComm x y AddComm = case addSuccL y x of AddSuccL -> AddComm
+
+{- |
+The proof is pretty expensive.
+For proving (x:+:y ~ y:+:x) we need about @x*y@ reduction steps.
+-}
+addComm :: Nat x -> Nat y -> AddComm x y
+addComm x =
+   induction
+      (case addZeroL x of AddZeroL -> AddComm)
+      (\y -> succComm x y $ addComm x y)
+
+
+{-
+induction step:
+
+x :+: (y :+: Succ z)
+x :+: Succ (y :+: z)
+Succ (x :+: (y :+: z))
+Succ ((x :+: y) :+: z)
+(x :+: y) :+: Succ z
+-}
+data AddAssoc x y z = (x:+:(y:+:z)) ~ ((x:+:y):+:z) => AddAssoc
+
+succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)
+succAssoc AddAssoc = AddAssoc
+
+addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z
+addAssoc x y = induction AddAssoc (succAssoc . addAssoc x y)
+
+
+newtype
+   QuantifiedMul condx condy prop x y =
+      QuantifiedMul {runQuantifiedMul :: condx x -> condy y -> prop (x :*: y)}
+
+mulNat :: Nat x -> Nat y -> Nat (x :*: y)
+mulNat x0 y0@Nat =
+   runQuantifiedMul
+      (switchNat
+         (QuantifiedMul $ \Nat Nat -> Nat)
+         (QuantifiedMul $ \x -> addNat x . mulNat x . prevNat))
+      x0 y0
+
+mulPos :: Pos x -> Pos y -> Pos (x :*: y)
+mulPos x0 y0@Pos =
+   runQuantifiedMul
+      (switchPos
+         (QuantifiedMul $ \x -> addPosL x . mulNat (natFromPos x) . prevPos))
+      x0 y0
diff --git a/src/Type/Data/Ord.hs b/src/Type/Data/Ord.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Data/Ord.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Data.Ord
+    ( Compare
+    , compare
+    , LT
+    , EQ
+    , GT
+    , IsLT
+    , isLT
+    , IsEQ
+    , isEQ
+    , IsGT
+    , isGT
+    , (:<:)
+    , lt
+    , LTT
+    , (:<=:)
+    , le
+    , LET
+    , (:==:)
+    , eq
+    , EQT
+    , (:/=:)
+    , ne
+    , NET
+    , (:>=:)
+    , ge
+    , GET
+    , (:>:)
+    , gt
+    , GTT
+    , Min
+    , min
+    , Max
+    , max
+    ) where
+
+import Type.Data.Bool (If, Not, True, False)
+import Type.Base.Proxy (Proxy(Proxy))
+
+import Prelude ()
+
+
+type family Compare x y
+data LT
+data EQ
+data GT
+compare :: Proxy x -> Proxy y -> Proxy (Compare x y)
+compare Proxy Proxy = Proxy
+
+type family IsLT c
+type instance IsLT LT = True
+type instance IsLT EQ = False
+type instance IsLT GT = False
+isLT :: Proxy c -> Proxy (IsLT c)
+isLT Proxy = Proxy
+
+type family IsEQ c
+type instance IsEQ LT = False
+type instance IsEQ EQ = True
+type instance IsEQ GT = False
+isEQ :: Proxy c -> Proxy (IsEQ c)
+isEQ Proxy = Proxy
+
+type family IsGT c
+type instance IsGT LT = False
+type instance IsGT EQ = False
+type instance IsGT GT = True
+isGT :: Proxy c -> Proxy (IsGT c)
+isGT Proxy = Proxy
+
+type instance Compare LT LT = EQ
+type instance Compare LT EQ = LT
+type instance Compare LT GT = LT
+type instance Compare EQ LT = GT
+type instance Compare EQ EQ = EQ
+type instance Compare EQ GT = LT
+type instance Compare GT LT = GT
+type instance Compare GT EQ = GT
+type instance Compare GT GT = EQ
+
+type family LTT x y
+type instance LTT x y = IsLT (Compare x y)
+lt :: Proxy x -> Proxy y -> Proxy (LTT x y)
+lt Proxy Proxy = Proxy
+class x :<: y
+
+type family LET x y
+type instance LET x y = Not (GTT x y)
+le :: Proxy x -> Proxy y -> Proxy (LET x y)
+le Proxy Proxy = Proxy
+class x :<=: y
+
+type family EQT x y
+type instance EQT x y = IsEQ (Compare x y)
+eq :: Proxy x -> Proxy y -> Proxy (EQT x y)
+eq Proxy Proxy = Proxy
+class x :==: y
+
+type family NET x y
+type instance NET x y = Not (EQT x y)
+ne :: Proxy x -> Proxy y -> Proxy (NET x y)
+ne Proxy Proxy = Proxy
+class x :/=: y
+
+type family GET x y
+type instance GET x y = Not (LTT x y)
+ge :: Proxy x -> Proxy y -> Proxy (GET x y)
+ge Proxy Proxy = Proxy
+class x :>=: y
+
+type family GTT x y
+type instance GTT x y = IsGT (Compare x y)
+gt :: Proxy x -> Proxy y -> Proxy (GTT x y)
+gt Proxy Proxy = Proxy
+class x :>: y
+
+type family Min x y
+type instance Min x y = If (LET x y) x y
+min :: Proxy x -> Proxy y -> Proxy (Min x y)
+min Proxy Proxy = Proxy
+
+type family Max x y
+type instance Max x y = If (GET x y) x y
+max :: Proxy x -> Proxy y -> Proxy (Max x y)
+max Proxy Proxy = Proxy
+
+type instance Compare False False = EQ
+type instance Compare False True  = LT
+type instance Compare True  False = GT
+type instance Compare True  True  = EQ
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,369 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Main where
+
+import qualified Type.Data.Num.Decimal.Literal as Lit
+import qualified Type.Data.Num.Decimal.Number as Dec
+import qualified Type.Data.Num.Unary.Literal as UnaryLit
+import Type.Data.Num.Decimal.Number (Dec)
+import Type.Data.Num.Decimal.Digit
+import Type.Data.Num as Num
+import Type.Data.Bool
+import Type.Data.Ord
+import Type.Base.Proxy (Proxy(Proxy))
+
+import qualified Test.QuickCheck as Q
+
+import Control.Monad (when)
+import Data.Char (intToDigit)
+
+import qualified Prelude
+
+
+type D0 = Dec Lit.D0
+type D1 = Dec Lit.D1
+type D2 = Dec Lit.D2
+type D3 = Dec Lit.D3
+type D4 = Dec Lit.D4
+type D5 = Dec Lit.D5
+type D6 = Dec Lit.D6
+type D7 = Dec Lit.D7
+type D8 = Dec Lit.D8
+type D9 = Dec Lit.D9
+type D10 = Dec Lit.D10
+type D11 = Dec Lit.D11
+type D16 = Dec Lit.D16
+type D17 = Dec Lit.D17
+type D31 = Dec Lit.D31
+type D32 = Dec Lit.D32
+type D49 = Dec Lit.D49
+type D50 = Dec Lit.D50
+type D57 = Dec Lit.D57
+type D58 = Dec Lit.D58
+type D90 = Dec Lit.D90
+type D99 = Dec Lit.D99
+type D100 = Dec Lit.D100
+type D101 = Dec Lit.D101
+
+type DN1 = Dec Lit.DN1
+type DN2 = Dec Lit.DN2
+type DN5 = Dec Lit.DN5
+type DN6 = Dec Lit.DN6
+type DN9 = Dec Lit.DN9
+type DN10 = Dec Lit.DN10
+type DN11 = Dec Lit.DN11
+type DN50 = Dec Lit.DN50
+type DN99 = Dec Lit.DN99
+type DN100 = Dec Lit.DN100
+type DN101 = Dec Lit.DN101
+
+type D527 = Dec (Lit.Pos3 Dec5 Dec2 Dec7)
+type D720 = Dec (Lit.Pos3 Dec7 Dec2 Dec0)
+type D989 = Dec (Lit.Pos3 Dec9 Dec8 Dec9)
+type D1000 = Dec (Lit.Pos4 Dec1 Dec0 Dec0 Dec0)
+type D1024 = Dec (Lit.Pos4 Dec1 Dec0 Dec2 Dec4)
+type D10000 = Dec (Lit.Pos5 Dec1 Dec0 Dec0 Dec0 Dec0)
+type D3628800 = Dec (Lit.Pos7 Dec3 Dec6 Dec2 Dec8 Dec8 Dec0 Dec0)
+
+testIsPositive1 :: IsPositive D1 -> True
+testIsPositive1 = Prelude.id
+testIsPositive2 :: IsPositive D0 -> False
+testIsPositive2 = Prelude.id
+testIsPositive3 :: IsPositive DN1 -> False
+testIsPositive3 = Prelude.id
+testIsPositive4 :: IsPositive D10 -> True
+testIsPositive4 = Prelude.id
+testIsPositive5 :: IsPositive DN10 -> False
+testIsPositive5 = Prelude.id
+
+testIsNegative1 :: IsNegative D1 -> False
+testIsNegative1 = Prelude.id
+testIsNegative2 :: IsNegative D0 -> False
+testIsNegative2 = Prelude.id
+testIsNegative3 :: IsNegative DN1 -> True
+testIsNegative3 = Prelude.id
+testIsNegative4 :: IsNegative D10 -> False
+testIsNegative4 = Prelude.id
+testIsNegative5 :: IsNegative DN10 -> True
+testIsNegative5 = Prelude.id
+
+testIsZero1 :: IsZero D1 -> False
+testIsZero1 = Prelude.id
+testIsZero2 :: IsZero D0 -> True
+testIsZero2 = Prelude.id
+testIsZero3 :: IsZero DN1 -> False
+testIsZero3 = Prelude.id
+testIsZero4 :: IsZero D10 -> False
+testIsZero4 = Prelude.id
+testIsZero5 :: IsZero DN10 -> False
+testIsZero5 = Prelude.id
+
+testSucc1 :: Succ D0 -> D1
+testSucc1 = Prelude.id
+testSucc2 :: Succ D9 -> D10
+testSucc2 = Prelude.id
+testSucc3 :: Succ DN1 -> D0
+testSucc3 = Prelude.id
+testSucc4 :: Succ D99 -> D100
+testSucc4 = Prelude.id
+testSucc5 :: Succ DN100 -> DN99
+testSucc5 = Prelude.id
+testSucc6 :: Succ D100 -> D101
+testSucc6 = Prelude.id
+testSucc7 :: Succ DN101 -> DN100
+testSucc7 = Prelude.id
+testSucc8 :: Succ D0 -> D1 :+: D0
+testSucc8 = Prelude.id
+testSucc9 :: Succ D0 -> D0 :+: D1
+testSucc9 = Prelude.id
+testSucc10 :: Succ D9 -> D1 :+: D9
+testSucc10 = Prelude.id
+testSucc11 :: Succ D9 -> D9 :+: D1
+testSucc11 = Prelude.id
+
+testPred1 :: Pred D1 -> D0
+testPred1 = Prelude.id
+testPred2 :: Pred D0 -> DN1
+testPred2 = Prelude.id
+testPred3 :: Pred DN1 -> DN2
+testPred3 = Prelude.id
+testPred4 :: Pred DN9 -> DN10
+testPred4 = Prelude.id
+testPred5 :: Pred D10 -> D9
+testPred5 = Prelude.id
+testPred6 :: Pred DN99 -> DN100
+testPred6 = Prelude.id
+testPred7 :: Pred D100 -> D99
+testPred7 = Prelude.id
+testPred8 :: Pred D0 -> D0 :-: D1
+testPred8 = Prelude.id
+testPred9 :: Pred D10 -> D10 :-: D1
+testPred9 = Prelude.id
+testPred10 :: Pred D9 -> D8
+testPred10 = Prelude.id
+testPred11 :: Pred D8 -> D7
+testPred11 = Prelude.id
+testPred12 :: Pred D7 -> D6
+testPred12 = Prelude.id
+testPred13 :: Pred D6 -> D5
+testPred13 = Prelude.id
+testPred14 :: Pred D5 -> D4
+testPred14 = Prelude.id
+testPred15 :: Pred D4 -> D3
+testPred15 = Prelude.id
+testPred16 :: Pred D3 -> D2
+testPred16 = Prelude.id
+testPred17 :: Pred D2 -> D1
+testPred17 = Prelude.id
+testPred18 :: Pred D1 -> D0
+testPred18 = Prelude.id
+
+testAdd1 :: D0 :+: D0 -> D0
+testAdd1 = Prelude.id
+testAdd2 :: DN1 :+: D1 -> D0
+testAdd2 = Prelude.id
+testAdd3 :: D1 :+: DN1 -> D0
+testAdd3 = Prelude.id
+testAdd4 :: D1 :+: D1 -> D2
+testAdd4 = Prelude.id
+testAdd5 :: D9 :+: D1 -> D10
+testAdd5 = Prelude.id
+testAdd6 :: D10 :+: DN1 -> D9
+testAdd6 = Prelude.id
+testAdd7 :: D100 :+: DN1 -> D99
+testAdd7 = Prelude.id
+testAdd8 :: D100 :+: DN10 -> D90
+testAdd8 = Prelude.id
+
+testSub1 :: D0 :-: D0 -> D0
+testSub1 = Prelude.id
+testSub2 :: D1 :-: D0 -> D1
+testSub2 = Prelude.id
+testSub3 :: D0 :-: D1 -> DN1
+testSub3 = Prelude.id
+testSub4 :: DN1 :-: D0 -> DN1
+testSub4 = Prelude.id
+testSub5 :: D0 :-: DN1 -> D1
+testSub5 = Prelude.id
+testSub6 :: D100 :-: D1 -> D99
+testSub6 = Prelude.id
+testSub7 :: DN100 :-: D1 -> DN101
+testSub7 = Prelude.id
+testSub8 :: D100 :-: DN1 -> D101
+testSub8 = Prelude.id
+testSub9 :: DN100 :-: DN1 -> DN99
+testSub9 = Prelude.id
+testSub10 :: D1 :-: D100 -> DN99
+testSub10 = Prelude.id
+testSub11 :: DN1 :-: D100 -> DN101
+testSub11 = Prelude.id
+testSub12 :: D1 :-: DN100 -> D101
+testSub12 = Prelude.id
+testSub13 :: DN1 :-: DN100 -> D99
+testSub13 = Prelude.id
+testSub14 :: D57 :-: D58 -> DN1
+testSub14 = Prelude.id
+testSub15 :: D1000 :-: D11 -> D989
+testSub15 = Prelude.id
+
+testHalf1 :: Div2 D0 -> D0
+testHalf1 = Prelude.id
+testHalf2 :: Div2 D1 -> D0
+testHalf2 = Prelude.id
+testHalf3 :: Div2 D2 -> D1
+testHalf3 = Prelude.id
+testHalf4 :: Div2 D10 -> D5
+testHalf4 = Prelude.id
+testHalf5 :: Div2 D11 -> D5
+testHalf5 = Prelude.id
+testHalf6 :: Div2 D99 -> D49
+testHalf6 = Prelude.id
+testHalf7 :: Div2 D100 -> D50
+testHalf7 = Prelude.id
+testHalf8 :: Div2 D101 -> D50
+testHalf8 = Prelude.id
+testHalf9 :: Div2 DN1 -> D0
+testHalf9 = Prelude.id
+testHalf10 :: Div2 DN2 -> DN1
+testHalf10 = Prelude.id
+testHalf11 :: Div2 DN10 -> DN5
+testHalf11 = Prelude.id
+testHalf12 :: Div2 DN11 -> DN5
+testHalf12 = Prelude.id
+testHalf13 :: Div2 DN100 -> DN50
+testHalf13 = Prelude.id
+
+testMul1 :: D0 :*: D0 -> D0
+testMul1 = Prelude.id
+testMul2 :: D0 :*: D1 -> D0
+testMul2 = Prelude.id
+testMul3 :: D1 :*: D0 -> D0
+testMul3 = Prelude.id
+testMul4 :: D1 :*: D1 -> D1
+testMul4 = Prelude.id
+testMul5 :: D1 :*: DN1 -> DN1
+testMul5 = Prelude.id
+testMul6 :: DN1 :*: D1 -> DN1
+testMul6 = Prelude.id
+testMul7 :: DN1 :*: DN1 -> D1
+testMul7 = Prelude.id
+testMul8 :: D100 :*: D100 -> D10000
+testMul8 = Prelude.id
+testMul9 :: D17 :*: D31 -> D527
+testMul9 = Prelude.id
+
+testFac1 :: Fac D0 -> D1
+testFac1 = Prelude.id
+testFac2 :: Fac D1 -> D1
+testFac2 = Prelude.id
+testFac3 :: Fac D6 -> D720
+testFac3 = Prelude.id
+testFac4 :: Fac D10 -> D3628800
+testFac4 = Prelude.id
+
+testEQ1 :: EQT D0 D0 -> True
+testEQ1 = Prelude.id
+testEQ2 :: EQT D0 (Pred D1) -> True
+testEQ2 = Prelude.id
+testEQ3 :: EQT (D1 :+: D9) D10 -> True
+testEQ3 = Prelude.id
+testEQ4 :: EQT (D1 :+: D9) D11 -> False
+testEQ4 = Prelude.id
+testEQ5 :: EQT D9 D0 -> False
+testEQ5 = Prelude.id
+testEQ6 :: EQT D8 D0 -> False
+testEQ6 = Prelude.id
+testEQ7 :: EQT D7 D0 -> False
+testEQ7 = Prelude.id
+testEQ8 :: EQT D6 D0 -> False
+testEQ8 = Prelude.id
+testEQ9 :: EQT D5 D0 -> False
+testEQ9 = Prelude.id
+testEQ10 :: EQT D4 D0 -> False
+testEQ10 = Prelude.id
+testEQ11 :: EQT D3 D0 -> False
+testEQ11 = Prelude.id
+testEQ12 :: EQT D2 D0 -> False
+testEQ12 = Prelude.id
+testEQ13 :: EQT D1 D0 -> False
+testEQ13 = Prelude.id
+
+testMin1 :: Min D0 D5 -> D0
+testMin1 = Prelude.id
+testMin2 :: Min D5 D0 -> D0
+testMin2 = Prelude.id
+testMin3 :: Min DN5 D5 -> DN5
+testMin3 = Prelude.id
+
+testMax1 :: Max D1 D6 -> D6
+testMax1 = Prelude.id
+testMax2 :: Max DN6 D6 -> D6
+testMax2 = Prelude.id
+testMax3 :: Max D6 D1 -> D6
+testMax3 = Prelude.id
+
+testExp1 :: Pow2 D0 -> D1
+testExp1 = Prelude.id
+testExp2 :: Pow2 D1 -> D2
+testExp2 = Prelude.id
+testExp3 :: Pow2 D2 -> D4
+testExp3 = Prelude.id
+testExp4 :: Pow2 D3 -> D8
+testExp4 = Prelude.id
+testExp5 :: Pow2 D4 -> D16
+testExp5 = Prelude.id
+testExp6 :: Pow2 D5 -> D32
+testExp6 = Prelude.id
+testExp7 :: Pow2 D10 -> D1024
+testExp7 = Prelude.id
+
+testLog1 :: Log2Ceil D1 -> D0
+testLog1 = Prelude.id
+testLog2 :: Log2Ceil D2 -> D1
+testLog2 = Prelude.id
+testLog3 :: Log2Ceil D3 -> D2
+testLog3 = Prelude.id
+testLog4 :: Log2Ceil D4 -> D2
+testLog4 = Prelude.id
+testLog5 :: Log2Ceil D7 -> D3
+testLog5 = Prelude.id
+testLog6 :: Log2Ceil D8 -> D3
+testLog6 = Prelude.id
+testLog7 :: Log2Ceil D9 -> D4
+testLog7 = Prelude.id
+
+testDecToUnary :: Dec.ToUnary Lit.D42 -> UnaryLit.U42
+testDecToUnary = Prelude.id
+
+testDecFromUnary :: Dec.FromUnary UnaryLit.U42 -> Lit.D42
+testDecFromUnary = Prelude.id
+
+
+class TestIter n zero where
+    testIter :: Proxy n -> Proxy zero -> Prelude.String
+
+instance ( Num.Natural n, EQT n D0 ~ True )
+  => TestIter n True where
+    testIter _ _ = ""
+
+instance ( Num.Natural n, EQT n D0 ~ False
+         , TestIter (Pred n) (EQT (Pred n) D0) )
+  => TestIter n False where
+    testIter n _ =
+        intToDigit (Num.fromInteger n) :
+        testIter (Proxy :: Proxy (Pred n)) (Proxy :: Proxy (EQT (Pred n) D0))
+
+main :: Prelude.IO ()
+main = do
+  let testIterResult = testIter (Dec.decimal Lit.d9) (Proxy :: Proxy False)
+  when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))
+  Q.quickCheck prop_reifyIntegral
+
+prop_reifyIntegral :: Prelude.Integer -> Prelude.Bool
+prop_reifyIntegral i =
+  Num.reifyIntegral (Proxy :: Proxy Dec.Decimal) i Num.fromInteger Prelude.== i
diff --git a/tfp.cabal b/tfp.cabal
--- a/tfp.cabal
+++ b/tfp.cabal
@@ -1,68 +1,74 @@
 name:           tfp
-version:        0.3
-cabal-version:  >= 1.6
+version:        1.0.2
 build-type:     Simple
 license:        BSD3
 license-file:   LICENSE
-copyright:      Copyright (c) 2008 Peter Gavin
-author:         Peter Gavin
-maintainer:     pgavin@gmail.com
-homepage:       http://abt12monk.org/git/tfp.git/
+copyright:      Copyright (c) 2014 Henning Thielemann, 2008 Peter Gavin
+author:         Peter Gavin, Henning Thielemann
+maintainer:     haskell@henning-thielemann.de
+homepage:       http://www.haskell.org/haskellwiki/Type_arithmetic
 stability:      alpha
-package-url:    http://abt12monk.org/git/tfp.git/
-synopsis:       Type-level programming library using type families
-description:	TFP (short for Type Family Programming) provides implementations of type-level integers and booleans,
-		and (eventually) simple type-level data structures. It uses type families as functions to produce new types,
-		which provides an intuitive way to parameterize data types and functions on numerical values at compile time.
-category:       Data
-tested-with:    GHC == 6.9.0
+synopsis:       Type-level integers, booleans, lists using type families
+description:
+  TFP is an abbreviation for Type Family Programming.
+  It provides implementations of type-level integers and booleans,
+  and (eventually) simple type-level data structures.
+  It uses type families as functions to produce new types,
+  which provides an intuitive way to parameterize data types
+  and functions on numerical values at compile time.
+category:       Type System
+tested-with:    GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 8.0.1
+cabal-version:  1.14
+extra-source-files:
+  Changes.md
 
-source-repository head {
-  type:         git
-  location:     http://abt12monk.org/git/tfp.git/
-}
+source-repository head
+  type:         darcs
+  location:     https://hub.darcs.net/thielema/tfp/
 
-flag build-test
-  description: Build the tfp-test test program
-  default: False
+source-repository this
+  tag:          1.0.2
+  type:         darcs
+  location:     https://hub.darcs.net/thielema/tfp/
 
+
 library {
-  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
-                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
-                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,
-                  Rank2Types, FlexibleContexts
-  build-depends:  base >= 3.0 && < 5, template-haskell >= 2.0
+  default-language: Haskell2010
+  build-depends:
+    utility-ht >=0.0.10 && <0.1,
+    base >=4.5 && <5
+  ghc-options: -Wall
+  if impl(ghc>=8.0)
+    ghc-options: -fno-warn-redundant-constraints
+  hs-source-dirs: src
   exposed-modules:
-    Data.SizedInt,
-    Data.SizedWord,
-    Types,
-    Types.Base,
-    Types.Data.Bool,
-    Types.Data.Num
-    Types.Data.Num.Ops
-    Types.Data.Num.Decimal,
-    Types.Data.Num.Decimal.Literals
-    Types.Data.Num.Decimal.Literals.TH
-    Types.Data.Num.Decimal.Digits
-    Types.Data.List,
-    Types.Data.Ord
-  other-modules:
-    Types.Data.Num.Decimal.Ops
+    Data.SizedInt
+    Data.SizedWord
+    Type.Base.Proxy
+    Type.Data.Bool
+    Type.Data.Num
+    Type.Data.Num.Unary
+    Type.Data.Num.Unary.Literal
+    Type.Data.Num.Unary.Proof
+    Type.Data.Num.Decimal
+    Type.Data.Num.Decimal.Literal
+    Type.Data.Num.Decimal.Digit
+    Type.Data.Num.Decimal.Digit.Proof
+    Type.Data.Num.Decimal.Number
+    Type.Data.Num.Decimal.Proof
+    Type.Data.List
+    Type.Data.Ord
 }
 
 
-executable tfp-test {
-  if flag(build-test) {
-    buildable: True
-  } else {
-    buildable: False
-  }
-  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
-                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
-                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,
-                  FunctionalDependencies, Rank2Types, FlexibleContexts
+test-suite tfp-test {
+  type: exitcode-stdio-1.0
+  build-depends:
+    tfp,
+    QuickCheck >= 1.2.0.0,
+    base
+  default-language: Haskell2010
+  ghc-options: -Wall
   main-is: Test.hs
-  build-depends:  base >= 3.0 && < 5, template-haskell >= 2.0, QuickCheck >= 1.2.0.0
+  hs-source-dirs: test
 }