git.iko.soy/Idris-dev
on d03a437 help sign in
Idris-dev/test/tutorial006/tutorial006b.idr
12 lines 303 B history raw
2data Parity : Nat -> Type where
3 Even : Parity (n + n)
4 Odd : Parity (S (n + n))
6parity : (n:Nat) -> Parity n
7parity Z = Even {n=Z}
8parity (S Z) = Odd {n=Z}
9parity (S (S k)) with (parity k)
10 parity (S (S (j + j))) | Even = Even {n=S j}
11 parity (S (S (S (j + j)))) | Odd = Odd {n=S j}