git.iko.soy/Idris-dev
on master help sign in
Extend rules for 'impossible' cases
6efe40bEdwin Brady
libs/prelude/Prelude/Basics.idr+3−3
compare with master
unifiedsplit
@@ -53,9 +53,9 @@ data Dec : Type -> Type where
53
53
54 ||| The case where the property holds
54 ||| The case where the property holds
55 ||| @ prf the proof
55 ||| @ prf the proof
56− Yes : {A : Type} -> (prf : A) -> Dec A
56+ Yes : (prf : prop) -> Dec prop
57
57
58 ||| The case where the property holding would be a contradiction
58 ||| The case where the property holding would be a contradiction
59− ||| @ contra a demonstration that A would be a contradiction
59+ ||| @ contra a demonstration that prop would be a contradiction
60− No : {A : Type} -> (contra : A -> Void) -> Dec A
60+ No : (contra : prop -> Void) -> Dec prop
61
61
src/Idris/Coverage.hs+1
@@ -135,6 +135,7 @@ validCoverageCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
135 = case (unApply topx, unApply topy) of
135 = case (unApply topx, unApply topy) of
136 ((P _ x _, _), (P _ y _, _)) -> x == y
136 ((P _ x _, _), (P _ y _, _)) -> x == y
137 _ -> False
137 _ -> False
138+validCoverageCase ctxt (InfiniteUnify _ _ _) = False
138validCoverageCase ctxt (CantConvert _ _ _) = False
139validCoverageCase ctxt (CantConvert _ _ _) = False
139validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
140validCoverageCase ctxt (At _ e) = validCoverageCase ctxt e
140validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e
141validCoverageCase ctxt (Elaborating _ _ _ e) = validCoverageCase ctxt e