Revert IsEven to the way it was.
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Thu, 22 Mar 2012 07:46:22 +0000 (00:46 -0700)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Thu, 22 Mar 2012 07:46:22 +0000 (00:46 -0700)
GHC/TypeLits.hs

index cbbd015..fd5dd1a 100644 (file)
@@ -174,8 +174,8 @@ instance Show (IsZero n) where
 
 data IsEven :: Nat -> * where
   IsEvenZero :: IsEven 0
-  IsEven     :: !(TNat n) -> IsEven (2 * n + 2)
-  IsOdd      :: !(TNat n) -> IsEven (2 * n + 1)
+  IsEven     :: !(TNat (n+1)) -> IsEven (2 * n + 2)
+  IsOdd      :: !(TNat n)     -> IsEven (2 * n + 1)
 
 isEven :: TNat n -> IsEven n
 isEven (TNat n) | n == 0      = unsafeCoerce IsEvenZero