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

Safe Haskell	None
Language	Haskell98

Agda.Compiler.MAlonzo.Primitives

Synopsis

Documentation

checkTypeOfMain :: QName -> Type -> TCM [Decl] -> TCM [Decl] Source

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

importsForPrim :: TCM [ModuleName] Source

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

primBody :: String -> TCM Exp Source

noCheckCover :: QName -> TCM Bool Source

pconName :: String -> TCM String Source

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