Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.MAlonzo.Primitives
Synopsis
checkTypeOfMain :: QName -> Type -> TCM ()
importsForPrim :: TCM [ModuleName]
declsForPrim :: TCM [Decl]
xForPrim :: [(String, TCM [a])] -> TCM [a]
primBody :: String -> TCM Exp
pconName :: String -> TCM String
hasCompiledData :: [String] -> TCM Bool
Documentation
checkTypeOfMain :: QName -> Type -> TCM ()Source
Check that the main function has type IO a, for some a.
importsForPrim :: TCM [ModuleName]Source
declsForPrim :: TCM [Decl]Source
xForPrim :: [(String, TCM [a])] -> TCM [a]Source
primBody :: String -> TCM ExpSource
pconName :: String -> TCM StringSource
hasCompiledData :: [String] -> TCM BoolSource
Produced by Haddock version 2.6.1