| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Primitives
Synopsis
- isMainFunction :: QName -> Defn -> Bool
- hasMainFunction :: IsMain -> Interface -> IsMain
- checkTypeOfMain :: IsMain -> QName -> Definition -> 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
Arguments
| :: IsMain | Are we looking at the main module? |
| -> Interface | The module. |
| -> IsMain | Did we find a "main" function? |
Check for "main" function, but only in the main module.
checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl] Source #
Check that the main function has type IO a, for some a.
treelessPrimName :: TPrim -> String Source #
importsForPrim :: TCM [ModuleName] Source #
Haskell modules to be imported for BUILT-INs