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

Safe HaskellNone
LanguageHaskell98

Agda.Main

Description

Agda main module.

Synopsis

Documentation

runAgda :: TCM ()

The main function

runAgdaWithOptions

Arguments

:: TCM ()

HTML generating action

-> String

program name

-> CommandLineOptions

parsed command line options

-> TCM () 

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

printUsage :: IO ()

Print usage information.

printVersion :: 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