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

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 ()

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

importsForPrim :: TCM [ModuleName]

declsForPrim :: TCM [Decl]

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

primBody :: String -> TCM Exp

pconName :: String -> TCM String

hasCompiledData :: [String] -> TCM Bool