git.iko.soy/Idris-dev
on 875eecc help sign in
Idris-dev/tutorial/examples/binary.idr
64 lines 1.4 kB history raw
1module Main
3data Binary : Nat -> Type 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 = show' where
10 show' : Binary n' -> String
11 show' (bO x) = show x ++ "0"
12 show' (bI x) = show x ++ "1"
13 show' bEnd = ""
15data Parity : Nat -> Type where
16 even : Parity (n + n)
17 odd : Parity (S (n + n))
19parity : (n:Nat) -> Parity n
20parity O = even {n=O}
21parity (S O) = odd {n=O}
22parity (S (S k)) with (parity k)
23 parity (S (S (j + j))) | even ?= even {n=S j}
24 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))
32intToNat : Int -> Nat
33intToNat 0 = O
34intToNat x = if (x>0) then (S (intToNat (x-1))) else O
36main : IO ()
37main = do putStr "Enter a number: "
38 x <- getLine
39 print (natToBin (fromInteger (cast x)))
41---------- Proofs ----------
43parity_lemma_1 = proof {
44 intros;
45 rewrite sym (plusSuccRightSucc j j);
46 trivial;
49natToBin_lemma_1 = proof {
50 intro;
51 intro;
52 rewrite sym (plusSuccRightSucc j j);
53 trivial;
56parity_lemma_2 = proof {
57 intro;
58 intro;
59 rewrite sym (plusSuccRightSucc j j);
60 trivial;