Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

40 lines (30 sloc) 0.792 kB
module main
data Parity : Nat -> Set where
even : Parity (n + n)
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j
main : IO ()
main = do print (natToBin 42)
---------- Proofs ----------
main.parity_lemma_2 = proof {
intro;
intro;
rewrite sym (plusSuccRightSucc j j);
trivial;
};
main.parity_lemma_1 = proof {
intro j;
intro;
rewrite sym (plusSuccRightSucc j j);
trivial;
};
Jump to Line
Something went wrong with that request. Please try again.