Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.MAlonzo.Primitives

Synopsis

Documentation

checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef) Source #

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

importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName] Source #

Haskell modules to be imported for BUILT-INs

primBody :: MonadTCError m => PrimitiveId -> m Exp Source #

Definition bodies for primitive functions