Agda.TypeChecking.Monad.Options
- data Target
- 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
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 CommandLineOptionsSource
setOptionsFromPragma :: MonadTCM tcm => Pragma -> tcm ()Source
setOptionsFromPragmas :: MonadTCM tcm => [Pragma] -> tcm ()Source
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
shouldReifyInteractionPoints :: MonadTCM tcm => tcm BoolSource
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 FilePathSource
Should only be run if hasInputFile.
hasInputFile :: MonadTCM tcm => tcm BoolSource
proofIrrelevance :: MonadTCM tcm => tcm BoolSource
hasUniversePolymorphism :: MonadTCM tcm => tcm BoolSource
showImplicitArguments :: MonadTCM tcm => tcm BoolSource
setShowImplicitArguments :: MonadTCM tcm => Bool -> tcm a -> tcm aSource
ignoreInterfaces :: MonadTCM tcm => tcm BoolSource
positivityCheckEnabled :: MonadTCM tcm => tcm BoolSource
typeInType :: MonadTCM tcm => tcm BoolSource
type VerboseKey = StringSource
verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()Source
Precondition: The level must be non-negative.
reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> tcm Doc -> tcm ()Source