edwinb/Idris-dev — pull request #80 by raichoo (2012-11-12 20:55:14+00:00)
Title: coverage fix for unhandled cases

Error:

src/Idris/Coverage.hs:(402,4)-(409,51): Non-exhaustive patterns in case

Testcase to reproduce:

module Test

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 O)) = even {n = S O}
parity (S (S k)) with (parity k)
parity (S (S (m + m))) | even ?= even {n = S m}
parity (S (S (S (m + m)))) | odd ?= odd {n = S m}

{-
Test.parity_lemma_1 = proof {
intro;
rewrite plusSuccRightSucc m m;
intro;
trivial;
}

Test.parity_lemma_2 = proof {
intro;
rewrite plusSuccRightSucc m m;
intro;
trivial;
}
-}

prove lemmas without doing :addproof