Agda.Interaction.Options · Agda-2.8.0.2

Note that --cubical and --erased-cubical are "jointly infective": if one of them is used in one module, then one or the other must be used in all modules that depend on this module.

valueinputFlag :: FilePath -> Flag CommandLineOptions

#

valuelensOptAllowExec

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptAllowIncompleteMatch

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptAllowUnsolved

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptAutoInline

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptBacktrackingInstances

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCaching

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCallByName

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCohesion

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCompileMain

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptConfluenceCheck

:: Functor f
=> Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCopatterns

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCountClusters

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCubical

#

valuelensOptCubicalCompatible

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptCumulativity

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptDoubleCheck

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptEraseRecordParameters

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptErasedMatches

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptErasure

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptEta

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptExactSplit

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptExperimentalIrrelevance

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptExperimentalLazyInstances

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptFastReduce

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptFirstOrder

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptFlatSplit

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptForcing

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptGuarded

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptGuardedness

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptHiddenArgumentPuns

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptImportSorts

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptInferAbsurdClauses

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptInjectiveTypeConstructors

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptInstanceSearchDepth

:: Functor f
=> Int -> f Int
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptInversionMaxDepth

:: Functor f
=> Int -> f Int
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptIrrelevantProjections

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptKeepCoveringClauses

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptKeepPatternVariables

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptLevelUniverse

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptLoadPrimitives

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptNoUniverseCheck

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptOmegaInOmega

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptPatternMatching

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptPolarity

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptPositivityCheck

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptPostfixProjections

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptPrintPatternSynonyms

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptProfiling

#

valuelensOptProjectionLike

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptProp

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptQualifiedInstances

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptRequireUniqueMetaSolutions

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptRewriting

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptSafe

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptSaveMetas

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptShowIdentitySubstitutions

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptShowImplicit

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptShowIrrelevant

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptSizedTypes

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptSyntacticEquality

:: Functor f
=> Maybe Int -> f (Maybe Int)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptTerminationCheck

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptTerminationDepth

:: Functor f
=> CutOff -> f CutOff
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptTwoLevel

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptUniverseCheck

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptUniversePolymorphism

:: Functor f
=> WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptUseUnicode

:: Functor f
=> WithDefault' UnicodeOrAscii 'True -> f (WithDefault' UnicodeOrAscii 'True)
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptVerbose

:: Functor f
=> Maybe (Trie VerboseKeyItem VerboseLevel) -> f (Maybe (Trie VerboseKeyItem VerboseLevel))
-> PragmaOptions
-> f PragmaOptions

#

valuelensOptWarningMode

#

valuelensOptWithoutK

:: Functor f
=> WithDefault' Bool 'False -> f (WithDefault' Bool 'False)
-> PragmaOptions
-> f PragmaOptions

#

valuemapFlag :: (String -> String) -> OptDescr a -> OptDescr a

#

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

valueoptAllowExec :: PragmaOptions -> Bool

#

valueoptAllowIncompleteMatch :: PragmaOptions -> Bool

#

valueoptAllowUnsolved :: PragmaOptions -> Bool

#

valueoptAutoInline :: PragmaOptions -> Bool

#

valueoptBacktrackingInstances :: PragmaOptions -> Bool

#

valueoptCaching :: PragmaOptions -> Bool

#

valueoptCallByName :: PragmaOptions -> Bool

#

valueoptCohesion :: PragmaOptions -> Bool

#

optCohesion is implied by optFlatSplit.

valueoptCompileNoMain :: PragmaOptions -> Bool

#

valueoptConfluenceCheck :: PragmaOptions -> Maybe ConfluenceCheck

#

valueoptCopatterns :: PragmaOptions -> Bool

#

valueoptCountClusters :: PragmaOptions -> Bool

#

valueoptCubical :: PragmaOptions -> Maybe Cubical

#

valueoptCubicalCompatible :: PragmaOptions -> Bool

#

valueoptCumulativity :: PragmaOptions -> Bool

#

valueoptDoubleCheck :: PragmaOptions -> Bool

#

valueoptEraseRecordParameters :: PragmaOptions -> Bool

#

valueoptErasedMatches :: PragmaOptions -> Bool

#

valueoptErasure :: PragmaOptions -> Bool

#

optErasure is implied by optEraseRecordParameters. optErasure is also implied by an explicitly given `--erased-matches`.

valueoptEta :: PragmaOptions -> Bool

#

valueoptExperimentalIrrelevance :: PragmaOptions -> Bool

#

valueoptFastReduce :: PragmaOptions -> Bool

#

valueoptFirstOrder :: PragmaOptions -> Bool

#

valueoptFlatSplit :: PragmaOptions -> Bool

#

valueoptForcedArgumentRecursion :: PragmaOptions -> Bool

#

valueoptForcing :: PragmaOptions -> Bool

#

valueoptGuarded :: PragmaOptions -> Bool

#

valueoptGuardedness :: PragmaOptions -> Bool

#

valueoptHiddenArgumentPuns :: PragmaOptions -> Bool

#

valueoptImportSorts :: PragmaOptions -> Bool

#

optImportSorts requires optLoadPrimitives.

valueoptInferAbsurdClauses :: PragmaOptions -> Bool

#

valueoptInjectiveTypeConstructors :: PragmaOptions -> Bool

#

valueoptInstanceSearchDepth :: PragmaOptions -> Int

#

valueoptInversionMaxDepth :: PragmaOptions -> Int

#

valueoptIrrelevantProjections :: PragmaOptions -> Bool

#

valueoptKeepCoveringClauses :: PragmaOptions -> Bool

#

valueoptKeepPatternVariables :: PragmaOptions -> Bool

#

valueoptLargeIndices :: PragmaOptions -> Bool

#

valueoptLevelUniverse :: PragmaOptions -> Bool

#

valueoptLoadPrimitives :: PragmaOptions -> Bool

#

valueoptOmegaInOmega :: PragmaOptions -> Bool

#

valueoptPatternMatching :: PragmaOptions -> Bool

#

valueoptPolarity :: PragmaOptions -> Bool

#

valueoptPositivityCheck :: PragmaOptions -> Bool

#

valueoptPostfixProjections :: PragmaOptions -> Bool

#

valueoptPrintPatternSynonyms :: PragmaOptions -> Bool

#

valueoptProfiling :: PragmaOptions -> ProfileOptions

#

valueoptProjectionLike :: PragmaOptions -> Bool

#

valueoptProp :: PragmaOptions -> Bool

#

valueoptQualifiedInstances :: PragmaOptions -> Bool

#

valueoptRequireUniqueMetaSolutions :: PragmaOptions -> Bool

#

valueoptRewriting :: PragmaOptions -> Bool

#

valueoptSafe :: PragmaOptions -> Bool

#

valueoptSaveMetas :: PragmaOptions -> Bool

#

valueoptShowGeneralized :: PragmaOptions -> Bool

#

valueoptShowIdentitySubstitutions :: PragmaOptions -> Bool

#

valueoptShowImplicit :: PragmaOptions -> Bool

#

valueoptShowIrrelevant :: PragmaOptions -> Bool

#

valueoptSizedTypes :: PragmaOptions -> Bool

#

valueoptSyntacticEquality :: PragmaOptions -> Maybe Int

#

valueoptTerminationCheck :: PragmaOptions -> Bool

#

valueoptTerminationDepth :: PragmaOptions -> CutOff

#

valueoptTwoLevel :: PragmaOptions -> Bool

#

valueoptUniverseCheck :: PragmaOptions -> Bool

#

valueoptUniversePolymorphism :: PragmaOptions -> Bool

#

valueoptUseUnicode :: PragmaOptions -> UnicodeOrAscii

#

valueoptVerbose :: PragmaOptions -> Maybe (Trie VerboseKeyItem VerboseLevel)

#

valueoptWarningMode :: PragmaOptions -> WarningMode

#

valueoptWithoutK :: PragmaOptions -> Bool

#

valueoptionWarningName :: OptionWarning -> WarningName

#

valueparsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts

#

Parse options for a plugin.

valueparsePragmaOptions

:: OptionsPragma
Pragma options.
-> CommandLineOptions
Command-line options which should be updated.
-> OptM PragmaOptions

#

Parse options from an options pragma.

valueparseVerboseKey :: VerboseKey -> [VerboseKeyItem]

#

valuerecheckBecausePragmaOptionsChanged

:: PragmaOptions
The options that were used to check the file.
-> PragmaOptions
The options that are currently in effect.
-> Bool

#

This function returns True if the file should be rechecked.

valuerunOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)

#

valuesafeFlag :: Flag PragmaOptions

#

valuestandardOptions :: [OptDescr (Flag CommandLineOptions)]

#

valuestandardOptions_ :: [OptDescr ()]

#

Used for printing usage info. Does not include the dead options.

valuestripRTS :: [String] -> [String]

#

Removes RTS options from a list of options.

valueunsafePragmaOptions :: PragmaOptions -> [String]

#

Check for unsafe pragmas. Gives a list of used unsafe flags.

valueusage :: [OptDescr ()] -> String -> Help -> String

#

The usage info message. The argument is the program name (probably agda).

valuedefaultCutOff :: CutOff

#

The default termination depth.

typetype Flag opts = opts -> OptM opts

#

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

datadata ImpliedPragmaOption where

#

Constructors

ImpliesPragmaOption :: String -> Bool -> (PragmaOptions -> WithDefault a) -> String -> Bool -> (PragmaOptions -> WithDefault b) -> ImpliedPragmaOption

datadata InfectiveCoinfectiveOption

#

Descriptions of infective and coinfective options.

Constructors

ICOption
- icOptionActive :: PragmaOptions -> Bool
  Is the option active?
- icOptionDescription :: String
  A description of the option (typically a flag that activates the option).
- icOptionKind :: InfectiveCoinfective
  Is the option (roughly speaking) infective or coinfective?
- icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
  This function returns True exactly when, from the perspective of the option in question, the options in the current module (the first argument) are compatible with the options in a given imported module (the second argument).
- icOptionWarning :: TopLevelModuleName -> Doc
  A warning message that should be used if this option is not used correctly. The given module name is the name of an imported module for which icOptionOK failed.

newtypenewtype OptM a

#

The options parse monad OptM collects warnings that are not discarded when a fatal error occurrs

Instances5Monad, Functor, Applicative, MonadError, MonadWriter

Monad OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
Functor OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
Applicative OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
MonadError OptionError OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
MonadWriter OptionWarnings OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base

typetype OptionError = String

#

datadata OptionWarning

#

Warnings when parsing options.

Constructors

OptionRenamed
Name of option changed in a newer version of Agda.
- oldOptionName :: String
- newOptionName :: String
WarningProblem WarningModeError
A problem with setting or unsetting a warning.

Instances7Show, Generic, NFData, Pretty, EmbPrj, MonadWriter, …

Show OptionWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
Generic OptionWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
NFData OptionWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
Pretty OptionWarningDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
EmbPrj OptionWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
MonadWriter OptionWarnings OptMDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Base
type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "OptionRenamed" 'PrefixI 'True) (S1 ('MetaSel ('Just "oldOptionName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "newOptionName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "WarningProblem" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningModeError)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Base

datadata CommandLineOptions

#

Constructors

Options
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
  The list should not contain duplicates.
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
  Use this (if Just) instead of ~/.agda/libraries.
- optDefaultLibs :: Bool
  Use ~/.agda/defaults.
- optUseLibs :: Bool
  look for .agda-lib files.
- optTraceImports :: Integer
  Configure notifications about imported modules.
- optTrustedExecutables :: Map ExeName FilePath
  Map names of trusted executables to absolute paths.
- optPrintAgdaDataDir :: Bool
- optPrintAgdaAppDir :: Bool
- optPrintVersion :: Maybe PrintAgdaVersion
- optPrintHelp :: Maybe Help
- optBuildLibrary :: Bool
  --build-library: Build all modules in the current library.
- optSetup :: Bool
  Force Agda to self-setup at startup.
- optEmacsMode :: Set EmacsModeCommand
  Emacs mode administration (formerly done by the agda-mode executable). Accepted subcommands: locate, setup, compile. Can be given several times, subcommands are accumulated in the set.
- optInteractive :: Bool
  Agda REPL (-I).
- optGHCiInteraction :: Bool
  --interaction mode.
- optJSONInteraction :: Bool
  --interaction-json mode.
- optExitOnError :: !Bool
  Exit if an interactive command fails.
- optCompileDir :: Maybe FilePath
  In the absence of a path the project root is used.
- optGenerateVimFile :: Bool
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool
  Should the top-level module only be scope-checked, and not type-checked?
- optTransliterate :: Bool
  Should code points that are not supported by the locale be transliterated?
- optDiagnosticsColour :: DiagnosticsColours
  Configure colour output.

Instances8Show, Generic, NFData, LensPragmaOptions, LensIncludePaths, LensPersistentVerbosity, …

Show CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensPragmaOptions CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensIncludePaths CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensPersistentVerbosity CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensSafeMode CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "Options" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "optProgramName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "optInputFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))) :*: ((S1 ('MetaSel ('Just "optAbsoluteIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath]) :*: S1 ('MetaSel ('Just "optLibraries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName])) :*: (S1 ('MetaSel ('Just "optOverrideLibrariesFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optDefaultLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optUseLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optTraceImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Just "optTrustedExecutables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ExeName FilePath)))) :*: ((S1 ('MetaSel ('Just "optPrintAgdaDataDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPrintAgdaAppDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optPrintVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe PrintAgdaVersion)) :*: S1 ('MetaSel ('Just "optPrintHelp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Help)))))) :*: (((S1 ('MetaSel ('Just "optBuildLibrary") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optSetup") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optEmacsMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set EmacsModeCommand)))) :*: ((S1 ('MetaSel ('Just "optInteractive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optGHCiInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optJSONInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optExitOnError") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)))) :*: (((S1 ('MetaSel ('Just "optCompileDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optGenerateVimFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optIgnoreInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optIgnoreAllInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optPragmaOptions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PragmaOptions) :*: S1 ('MetaSel ('Just "optOnlyScopeChecking") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optTransliterate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDiagnosticsColour") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DiagnosticsColours)))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata ConfluenceCheck

#

LocalConfluenceCheck GlobalConfluenceCheck

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
EmbPrj ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata DiagnosticsColours

#

AlwaysColour NeverColour AutoColour

Instances4Show, Generic, NFData, Rep

Show DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata EmacsModeCommand

#

If several --emacs-mode commands are given, they are executed in the order as given in this datatype.

Constructors

EmacsModeCompile
Compile the .el files to .elc.
EmacsModeSetup
Add the initialization lines to .emacs.
EmacsModeLocate
Print the installation location of agda2.el.

Instances6Eq, Ord, Show, Generic, NFData, Rep

Eq EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Ord EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata InfectiveCoinfective

#

Infective or coinfective?

Infective Coinfective

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
EmbPrj InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata PragmaOptions

#

Options which can be set in a pragma.

Constructors

PragmaOptions
- _optShowImplicit :: WithDefault 'False
- _optShowGeneralized :: WithDefault 'True
  Show generalized parameters in Pi types
- _optShowIrrelevant :: WithDefault 'False
- _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
- _optVerbose :: !Verbosity
- _optProfiling :: ProfileOptions
- _optProp :: WithDefault 'False
- _optLevelUniverse :: WithDefault 'False
- _optTwoLevel :: WithDefault 'False
- _optAllowUnsolved :: WithDefault 'False
- _optAllowIncompleteMatch :: WithDefault 'False
- _optPositivityCheck :: WithDefault 'True
- _optTerminationCheck :: WithDefault 'True
- _optTerminationDepth :: CutOff
  Cut off structural order comparison at some depth in termination checker?
- _optUniverseCheck :: WithDefault 'True
- _optOmegaInOmega :: WithDefault 'False
- _optCumulativity :: WithDefault 'False
- _optSizedTypes :: WithDefault 'False
- _optGuardedness :: WithDefault 'False
- _optInjectiveTypeConstructors :: WithDefault 'False
- _optUniversePolymorphism :: WithDefault 'True
- _optIrrelevantProjections :: WithDefault 'False
- _optExperimentalIrrelevance :: WithDefault 'False
  irrelevant levels, irrelevant data matching
- _optWithoutK :: WithDefault 'False
- _optCubicalCompatible :: WithDefault 'False
- _optCopatterns :: WithDefault 'True
  Allow definitions by copattern matching?
- _optPatternMatching :: WithDefault 'True
  Is pattern matching allowed in the current file?
- _optExactSplit :: WithDefault 'False
- _optHiddenArgumentPuns :: WithDefault 'False
  Should patterns of the form {x} or ⦃ x ⦄ be interpreted as puns?
- _optEta :: WithDefault 'True
- _optForcing :: WithDefault 'True
  Perform the forcing analysis on data constructors?
- _optProjectionLike :: WithDefault 'True
  Perform the projection-likeness analysis on functions?
- _optErasure :: WithDefault 'False
- _optErasedMatches :: WithDefault 'True
  Allow matching in erased positions for single-constructor, non-indexed data/record types. (This kind of matching is always allowed for record types with η-equality.)
- _optEraseRecordParameters :: WithDefault 'False
  Mark parameters of record modules as erased?
- _optRewriting :: WithDefault 'False
  Can rewrite rules be added and used?
- _optCubical :: Maybe Cubical
- _optGuarded :: WithDefault 'False
- _optFirstOrder :: WithDefault 'False
  Should we speculatively unify function applications as if they were injective? Implies optRequireUniqueMetaSolutions.
- _optRequireUniqueMetaSolutions :: WithDefault 'True
  Forbid non-unique meta solutions allowed. For instance from INJECTIVE_FOR_INFERENCE pragmas.
- _optPostfixProjections :: WithDefault 'True
  Should system generated projections ProjSystem be printed postfix (True) or prefix (False).
- _optKeepPatternVariables :: WithDefault 'True
  Should case splitting replace variables with dot patterns (False) or keep them as variables (True).
- _optInferAbsurdClauses :: WithDefault 'True
  Should case splitting and coverage checking try to discharge absurd clauses? Default: True, but False might make coverage checking considerably faster in some cases.
- _optInstanceSearchDepth :: Int
- _optBacktrackingInstances :: WithDefault 'False
- _optQualifiedInstances :: WithDefault 'True
  Should instance search consider instances with qualified names?
- _optInversionMaxDepth :: Int
- _optSafe :: WithDefault 'False
- _optDoubleCheck :: WithDefault 'False
- _optSyntacticEquality :: !Maybe Int
  Should the conversion checker use the syntactic equality shortcut? Nothing means that it should. Just n, for a non-negative number n, means that syntactic equality checking gets n units of fuel. If the fuel becomes zero, then syntactic equality checking is turned off. The fuel counter is decreased in the failure continuation of checkSyntacticEquality.
- _optWarningMode :: WarningMode
- _optCompileMain :: WithDefault 'True
  Treat the module given at the command line or via interaction as main module in compilation?
- _optCaching :: WithDefault 'True
- _optCountClusters :: WithDefault 'False
  Count extended grapheme clusters rather than code points when generating LaTeX.
- _optAutoInline :: WithDefault 'False
  Automatic compile-time inlining for simple definitions (unless marked NOINLINE).
- _optPrintPatternSynonyms :: WithDefault 'True
- _optFastReduce :: WithDefault 'True
  Use the Agda abstract machine (fastReduce)?
- _optCallByName :: WithDefault 'False
  Use call-by-name instead of call-by-need.
- _optConfluenceCheck :: Maybe ConfluenceCheck
  Check confluence of rewrite rules?
- _optCohesion :: WithDefault 'False
  Are the cohesion modalities available?
- _optFlatSplit :: WithDefault 'False
  Can we split on a (@flat x : A) argument?
- _optPolarity :: WithDefault 'False
  Can we use modal polarities (++, +, etc.)?
- _optImportSorts :: WithDefault 'True
  Should every top-level module start with an implicit statement open import Agda.Primitive using (Set; Prop)?
- _optLoadPrimitives :: WithDefault 'True
  Should we load the primitive modules at all? This is a stronger form of optImportSorts.
- _optAllowExec :: WithDefault 'False
  Allow running external executables from meta programs.
- _optSaveMetas :: WithDefault 'False
  Save meta-variables to interface files.
- _optShowIdentitySubstitutions :: WithDefault 'False
  Show identity substitutions when pretty-printing terms (i.e. always show all arguments of a metavariable).
- _optKeepCoveringClauses :: WithDefault 'False
  Do not discard clauses constructed by the coverage checker (needed for some external backends).
- _optLargeIndices :: WithDefault 'False
  Allow large indices, and large forced arguments in constructors.
- _optForcedArgumentRecursion :: WithDefault 'True
  Allow recursion on forced constructor arguments.
- _optExperimentalLazyInstances :: WithDefault 'False
  Defer instance search based on discrimination tree results

Instances9Eq, Show, Generic, NFData, LensPersistentVerbosity, LensSafeMode, …

Eq PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensPersistentVerbosity PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensSafeMode PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensVerbosity PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
EmbPrj PragmaOptionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "PragmaOptions" 'PrefixI 'True) ((((((S1 ('MetaSel ('Just "_optShowImplicit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optShowGeneralized") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optShowIrrelevant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optUseUnicode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault' UnicodeOrAscii 'True)))) :*: ((S1 ('MetaSel ('Just "_optVerbose") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Verbosity) :*: S1 ('MetaSel ('Just "_optProfiling") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProfileOptions)) :*: (S1 ('MetaSel ('Just "_optProp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optLevelUniverse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :*: (((S1 ('MetaSel ('Just "_optTwoLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optAllowUnsolved") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optAllowIncompleteMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optTerminationDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CutOff)) :*: (S1 ('MetaSel ('Just "_optUniverseCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: (S1 ('MetaSel ('Just "_optOmegaInOmega") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCumulativity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))))) :*: ((((S1 ('MetaSel ('Just "_optSizedTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optGuardedness") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optInjectiveTypeConstructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optUniversePolymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optIrrelevantProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optExperimentalIrrelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optWithoutK") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optCubicalCompatible") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCopatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))))) :*: (((S1 ('MetaSel ('Just "_optPatternMatching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optExactSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optHiddenArgumentPuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optEta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optForcing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optProjectionLike") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optErasure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optErasedMatches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optEraseRecordParameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))))))) :*: (((((S1 ('MetaSel ('Just "_optRewriting") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCubical") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Cubical))) :*: (S1 ('MetaSel ('Just "_optGuarded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optFirstOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optRequireUniqueMetaSolutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optPostfixProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optKeepPatternVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: (S1 ('MetaSel ('Just "_optInferAbsurdClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optInstanceSearchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :*: (((S1 ('MetaSel ('Just "_optBacktrackingInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optQualifiedInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optInversionMaxDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "_optSafe") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optDoubleCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optSyntacticEquality") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Int))) :*: (S1 ('MetaSel ('Just "_optWarningMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningMode) :*: (S1 ('MetaSel ('Just "_optCompileMain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optCaching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))))))) :*: ((((S1 ('MetaSel ('Just "_optCountClusters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optAutoInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optPrintPatternSynonyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optFastReduce") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optCallByName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optConfluenceCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ConfluenceCheck))) :*: (S1 ('MetaSel ('Just "_optCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optFlatSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optPolarity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))))) :*: (((S1 ('MetaSel ('Just "_optImportSorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optLoadPrimitives") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optAllowExec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optSaveMetas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optShowIdentitySubstitutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optKeepCoveringClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optLargeIndices") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optForcedArgumentRecursion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optExperimentalLazyInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata PrintAgdaVersion

#

Options --version and --numeric-version (last wins).

Constructors

PrintAgdaVersion
Print Agda version information.
PrintAgdaNumericVersion
Print Agda version number.

Instances4Show, Generic, NFData, Rep

Show PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

typetype VerboseKey = String

#

typetype VerboseLevel = Int

#

typetype Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)

#

Nothing is used if no verbosity options have been given, thus making it possible to handle the default case relatively quickly. Note that Nothing corresponds to a trie with verbosity level 1 for the empty path.

datadata WarningMode

#

A WarningMode has two components: a set of warnings to be displayed and a flag stating whether warnings should be turned into fatal errors.

Constructors

WarningMode
- _warningSet :: Set WarningName
- _warn2Error :: Bool

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq WarningModeDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Show WarningModeDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Generic WarningModeDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
NFData WarningModeDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
EmbPrj WarningModeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings

datadata UnicodeOrAscii

#

We want to know whether we are allowed to insert unicode characters or not.

Constructors

UnicodeOk
true: Unicode characters are allowed.
AsciiOnly
'false: Stick to ASCII.

Instances10Bounded, Enum, Eq, Show, Generic, NFData, …

Bounded UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
Enum UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
Eq UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
Show UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
Generic UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
NFData UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
Boolean UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
IsBool UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph
EmbPrj UnicodeOrAsciiDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Glyph

datadata ArgDescr a

#

Describes whether an option takes an argument or not, and if so how the argument is injected into a value of type a.

Constructors

NoArg a
no argument expected
ReqArg (String -> a) String
option requires argument
OptArg (Maybe String -> a) String
optional argument

Instances1Functor

Functor ArgDescrDefined in Agda-2.8.0.2 · Agda.Utils.GetOpt

datadata OptDescr a

#

Each OptDescr describes a single option.

The arguments to Option are:

list of short option characters
list of long option strings (without "--")
argument descriptor
explanation of option for user

Constructors

Option [Char] [String] (ArgDescr a) String
description of a single options:

Instances1Functor

Functor OptDescrDefined in Agda-2.8.0.2 · Agda.Utils.GetOpt

classclass (Functor m, Applicative m, Monad m) => HasOptions (m :: Type -> Type) where

#

Methods

pragmaOptions :: m PragmaOptions
Returns the pragma options which are currently in effect.
commandLineOptions :: m CommandLineOptions
Returns the command line options which are currently in effect.

Instances19HasOptions, …

HasOptions ReplMDefined in Agda-2.8.0.2 · Agda.Interaction.CommandLine
HasOptions IMDefined in Agda-2.8.0.2 · Agda.Interaction.Monad
HasOptions TerMDefined in Agda-2.8.0.2 · Agda.Termination.Monad
HasOptions ForcedVariableCollection'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Forcing
HasOptions ReduceMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasOptions NLMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatch
HasOptions m => HasOptions (AbsToConT m)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
HasOptions m => HasOptions (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
HasOptions m => HasOptions (BlockT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasOptions m => HasOptions (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Names
HasOptions m => HasOptions (ListT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
HasOptions m => HasOptions (ChangeT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
HasOptions m => HasOptions (MaybeT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
MonadIO m => HasOptions (TCMT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
HasOptions m => HasOptions (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
HasOptions m => HasOptions (IdentityT m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
HasOptions m => HasOptions (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
HasOptions m => HasOptions (StateT s m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions
(HasOptions m, Monoid w) => HasOptions (WriterT w m)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.HasOptions

datadata CommandLineOptions

#

Constructors

Options
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
  The list should not contain duplicates.
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
  Use this (if Just) instead of ~/.agda/libraries.
- optDefaultLibs :: Bool
  Use ~/.agda/defaults.
- optUseLibs :: Bool
  look for .agda-lib files.
- optTraceImports :: Integer
  Configure notifications about imported modules.
- optTrustedExecutables :: Map ExeName FilePath
  Map names of trusted executables to absolute paths.
- optPrintAgdaDataDir :: Bool
- optPrintAgdaAppDir :: Bool
- optPrintVersion :: Maybe PrintAgdaVersion
- optPrintHelp :: Maybe Help
- optBuildLibrary :: Bool
  --build-library: Build all modules in the current library.
- optSetup :: Bool
  Force Agda to self-setup at startup.
- optEmacsMode :: Set EmacsModeCommand
  Emacs mode administration (formerly done by the agda-mode executable). Accepted subcommands: locate, setup, compile. Can be given several times, subcommands are accumulated in the set.
- optInteractive :: Bool
  Agda REPL (-I).
- optGHCiInteraction :: Bool
  --interaction mode.
- optJSONInteraction :: Bool
  --interaction-json mode.
- optExitOnError :: !Bool
  Exit if an interactive command fails.
- optCompileDir :: Maybe FilePath
  In the absence of a path the project root is used.
- optGenerateVimFile :: Bool
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool
  Should the top-level module only be scope-checked, and not type-checked?
- optTransliterate :: Bool
  Should code points that are not supported by the locale be transliterated?
- optDiagnosticsColour :: DiagnosticsColours
  Configure colour output.

Instances8Show, Generic, NFData, LensPragmaOptions, LensIncludePaths, LensPersistentVerbosity, …

Show CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensPragmaOptions CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensIncludePaths CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensPersistentVerbosity CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensSafeMode CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "Options" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "optProgramName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "optInputFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))) :*: ((S1 ('MetaSel ('Just "optAbsoluteIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath]) :*: S1 ('MetaSel ('Just "optLibraries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName])) :*: (S1 ('MetaSel ('Just "optOverrideLibrariesFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optDefaultLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optUseLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optTraceImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Just "optTrustedExecutables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ExeName FilePath)))) :*: ((S1 ('MetaSel ('Just "optPrintAgdaDataDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPrintAgdaAppDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optPrintVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe PrintAgdaVersion)) :*: S1 ('MetaSel ('Just "optPrintHelp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Help)))))) :*: (((S1 ('MetaSel ('Just "optBuildLibrary") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optSetup") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optEmacsMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set EmacsModeCommand)))) :*: ((S1 ('MetaSel ('Just "optInteractive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optGHCiInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optJSONInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optExitOnError") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)))) :*: (((S1 ('MetaSel ('Just "optCompileDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: S1 ('MetaSel ('Just "optGenerateVimFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optIgnoreInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optIgnoreAllInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optPragmaOptions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PragmaOptions) :*: S1 ('MetaSel ('Just "optOnlyScopeChecking") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optTransliterate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDiagnosticsColour") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DiagnosticsColours)))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata ConfluenceCheck

#

LocalConfluenceCheck GlobalConfluenceCheck

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
EmbPrj ConfluenceCheckDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata DiagnosticsColours

#

AlwaysColour NeverColour AutoColour

Instances4Show, Generic, NFData, Rep

Show DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData DiagnosticsColoursDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata EmacsModeCommand

#

If several --emacs-mode commands are given, they are executed in the order as given in this datatype.

Constructors

EmacsModeCompile
Compile the .el files to .elc.
EmacsModeSetup
Add the initialization lines to .emacs.
EmacsModeLocate
Print the installation location of agda2.el.

Instances6Eq, Ord, Show, Generic, NFData, Rep

Eq EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Ord EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData EmacsModeCommandDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata InfectiveCoinfective

#

Infective or coinfective?

Infective Coinfective

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
EmbPrj InfectiveCoinfectiveDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

classclass LensPragmaOptions a where

#

Methods

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

Instances3LensPragmaOptions

LensPragmaOptions CommandLineOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensPragmaOptions PreScopeStateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensPragmaOptions TCStateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base

datadata PragmaOptions

#

Options which can be set in a pragma.

Constructors

PragmaOptions
- _optShowImplicit :: WithDefault 'False
- _optShowGeneralized :: WithDefault 'True
  Show generalized parameters in Pi types
- _optShowIrrelevant :: WithDefault 'False
- _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
- _optVerbose :: !Verbosity
- _optProfiling :: ProfileOptions
- _optProp :: WithDefault 'False
- _optLevelUniverse :: WithDefault 'False
- _optTwoLevel :: WithDefault 'False
- _optAllowUnsolved :: WithDefault 'False
- _optAllowIncompleteMatch :: WithDefault 'False
- _optPositivityCheck :: WithDefault 'True
- _optTerminationCheck :: WithDefault 'True
- _optTerminationDepth :: CutOff
  Cut off structural order comparison at some depth in termination checker?
- _optUniverseCheck :: WithDefault 'True
- _optOmegaInOmega :: WithDefault 'False
- _optCumulativity :: WithDefault 'False
- _optSizedTypes :: WithDefault 'False
- _optGuardedness :: WithDefault 'False
- _optInjectiveTypeConstructors :: WithDefault 'False
- _optUniversePolymorphism :: WithDefault 'True
- _optIrrelevantProjections :: WithDefault 'False
- _optExperimentalIrrelevance :: WithDefault 'False
  irrelevant levels, irrelevant data matching
- _optWithoutK :: WithDefault 'False
- _optCubicalCompatible :: WithDefault 'False
- _optCopatterns :: WithDefault 'True
  Allow definitions by copattern matching?
- _optPatternMatching :: WithDefault 'True
  Is pattern matching allowed in the current file?
- _optExactSplit :: WithDefault 'False
- _optHiddenArgumentPuns :: WithDefault 'False
  Should patterns of the form {x} or ⦃ x ⦄ be interpreted as puns?
- _optEta :: WithDefault 'True
- _optForcing :: WithDefault 'True
  Perform the forcing analysis on data constructors?
- _optProjectionLike :: WithDefault 'True
  Perform the projection-likeness analysis on functions?
- _optErasure :: WithDefault 'False
- _optErasedMatches :: WithDefault 'True
  Allow matching in erased positions for single-constructor, non-indexed data/record types. (This kind of matching is always allowed for record types with η-equality.)
- _optEraseRecordParameters :: WithDefault 'False
  Mark parameters of record modules as erased?
- _optRewriting :: WithDefault 'False
  Can rewrite rules be added and used?
- _optCubical :: Maybe Cubical
- _optGuarded :: WithDefault 'False
- _optFirstOrder :: WithDefault 'False
  Should we speculatively unify function applications as if they were injective? Implies optRequireUniqueMetaSolutions.
- _optRequireUniqueMetaSolutions :: WithDefault 'True
  Forbid non-unique meta solutions allowed. For instance from INJECTIVE_FOR_INFERENCE pragmas.
- _optPostfixProjections :: WithDefault 'True
  Should system generated projections ProjSystem be printed postfix (True) or prefix (False).
- _optKeepPatternVariables :: WithDefault 'True
  Should case splitting replace variables with dot patterns (False) or keep them as variables (True).
- _optInferAbsurdClauses :: WithDefault 'True
  Should case splitting and coverage checking try to discharge absurd clauses? Default: True, but False might make coverage checking considerably faster in some cases.
- _optInstanceSearchDepth :: Int
- _optBacktrackingInstances :: WithDefault 'False
- _optQualifiedInstances :: WithDefault 'True
  Should instance search consider instances with qualified names?
- _optInversionMaxDepth :: Int
- _optSafe :: WithDefault 'False
- _optDoubleCheck :: WithDefault 'False
- _optSyntacticEquality :: !Maybe Int
  Should the conversion checker use the syntactic equality shortcut? Nothing means that it should. Just n, for a non-negative number n, means that syntactic equality checking gets n units of fuel. If the fuel becomes zero, then syntactic equality checking is turned off. The fuel counter is decreased in the failure continuation of checkSyntacticEquality.
- _optWarningMode :: WarningMode
- _optCompileMain :: WithDefault 'True
  Treat the module given at the command line or via interaction as main module in compilation?
- _optCaching :: WithDefault 'True
- _optCountClusters :: WithDefault 'False
  Count extended grapheme clusters rather than code points when generating LaTeX.
- _optAutoInline :: WithDefault 'False
  Automatic compile-time inlining for simple definitions (unless marked NOINLINE).
- _optPrintPatternSynonyms :: WithDefault 'True
- _optFastReduce :: WithDefault 'True
  Use the Agda abstract machine (fastReduce)?
- _optCallByName :: WithDefault 'False
  Use call-by-name instead of call-by-need.
- _optConfluenceCheck :: Maybe ConfluenceCheck
  Check confluence of rewrite rules?
- _optCohesion :: WithDefault 'False
  Are the cohesion modalities available?
- _optFlatSplit :: WithDefault 'False
  Can we split on a (@flat x : A) argument?
- _optPolarity :: WithDefault 'False
  Can we use modal polarities (++, +, etc.)?
- _optImportSorts :: WithDefault 'True
  Should every top-level module start with an implicit statement open import Agda.Primitive using (Set; Prop)?
- _optLoadPrimitives :: WithDefault 'True
  Should we load the primitive modules at all? This is a stronger form of optImportSorts.
- _optAllowExec :: WithDefault 'False
  Allow running external executables from meta programs.
- _optSaveMetas :: WithDefault 'False
  Save meta-variables to interface files.
- _optShowIdentitySubstitutions :: WithDefault 'False
  Show identity substitutions when pretty-printing terms (i.e. always show all arguments of a metavariable).
- _optKeepCoveringClauses :: WithDefault 'False
  Do not discard clauses constructed by the coverage checker (needed for some external backends).
- _optLargeIndices :: WithDefault 'False
  Allow large indices, and large forced arguments in constructors.
- _optForcedArgumentRecursion :: WithDefault 'True
  Allow recursion on forced constructor arguments.
- _optExperimentalLazyInstances :: WithDefault 'False
  Defer instance search based on discrimination tree results

Instances9Eq, Show, Generic, NFData, LensPersistentVerbosity, LensSafeMode, …

Eq PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Show PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
LensPersistentVerbosity PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensSafeMode PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
LensVerbosity PragmaOptionsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Lenses
EmbPrj PragmaOptionsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "PragmaOptions" 'PrefixI 'True) ((((((S1 ('MetaSel ('Just "_optShowImplicit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optShowGeneralized") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optShowIrrelevant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optUseUnicode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault' UnicodeOrAscii 'True)))) :*: ((S1 ('MetaSel ('Just "_optVerbose") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Verbosity) :*: S1 ('MetaSel ('Just "_optProfiling") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProfileOptions)) :*: (S1 ('MetaSel ('Just "_optProp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optLevelUniverse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :*: (((S1 ('MetaSel ('Just "_optTwoLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optAllowUnsolved") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optAllowIncompleteMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optTerminationDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CutOff)) :*: (S1 ('MetaSel ('Just "_optUniverseCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: (S1 ('MetaSel ('Just "_optOmegaInOmega") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCumulativity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))))) :*: ((((S1 ('MetaSel ('Just "_optSizedTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optGuardedness") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optInjectiveTypeConstructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optUniversePolymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optIrrelevantProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optExperimentalIrrelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optWithoutK") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optCubicalCompatible") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCopatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))))) :*: (((S1 ('MetaSel ('Just "_optPatternMatching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optExactSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optHiddenArgumentPuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optEta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optForcing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optProjectionLike") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optErasure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optErasedMatches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optEraseRecordParameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))))))) :*: (((((S1 ('MetaSel ('Just "_optRewriting") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optCubical") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Cubical))) :*: (S1 ('MetaSel ('Just "_optGuarded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optFirstOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optRequireUniqueMetaSolutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optPostfixProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optKeepPatternVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: (S1 ('MetaSel ('Just "_optInferAbsurdClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optInstanceSearchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :*: (((S1 ('MetaSel ('Just "_optBacktrackingInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optQualifiedInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optInversionMaxDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "_optSafe") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optDoubleCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optSyntacticEquality") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Int))) :*: (S1 ('MetaSel ('Just "_optWarningMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningMode) :*: (S1 ('MetaSel ('Just "_optCompileMain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optCaching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))))))) :*: ((((S1 ('MetaSel ('Just "_optCountClusters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optAutoInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optPrintPatternSynonyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optFastReduce") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :*: ((S1 ('MetaSel ('Just "_optCallByName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optConfluenceCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ConfluenceCheck))) :*: (S1 ('MetaSel ('Just "_optCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optFlatSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optPolarity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))))) :*: (((S1 ('MetaSel ('Just "_optImportSorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optLoadPrimitives") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :*: (S1 ('MetaSel ('Just "_optAllowExec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optSaveMetas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "_optShowIdentitySubstitutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optKeepCoveringClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "_optLargeIndices") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: (S1 ('MetaSel ('Just "_optForcedArgumentRecursion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :*: S1 ('MetaSel ('Just "_optExperimentalLazyInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

datadata PrintAgdaVersion

#

Options --version and --numeric-version (last wins).

Constructors

PrintAgdaVersion
Print Agda version information.
PrintAgdaNumericVersion
Print Agda version number.

Instances4Show, Generic, NFData, Rep

Show PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
Generic PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
NFData PrintAgdaVersionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Types
type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Types

typetype VerboseKey = String

#

typetype VerboseKeyItem = String1

#

typetype VerboseLevel = Int

#

typetype Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)

#

Nothing is used if no verbosity options have been given, thus making it possible to handle the default case relatively quickly. Note that Nothing corresponds to a trie with verbosity level 1 for the empty path.