ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.MAlonzo.Primitives

Synopsis

newtypenewtype MainFunctionDef

datadata CheckedMainFunctionDef

valueasMainFunctionDef :: Definition -> Maybe MainFunctionDef

valuemainFunctionDefs :: Interface -> [MainFunctionDef]

valuecheckTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)

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

valuecheckTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef

valuetreelessPrimName :: TPrim -> String

valueimportsForPrim :: BuiltinThings -> [Definition] -> [ModuleName]

Haskell modules to be imported for BUILT-INs

valuexForPrim :: Map SomeBuiltin a -> BuiltinThings -> [Definition] -> [a]

valueprimBody :: MonadTCError m => PrimitiveId -> m Exp

Definition bodies for primitive functions

valuenoCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool