| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Options

Synopsis

data Target

= PersistentOptions
| PragmaOptions

setCommandLineOptions :: MonadTCM tcm => Target -> CommandLineOptions -> tcm ()
commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions
setOptionsFromPragma :: MonadTCM tcm => Pragma -> tcm ()
setOptionsFromPragmas :: MonadTCM tcm => [Pragma] -> tcm ()
enableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
disableDisplayForms :: MonadTCM tcm => tcm a -> tcm a
displayFormsEnabled :: MonadTCM tcm => tcm Bool
dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm a
shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool
getIncludeDirs :: MonadTCM tcm => tcm [AbsolutePath]
makeIncludeDirsAbsolute :: MonadTCM tcm => AbsolutePath -> tcm ()
setInputFile :: MonadTCM tcm => FilePath -> tcm ()
getInputFile :: MonadTCM tcm => tcm FilePath
hasInputFile :: MonadTCM tcm => tcm Bool
proofIrrelevance :: MonadTCM tcm => tcm Bool
hasUniversePolymorphism :: MonadTCM tcm => tcm Bool
showImplicitArguments :: MonadTCM tcm => tcm Bool
setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm a
ignoreInterfaces :: MonadTCM tcm => tcm Bool
positivityCheckEnabled :: MonadTCM tcm => tcm Bool
typeInType :: MonadTCM tcm => tcm Bool
getVerbosity :: MonadTCM tcm => tcm (Trie String Int)
type VerboseKey = String
verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
reportS :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()

Documentation

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.
Constructors

PersistentOptions |
PragmaOptions |

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 `[.]`.

commandLineOptions :: MonadTCM tcm => tcm CommandLineOptions | Source

setOptionsFromPragma :: MonadTCM tcm => Pragma -> tcm () | Source

setOptionsFromPragmas :: MonadTCM tcm => [Pragma] -> tcm () | Source

enableDisplayForms :: MonadTCM tcm => tcm a -> tcm a | Source

Disable display forms.

disableDisplayForms :: MonadTCM tcm => tcm a -> tcm a | Source

Disable display forms.

displayFormsEnabled :: MonadTCM tcm => tcm Bool | Source

Check if display forms are enabled.

dontReifyInteractionPoints :: MonadTCM tcm => tcm a -> tcm a | Source

Don't reify interaction points

shouldReifyInteractionPoints :: MonadTCM tcm => tcm Bool | Source

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.

setInputFile :: MonadTCM tcm => FilePath -> tcm () | Source

getInputFile :: MonadTCM tcm => tcm FilePath | Source

Should only be run if `hasInputFile`.

hasInputFile :: MonadTCM tcm => tcm Bool | Source

proofIrrelevance :: MonadTCM tcm => tcm Bool | Source

hasUniversePolymorphism :: MonadTCM tcm => tcm Bool | Source

showImplicitArguments :: MonadTCM tcm => tcm Bool | Source

setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm a | Source

ignoreInterfaces :: MonadTCM tcm => tcm Bool | Source

positivityCheckEnabled :: MonadTCM tcm => tcm Bool | Source

typeInType :: MonadTCM tcm => tcm Bool | Source

getVerbosity :: MonadTCM tcm => tcm (Trie String Int) | Source

type VerboseKey = String | Source

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

Precondition: The level must be non-negative.

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

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

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

Produced by Haddock version 2.4.2