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

Agda.Main

Description

Agda main module.

Synopsis

Documentation

runAgda :: [Backend] -> IO () Source #

The main function

runAgda' :: [Backend] -> IO () Source #

The main function without importing built-in backends

getMainMode :: MonadError String m => [Backend] -> Maybe AbsolutePath -> CommandLineOptions -> m MainMode Source #

Determine the main execution mode to run, based on the configured backends and command line options. | This is pure.

runAgdaWithOptions Source #

Arguments

:: Interactor a

Backend interaction

-> String

program name

-> CommandLineOptions

parsed command line options

-> TCM a 

Run Agda with parsed command line options

printUsage :: [Backend] -> Help -> IO () Source #

Print usage information.

printVersion :: [Backend] -> PrintAgdaVersion -> IO () Source #

Print version information.

optionError :: String -> IO () Source #

What to do for bad options.

runTCMPrettyErrors :: TCM () -> IO () Source #

Run a TCM action in IO; catch and pretty print errors.

helpForLocaleError :: TCErr -> IO () Source #

If the error is an IO error, and the error message suggests that the problem is related to locales or code pages, print out some extra information.