git.iko.soy/Idris-dev
on master help sign in
Make top level type 'Type*'
7cc7c32Edwin Brady
src/Idris/Core/TT.hs+5−1
compare with master
unifiedsplit
@@ -594,7 +594,11 @@ constDocs (B64V v) = "A vector of sixty-four-bit values"
594constDocs prim = "Undocumented"
594constDocs prim = "Undocumented"
595
595
596data Universe = UniqueType | AllTypes
596data Universe = UniqueType | AllTypes
597− deriving (Show, Eq, Ord)
597+ deriving (Eq, Ord)
598+
599+instance Show Universe where
600+ show UniqueType = "UniqueType"
601+ show AllTypes = "Type*"
598
602
599data Raw = Var Name
603data Raw = Var Name
600 | RBind Name (Binder Raw) Raw
604 | RBind Name (Binder Raw) Raw
src/Idris/ParseExpr.hs+1−1
@@ -307,9 +307,9 @@ simpleExpr syn =
307 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
307 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
308 <|> proofExpr syn
308 <|> proofExpr syn
309 <|> tacticsExpr syn
309 <|> tacticsExpr syn
310+ <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
310 <|> do reserved "Type"; return PType
311 <|> do reserved "Type"; return PType
311 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
312 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
312− <|> do reserved "AllTypes"; return $ PUniverse AllTypes
313 <|> do c <- constant
313 <|> do c <- constant
314 fc <- getFC
314 fc <- getFC
315 return (modifyConst syn fc (PConstant c))
315 return (modifyConst syn fc (PConstant c))