Agda-2.5.4: A dependently typed functional programming language and proof assistant

Safe Haskell	None
Language	Haskell2010

Agda.Compiler.MAlonzo.Primitives

Synopsis

isMainFunction :: QName -> Bool
hasMainFunction :: Interface -> IsMain
checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl]
treelessPrimName :: TPrim -> String
importsForPrim :: TCM [ModuleName]
xForPrim :: [(String, TCM [a])] -> TCM [a]
primBody :: String -> TCM Exp
noCheckCover :: QName -> TCM Bool
pconName :: String -> TCM String
bltQual' :: String -> String -> TCM String

Documentation

isMainFunction :: QName -> Bool #

hasMainFunction :: Interface -> IsMain #

checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl] #

Check that the main function has type IO a, for some a.

treelessPrimName :: TPrim -> String #

importsForPrim :: TCM [ModuleName] #

Haskell modules to be imported for BUILT-INs

xForPrim :: [(String, TCM [a])] -> TCM [a] #

primBody :: String -> TCM Exp #

Definition bodies for primitive functions

noCheckCover :: QName -> TCM Bool #

pconName :: String -> TCM String #

bltQual' :: String -> String -> TCM String #