git.iko.soy/Idris-dev
on 10ea548 help sign in
Idris-dev/tutorial/examples/binary.idr
63 lines 1.3 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 = ""
13data Parity : Nat -> Set where
14 even : Parity (n + n)
15 odd : Parity (S (n + n))
17parity : (n:Nat) -> Parity n
18parity O = even {n=O}
19parity (S O) = odd {n=O}
20parity (S (S k)) with (parity k)
21 parity (S (S (j + j))) | even ?= even {n=S j}
22 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
24natToBin : (n:Nat) -> Binary n
25natToBin O = bEnd
26natToBin (S k) with (parity k)
27 natToBin (S (j + j)) | even = bI (natToBin j)
28 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
30intToNat : Int -> Nat
31intToNat 0 = O
32intToNat x = if (x>0) then (S (intToNat (x-1))) else O
34main : IO ()
35main = do putStr "Enter a number: "
36 x <- getLine
37 let b = natToBin (fromInteger (cast x))
38 print b
40---------- Proofs ----------
42natToBin_lemma_1 = proof {
43 intro;
44 intro;
45 rewrite plusn_Sm j j;
46 trivial;
49parity_lemma_2 = proof {
50 intro;
51 intro;
52 rewrite plusn_Sm j j;
53 trivial;
56parity_lemma_1 = proof {
57 intro j;
58 intro;
59 rewrite plusn_Sm j j;
60 trivial;