| Safe Haskell | None |
|---|
Agda.Compiler.MAlonzo.Primitives
- checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl]
- importsForPrim :: TCM [ModuleName]
- declsForPrim :: TCM [Decl]
- mazNatToInteger :: [Char]
- mazIntegerToNat :: [Char]
- mazNatToInt :: [Char]
- mazIntToNat :: [Char]
- mazCharToInteger :: [Char]
- mazListToHList :: [Char]
- mazHListToList :: [Char]
- mazListToString :: [Char]
- mazStringToList :: [Char]
- mazBoolToHBool :: [Char]
- mazHBoolToBool :: [Char]
- xForPrim :: [(String, TCM [a])] -> TCM [a]
- primBody :: String -> TCM Exp
- repl :: [[Char]] -> [Char] -> [Char]
- pconName :: String -> TCM String
- hasCompiledData :: [String] -> TCM Bool
- bltQual' :: String -> String -> TCMT IO String
Documentation
checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl]Source
Check that the main function has type IO a, for some a.
declsForPrim :: TCM [Decl]Source
mazNatToInt :: [Char]Source
mazIntToNat :: [Char]Source
mazListToHList :: [Char]Source
mazHListToList :: [Char]Source
mazBoolToHBool :: [Char]Source
mazHBoolToBool :: [Char]Source
hasCompiledData :: [String] -> TCM BoolSource