Commit cf67512b authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Revert IsEven to the way it was.

parent 3b8f0928
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment