Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 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
getVerbosity :: MonadTCM tcm => tcm (Trie String Int)Source
type VerboseKey = StringSource
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.6.0