| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Compiler.MAlonzo.Primitives

Synopsis

checkTypeOfMain :: QName -> Type -> TCM ()
importsForPrim :: TCM [Module]
declsForPrim :: TCM [HsDecl]
xForPrim :: [(String, TCM [a])] -> TCM [a]
primBody :: String -> TCM HsExp
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 [Module] | Source

declsForPrim :: TCM [HsDecl] | Source

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

primBody :: String -> TCM HsExp | Source

pconName :: String -> TCM String | Source

hasCompiledData :: [String] -> TCM Bool | Source

Produced by Haddock version 2.4.2