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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.MAlonzo.Primitives

Synopsis

- isMainFunction :: QName -> Defn -> Bool
- hasMainFunction :: Interface -> IsMain
- checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl]
- treelessPrimName :: TPrim -> String
- importsForPrim :: TCM [ModuleName]
- xForPrim :: [(String, TCM [a])] -> TCM [a]
- primBody :: String -> TCM Exp
- noCheckCover :: QName -> TCM Bool
- pconName :: String -> TCM String
- bltQual' :: String -> String -> TCM String

# Documentation

isMainFunction :: QName -> Defn -> Bool Source #

hasMainFunction :: Interface -> IsMain Source #

checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl] Source #

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

treelessPrimName :: TPrim -> String Source #

importsForPrim :: TCM [ModuleName] Source #

Haskell modules to be imported for BUILT-INs

xForPrim :: [(String, TCM [a])] -> TCM [a] Source #

primBody :: String -> TCM Exp Source #

Definition bodies for primitive functions

noCheckCover :: QName -> TCM Bool Source #

pconName :: String -> TCM String Source #

bltQual' :: String -> String -> TCM String Source #