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




data Target Source

Does the operation apply to the persistent options or only to the pragma options? In the former case the pragma options are also updated.

setCommandLineOptions :: MonadTCM tcm => Target -> CommandLineOptions -> tcm ()Source

Sets the command line options.

Ensures that the optInputFile field contains an absolute path.

An empty list of include directories is interpreted as [.].

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

Disable display forms.

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

Disable display forms.

displayFormsEnabled :: MonadTCM tcm => tcm BoolSource

Check if display forms are enabled.

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

Don't reify interaction points

getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]Source

Gets the include directories.

makeIncludeDirsAbsolute :: MonadTCM tcm => AbsolutePath -> tcm ()Source

Makes the include directories absolute.

Relative directories are made absolute with respect to the given path.

getInputFile :: MonadTCM tcm => tcm FilePathSource

Should only be run if hasInputFile.

setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm aSource

verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()Source

Precondition: The level must be non-negative.

reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()Source

reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()Source