git.iko.soy/Idris-dev
on bb3e629 help sign in
Idris-dev/tutorial/examples/binary.idr
62 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 print (natToBin (fromInteger (cast x)))
39---------- Proofs ----------
41natToBin_lemma_1 = proof {
42 intro;
43 intro;
44 rewrite sym (plusSuccRightSucc j j);
45 trivial;
48parity_lemma_2 = proof {
49 intro;
50 intro;
51 rewrite sym (plusSuccRightSucc j j);
52 trivial;
55parity_lemma_1 = proof {
56 intro j;
57 intro;
58 rewrite sym (plusSuccRightSucc j j);
59 trivial;