Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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 #

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

The main function

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

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

runAgdaWithOptions 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

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

Print usage information.

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.

main :: IO () Source #

Main