ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Options.Lenses

Lenses for CommandLineOptions and PragmaOptions.

Add as needed.

Nothing smart happening here.

2 types
6 classes
19 values

PackageAgda-2.7.0.1
Exports27
LanguageHaskell2010
LicenceMIT
SourceLenses.hs

Pragma options

2 declarations

classclass LensPragmaOptions a where

Methods

getPragmaOptions :: a -> PragmaOptions
setPragmaOptions :: PragmaOptions -> a -> a
mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> a -> a
lensPragmaOptions :: Lens' a PragmaOptions

Instances2LensPragmaOptions

LensPragmaOptions CommandLineOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensPragmaOptions TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifyPragmaOptions

:: MonadTCState m
=> PragmaOptions -> PragmaOptions
-> m ()

Verbosity in the local pragma options

classclass LensVerbosity a where

Methods

getVerbosity :: a -> Verbosity
setVerbosity :: Verbosity -> a -> a
mapVerbosity :: (Verbosity -> Verbosity) -> a -> a

Instances2LensVerbosity

LensVerbosity PragmaOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensVerbosity TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifyVerbosity :: MonadTCState m => (Verbosity -> Verbosity) -> m ()

valueputVerbosity :: MonadTCState m => Verbosity -> m ()

Command line options

2 declarations

classclass LensCommandLineOptions a where

Methods

getCommandLineOptions :: a -> CommandLineOptions
setCommandLineOptions :: CommandLineOptions -> a -> a
mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> a -> a

Instances2LensCommandLineOptions

LensCommandLineOptions PersistentTCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensCommandLineOptions TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifyCommandLineOptions

:: MonadTCState m
=> CommandLineOptions -> CommandLineOptions
-> m ()

Safe mode

typetype SafeMode = Bool

classclass LensSafeMode a where

Methods

getSafeMode :: a -> SafeMode
setSafeMode :: SafeMode -> a -> a
mapSafeMode :: (SafeMode -> SafeMode) -> a -> a

Instances4LensSafeMode

LensSafeMode CommandLineOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensSafeMode PragmaOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensSafeMode PersistentTCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensSafeMode TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifySafeMode :: MonadTCState m => (SafeMode -> SafeMode) -> m ()

valueputSafeMode :: MonadTCState m => SafeMode -> m ()

valuebuiltinModulesWithSafePostulates :: Set FilePath

These builtins may use postulates, and are still considered --safe

valuebuiltinModulesWithUnsafePostulates :: Set FilePath

These builtins may not use postulates under --safe. They are not automatically unsafe, but will be if they use an unsafe feature.

valueprimitiveModules :: Set FilePath

valuebuiltinModules :: Set FilePath

valueisPrimitiveModule :: MonadIO m => FilePath -> m Bool

valueisBuiltinModule :: MonadIO m => FilePath -> m Bool

valueisBuiltinModuleWithSafePostulates :: MonadIO m => FilePath -> m Bool

Include directories

classclass LensIncludePaths a where

Methods

getIncludePaths :: a -> [FilePath]
setIncludePaths :: [FilePath] -> a -> a
mapIncludePaths :: ([FilePath] -> [FilePath]) -> a -> a
getAbsoluteIncludePaths :: a -> [AbsolutePath]
setAbsoluteIncludePaths :: [AbsolutePath] -> a -> a
mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> a -> a

Instances3LensIncludePaths

LensIncludePaths CommandLineOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensIncludePaths PersistentTCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensIncludePaths TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifyIncludePaths :: MonadTCState m => ([FilePath] -> [FilePath]) -> m ()

valueputIncludePaths :: MonadTCState m => [FilePath] -> m ()

valuemodifyAbsoluteIncludePaths

:: MonadTCState m
=> [AbsolutePath] -> [AbsolutePath]
-> m ()

valueputAbsoluteIncludePaths :: MonadTCState m => [AbsolutePath] -> m ()

Include directories

typetype PersistentVerbosity = Verbosity

classclass LensPersistentVerbosity a where

Methods

getPersistentVerbosity :: a -> PersistentVerbosity
setPersistentVerbosity :: PersistentVerbosity -> a -> a
mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> a -> a

Instances4LensPersistentVerbosity

LensPersistentVerbosity CommandLineOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensPersistentVerbosity PragmaOptionsDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensPersistentVerbosity PersistentTCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses
LensPersistentVerbosity TCStateDefined in Agda-2.7.0.1 · Agda.Interaction.Options.Lenses

valuemodifyPersistentVerbosity

:: MonadTCState m
=> PersistentVerbosity -> PersistentVerbosity
-> m ()

valueputPersistentVerbosity :: MonadTCState m => PersistentVerbosity -> m ()