Agda-2.5.1: A dependently typed functional programming language and proof assistant
Agda.Compiler.MAlonzo.Primitives
Synopsis
checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl] Source
Check that the main function has type IO a, for some a.
importsForPrim :: TCM [ModuleName] Source
xForPrim :: [(String, TCM [a])] -> TCM [a] Source
primBody :: String -> TCM Exp Source
noCheckCover :: QName -> TCM Bool Source
pconName :: String -> TCM String Source
bltQual' :: String -> String -> TCM String Source