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