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




type Flag opts = opts -> Either String optsSource

The default output directory for HTML.

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

checkOpts :: Flag CommandLineOptionsSource

Checks that the given options are consistent.

parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptionsSource

Parse options from an options pragma.

parsePluginOptions :: String -> [String] -> opts -> [OptDescr (Flag opts)] -> Either String optsSource

Parse options for a plugin.

standardOptions_ :: [OptDescr ()]Source

Used for printing usage info.

isLiterate :: FilePath -> BoolSource

This should probably go somewhere else.

mapFlag :: (String -> String) -> OptDescr a -> OptDescr aSource

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> StringSource

The usage info message. The argument is the program name (probably agdaLight).