Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Main

Description

Agda main module.

Synopsis

Documentation

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

The main function

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.

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