| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Main
Description
Agda main module.
Synopsis
- builtinBackends :: [Backend]
- runAgda :: [Backend] -> IO ()
- runAgda' :: [Backend] -> IO ()
- defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM ()
- runAgdaWithOptions :: [Backend] -> TCM () -> (TCM (Maybe Interface) -> TCM a) -> String -> CommandLineOptions -> TCM (Maybe a)
- printUsage :: [Backend] -> Help -> IO ()
- backendUsage :: Backend -> String
- printVersion :: [Backend] -> IO ()
- optionError :: String -> IO ()
- runTCMPrettyErrors :: TCM () -> IO ()
- main :: IO ()
Documentation
builtinBackends :: [Backend] Source #
defaultInteraction :: CommandLineOptions -> TCM (Maybe Interface) -> TCM () Source #
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
backendUsage :: Backend -> String Source #
printVersion :: [Backend] -> 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.