Agda.Main

Agda main module.

Documentation

builtinBackends :: [Backend]

runAgda :: [Backend] -> IO ()

The main function

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

defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM ()

runAgdaWithOptions

Arguments

:: [Backend]

Backends only for printing usage and version information

-> TCM ()

HTML generating action

-> (TCM (Maybe Interface) -> TCM a)

Backend interaction

-> String

program name

-> CommandLineOptions

parsed command line options

-> TCM (Maybe a)

Run Agda with parsed command line options and with a custom HTML generator

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

Print usage information.

backendUsage :: Backend -> String

printVersion :: [Backend] -> IO ()

Print version information.

optionError :: String -> IO ()

What to do for bad options.

runTCMPrettyErrors :: TCM () -> IO ()

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

main :: IO ()

Main