Agda.Compiler.MAlonzo.Primitives
Documentation
checkTypeOfMain :: QName -> Type -> TCM ()
Check that the main function has type IO a, for some a.
importsForPrim :: TCM [ModuleName]
declsForPrim :: TCM [Decl]
hasCompiledData :: [String] -> TCM Bool
Agda-2.3.0: A dependently typed functional programming language and proof assistant
Agda.Compiler.MAlonzo.Primitives
checkTypeOfMain :: QName -> Type -> TCM ()
Check that the main function has type IO a, for some a.
importsForPrim :: TCM [ModuleName]
declsForPrim :: TCM [Decl]
hasCompiledData :: [String] -> TCM Bool