tutorial/examples/views.idr · Idris-dev

git.iko.soy/Idris-dev

on d1663cc 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;