Wrap data declarations in mutual blocks
This lets them get totality checked.
commitc56dee39a64613f37183e167aa8a0fc55ae6c94d
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 22 Apr 2015, 11:25 (12 years ago)
parente0b0516
src/Idris/Coverage.hs+1−1
@@ -705,7 +705,7 @@ checkMP ist i mp = if i > 0
705705 = case lookupTotal f (tt_ctxt ist) of
706706 [Total _] -> Unchecked -- okay so far
707707 [Partial _] -> Partial (Other [f])
708− x -> error $ "CAN'T HAPPEN: " ++ (show x)
708+ x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
709709 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
710710 = Total []
711711 tryPath desc path (e@(f, args) : es) arg
src/Idris/Parser.hs+1
@@ -1471,6 +1471,7 @@ loadSource lidr f toline
14711471 case x of
14721472 PClauses{} -> r
14731473 PClass{} -> r
1474+ PData{} -> r
14741475 PInstance{} -> r
14751476 _ -> x
14761477