@@ -0,0 +1,42 @@
1+module main;
2+
3+data Parity : Nat -> Set where
4+ even : Parity (n + n)
5+ | odd : Parity (S (n + n));
6+
7+parity : (n:Nat) -> Parity n;
8+parity O = even {n=O};
9+parity (S O) = odd {n=O};
10+parity (S (S k)) with parity k {
11+ parity (S (S (j + j))) | even ?= even {n=S j};
12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
13+}
14+
15+
16+natToBin : Nat -> List Bool;
17+natToBin O = Nil;
18+natToBin k with parity k {
19+ natToBin (j + j) | even = False :: natToBin j;
20+ natToBin (S (j + j)) | odd = True :: natToBin j;
21+}
22+
23+main : IO ();
24+main = print (natToBin 42);
25+
26+---------- Proofs ----------
27+
28+main.parity_lemma_2 = proof {
29+ intro;
30+ intro;
31+ rewrite plusn_Sm j j;
32+ trivial;
33+};
34+
35+main.parity_lemma_1 = proof {
36+ intro j;
37+ intro;
38+ rewrite plusn_Sm j j;
39+ trivial;
40+};
41+
42+