git.iko.soy/Idris-dev
on ebbcf8d help sign in
Idris-dev/tutorial/examples/binary.idr
67 lines 1.4 kB history raw
1module main;
3data Binary : Nat -> Set where
4 bEnd : Binary O
5 | bO : Binary n -> Binary (n + n)
6 | bI : Binary n -> Binary (S (n + n));
8instance Show (Binary n) where {
9 show (bO x) = show x ++ "0";
10 show (bI x) = show x ++ "1";
11 show bEnd = "";
14data Parity : Nat -> Set where
15 even : Parity (n + n)
16 | odd : Parity (S (n + n));
18parity : (n:Nat) -> Parity n;
19parity O = even {n=O};
20parity (S O) = odd {n=O};
21parity (S (S k)) with parity k {
22 parity (S (S (j + j))) | even ?= even {n=S j};
23 parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
26natToBin : (n:Nat) -> Binary n;
27natToBin O = bEnd;
28natToBin (S k) with parity k {
29 natToBin (S (j + j)) | even = bI (natToBin j);
30 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j));
33intToNat : Int -> Nat;
34intToNat 0 = O;
35intToNat x = if (x>0) then (S (intToNat (x-1))) else O;
37main : IO ();
38main = do { putStr "Enter a number: ";
39 x <- getLine;
40 let n = prim__strToInt x;
41 let b = natToBin (fromInteger n);
42 print b; };
44---------- Proofs ----------
46natToBin_lemma_1 = proof {
47 intro;
48 intro;
49 rewrite plusn_Sm j j;
50 trivial;
51};
53parity_lemma_2 = proof {
54 intro;
55 intro;
56 rewrite plusn_Sm j j;
57 trivial;
58};
60parity_lemma_1 = proof {
61 intro j;
62 intro;
63 rewrite plusn_Sm j j;
64 trivial;
65};