31ca891 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1

@@ -1384,6 +1384,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1384 where strName (UN n) = T.unpack n

1385 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1386 | otherwise = strName n

1387+ strName n | n == falseTy = "_|_"

1387 strName (MN i s) = T.unpack s

1388 strName (MN i s) = T.unpack s

1388 strName other = show other

1389 strName other = show other

1389

1390

src/Idris/Docs.hs+2

@@ -120,6 +120,8 @@ docFun n

120 where funName :: Name -> String

121 funName (UN n) = str n

122 funName (NS n _) = funName n

123+ funName n

124+ | n == falseTy = "_|_"

123

125

124getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

126getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

125getPArgNames (PPi plicity name ty body) ds =

127getPArgNames (PPi plicity name ty body) ds =

src/Idris/REPLParser.hs+1−1

@@ -50,7 +50,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

50 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

51 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

52 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

53− <|> try (do cmd ["doc"]; n <- P.fnName; eof; return (DocStr n))

53+ <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr n))

54 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

55 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

56 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))