git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/tutorial/Views.idr
25 lines 775 B history raw
1module views
3data Parity : Nat -> Type where
4 Even : Parity (n + n)
5 Odd : Parity (S (n + n))
7helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
8helpEven j p = rewrite plusSuccRightSucc j j in p
10helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
11helpOdd j p = rewrite plusSuccRightSucc j j in p
13parity : (n:Nat) -> Parity n
14parity Z = Even {n=Z}
15parity (S Z) = Odd {n=Z}
16parity (S (S k)) with (parity k)
17 parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
18 parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
20natToBin : Nat -> List Bool
21natToBin Z = Nil
22natToBin k with (parity k)
23 natToBin (j + j) | Even = False :: natToBin j
24 natToBin (S (j + j)) | Odd = True :: natToBin j