- setPragmaOptions :: PragmaOptions -> TCM ()
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- pragmaOptions :: TCM PragmaOptions
- commandLineOptions :: TCM CommandLineOptions
- setOptionsFromPragma :: OptionsPragma -> TCM ()
- enableDisplayForms :: TCM a -> TCM a
- disableDisplayForms :: TCM a -> TCM a
- displayFormsEnabled :: TCM Bool
- dontEtaContractImplicit :: TCM a -> TCM a
- doEtaContractImplicit :: MonadTCM tcm => tcm a -> tcm a
- shouldEtaContractImplicit :: TCM Bool
- dontReifyInteractionPoints :: TCM a -> TCM a
- shouldReifyInteractionPoints :: TCM Bool
- getIncludeDirs :: TCM [AbsolutePath]
- data RelativeTo
- setIncludeDirs :: [FilePath] -> RelativeTo -> TCM ()
- setInputFile :: FilePath -> TCM ()
- getInputFile :: TCM AbsolutePath
- hasInputFile :: TCM Bool
- proofIrrelevance :: TCM Bool
- hasUniversePolymorphism :: TCM Bool
- showImplicitArguments :: TCM Bool
- setShowImplicitArguments :: Bool -> TCM a -> TCM a
- ignoreInterfaces :: TCM Bool
- positivityCheckEnabled :: TCM Bool
- typeInType :: TCM Bool
- getVerbosity :: TCM (Trie String Int)
- type VerboseKey = String
- hasVerbosity :: VerboseKey -> Int -> TCM Bool
- verboseS :: VerboseKey -> Int -> TCM () -> TCM ()
- reportS :: VerboseKey -> Int -> String -> TCM ()
- reportSLn :: VerboseKey -> Int -> String -> TCM ()
- reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM ()
- verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM a
Documentation
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
), then the state is reset
(completely) .
Right
something
An empty list of relative include directories (
) is
interpreted as Left
[][.]
.
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. |
CurrentDir | The current working directory. |
:: [FilePath] | New include directories. |
-> RelativeTo | How should relative paths be interpreted? |
-> TCM () |
setInputFile :: FilePath -> TCM ()Source
getInputFile :: TCM AbsolutePathSource
Should only be run if hasInputFile
.
setShowImplicitArguments :: Bool -> TCM a -> TCM aSource
type VerboseKey = StringSource
hasVerbosity :: VerboseKey -> Int -> TCM BoolSource
verboseS :: VerboseKey -> Int -> TCM () -> TCM ()Source
Precondition: The level must be non-negative.
reportSDoc :: VerboseKey -> Int -> TCM Doc -> TCM ()Source
verboseBracket :: VerboseKey -> Int -> String -> TCM a -> TCM aSource