@@ -1,8 +1,8 @@
3data Parity : Nat -> Type where
3data Parity : Nat -> Type where
4− even : Parity (n + n)
4+ even : {n : Nat} -> Parity (n + n)
5− odd : Parity (S (n + n))
5+ odd : {n : Nat} -> Parity (S (n + n))
7parity : (n:Nat) -> Parity n
7parity : (n:Nat) -> Parity n
8parity Z = even {n=Z}
8parity Z = even {n=Z}