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