Merge pull request #2118 from japesinator/contains-hole
Show incomplete term holes for listy constructors
commit553631484524e89dd57462431c928b8b9bba54d2
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 5 Apr 2015, 00:43 (12 years ago)
parent927fc19da8b88a
src/Idris/AbsSyntaxTree.hs+2
@@ -1628,6 +1628,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16281628 basename (NS n _) = basename n
16291629 basename n = n
16301630
1631+ slist' _ _ e
1632+ | containsHole e = Nothing
16311633 slist' p bnd (PApp _ (PRef _ nil) _)
16321634 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
16331635 slist' p bnd (PRef _ nil)