samples/tutorial/views.idr · Idris-dev

git.iko.soy/Idris-dev

on d06ca16 help sign in

37 lines 749 B history raw

1module views

3data Parity : Nat -> Type where

4 Even : Parity (n + n)

5 Odd : Parity (S (n + n))

7parity : (n:Nat) -> Parity n

8parity Z = Even {n=Z}

9parity (S Z) = Odd {n=Z}

10parity (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}

14natToBin : Nat -> List Bool

15natToBin Z = Nil

16natToBin k with (parity k)

17 natToBin (j + j) | Even = False :: natToBin j

18 natToBin (S (j + j)) | Odd = True :: natToBin j

21---------- Proofs ----------

23views.parity_lemma_2 = proof {

24 intro;

25 intro;

26 rewrite sym (plusSuccRightSucc j j);

27 trivial;

30views.parity_lemma_1 = proof {

31 intro;

32 intro;

33 rewrite sym (plusSuccRightSucc j j);

34 trivial;