| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Primitives
Synopsis
- newtype MainFunctionDef = MainFunctionDef Definition
- data CheckedMainFunctionDef = CheckedMainFunctionDef {}
- asMainFunctionDef :: Definition -> Maybe MainFunctionDef
- mainFunctionDefs :: Interface -> [MainFunctionDef]
- checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
- checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
- treelessPrimName :: TPrim -> String
- importsForPrim :: BuiltinThings -> [Definition] -> [ModuleName]
- xForPrim :: Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a]
- primBody :: MonadTCError m => PrimitiveId -> m Exp
- noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool
Documentation
newtype MainFunctionDef Source #
Constructors
| MainFunctionDef Definition |
data CheckedMainFunctionDef Source #
Constructors
| CheckedMainFunctionDef | |
Fields | |
mainFunctionDefs :: Interface -> [MainFunctionDef] Source #
checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef) Source #
Check that the main function has type IO a, for some a.
treelessPrimName :: TPrim -> String Source #
importsForPrim :: BuiltinThings -> [Definition] -> [ModuleName] Source #
Haskell modules to be imported for BUILT-INs
xForPrim :: Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a] Source #
primBody :: MonadTCError m => PrimitiveId -> m Exp Source #
Definition bodies for primitive functions
noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool Source #