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

Agda.TypeChecking.Monad.Options

Synopsis

setCommandLineOptions :: MonadTCM tcm => 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 [FilePath] setInputFile :: MonadTCM tcm => FilePath -> tcm () getInputFile :: MonadTCM tcm => tcm FilePath hasInputFile :: MonadTCM tcm => tcm Bool proofIrrelevance :: 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

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

Sets the command line options. Ensures that the optInputFile field contains an absolute path.

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 [FilePath] Source

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

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