@@ -40,6 +40,12 @@ mkPatTm t = do i <- getIState
4040 toTT (PApp _ t args) = do t' <- toTT t
4141 args' <- mapM (toTT . getTm) args
4242 return $ mkApp t' args'
43+ toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
44+ r' <- toTT r
45+ return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
46+ toTT (PPair _ _ _ l r) = do l' <- toTT l
47+ r' <- toTT r
48+ return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
4349 -- For alternatives, pick the first and drop the namespaces. It doesn't
4450 -- really matter which is taken since matching will ignore the namespace.
4551 toTT (PAlternative _ _ (a : as)) = toTT a
@@ -78,7 +84,7 @@ genClauses fc n xs given
7884 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
7985 logCoverage 10 $ show argss ++ "\n" ++ show all_args
8086 logCoverage 3 $ "Original: \n" ++
81− showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
87+ showSep "\n" (map (\t -> showTmImpls (delab' i t True True)) xs)
8288 -- add an infinite supply of explicit arguments to update the possible
8389 -- cases for (the return type may be variadic, or function type, so
8490 -- there may be more case splitting that the idris_implicits record