7875005 · Idris-dev · git.iko.soy

src/Core/TT.hs+1

compare with master

unifiedsplit

@@ -210,6 +210,7 @@ instance Pretty Name where

210instance Show Name where

211 show (UN n) = n

212 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

213+ show (MN _ "underscore") = "_"

213 show (MN i s) = "{" ++ s ++ show i ++ "}"

214 show (MN i s) = "{" ++ s ++ show i ++ "}"

214 show NErased = "_"

215 show NErased = "_"

215

216

src/Idris/ElabDecls.hs+4

@@ -675,6 +675,10 @@ elabVal info aspat tm_in

675-- (build i info aspat (MN 0 "val") tm))

676 tclift (elaborate ctxt (MN 0 "val") infP []

677 (build i info aspat (MN 0 "val") (infTerm tm)))

678+ def' <- checkDef (FC "(input)" 0) defer

679+ addDeferred def'

680+ mapM_ (elabCaseBlock info) is

681+

678 logLvl 3 ("Value: " ++ show tm')

682 logLvl 3 ("Value: " ++ show tm')

679 recheckC (FC "(input)" 0) [] tm'

683 recheckC (FC "(input)" 0) [] tm'

680 let vtm = getInferTerm tm'

684 let vtm = getInferTerm tm'

src/Idris/Parser.hs+4−1

@@ -1077,11 +1077,14 @@ tyDeclList syn = try (sepBy1 (do x <- pfName

1077 t <- pTSig (noImp syn)

1078 return (map (\x -> (x, t)) ns)

1079

1080−tyOptDeclList syn = sepBy1 (do x <- pfName;

1080+tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder

1081 t <- option Placeholder (do lchar ':'

1082 pExpr syn)

1083 return (x,t))

1084 (lchar ',')

1085+ where pNameOrPlaceholder = pfName

1086+ <|> do symbol "_"

1087+ return (MN 0 "underscore")

1085

1088

1086bindList b [] sc = sc

1089bindList b [] sc = sc

1087bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

1090bindList b ((n, t):bs) sc = b n t (bindList b bs sc)