Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.MAlonzo.Primitives

Synopsis

- 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]

Check that the main function has type IO a, for some a.

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