Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




setPragmaOptions :: PragmaOptions -> TCM ()Source

Sets the pragma options.

setCommandLineOptions :: CommandLineOptions -> TCM ()Source

Sets the command line options (both persistent and pragma options are updated).

Relative include directories are made absolute with respect to the current working directory. If the include directories have changed (and were previously Right something), then the state is reset (completely) .

An empty list of relative include directories (Left []) is interpreted as [.].

pragmaOptions :: TCM PragmaOptionsSource

Returns the pragma options which are currently in effect.

commandLineOptions :: TCM CommandLineOptionsSource

Returns the command line options which are currently in effect.

enableDisplayForms :: TCM a -> TCM aSource

Disable display forms.

disableDisplayForms :: TCM a -> TCM aSource

Disable display forms.

displayFormsEnabled :: TCM BoolSource

Check if display forms are enabled.

dontEtaContractImplicit :: TCM a -> TCM aSource

Don't eta contract implicit

doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm aSource

Do eta contract implicit

dontReifyInteractionPoints :: TCM a -> TCM aSource

Don't reify interaction points

getIncludeDirs :: TCM [AbsolutePath]Source

Gets the include directories.

Precondition: optIncludeDirs must be Right something.

data RelativeTo Source

Which directory should form the base of relative include paths?


ProjectRoot AbsolutePath

The root directory of the "project" containing the given file. The file needs to be syntactically correct, with a module name matching the file name.


The current working directory.



:: [FilePath]

New include directories.

-> RelativeTo

How should relative paths be interpreted?

-> TCM () 

Makes the given directories absolute and stores them as include directories.

If the include directories change (and they were previously Right something), then the state is reset (completely, except for the include directories and stInteractionOutputCallback).

An empty list is interpreted as [.].

withShowAllArguments :: TCM a -> TCM aSource

Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.



:: String

The debug message.

-> TCM String 

If this command is run under the Emacs mode, then it formats the debug message in such a way that the Emacs mode can understand it.

displayDebugMessage :: String -> TCM ()Source

Displays a debug message in a suitable way.

verboseS :: VerboseKey -> Int -> TCM () -> TCM ()Source

Precondition: The level must be non-negative.