Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Options

Synopsis

- data CommandLineOptions = Options {
  - optProgramName :: String
  - optInputFile :: Maybe FilePath
  - optIncludePaths :: [FilePath]
  - optAbsoluteIncludePaths :: [AbsolutePath]
  - optLibraries :: [LibName]
  - optOverrideLibrariesFile :: Maybe FilePath
  - optDefaultLibs :: Bool
  - optUseLibs :: Bool
  - optTraceImports :: Integer
  - optTrustedExecutables :: Map ExeName FilePath
  - optPrintAgdaDataDir :: Bool
  - optPrintAgdaAppDir :: Bool
  - optPrintVersion :: Maybe PrintAgdaVersion
  - optPrintHelp :: Maybe Help
  - optBuildLibrary :: Bool
  - optSetup :: Bool
  - optEmacsMode :: Set EmacsModeCommand
  - optInteractive :: Bool
  - optGHCiInteraction :: Bool
  - optJSONInteraction :: Bool
  - optExitOnError :: !Bool
  - optCompileDir :: Maybe FilePath
  - optGenerateVimFile :: Bool
  - optIgnoreInterfaces :: Bool
  - optIgnoreAllInterfaces :: Bool
  - optPragmaOptions :: PragmaOptions
  - optOnlyScopeChecking :: Bool
  - optTransliterate :: Bool
  - optDiagnosticsColour :: DiagnosticsColours
  }
- defaultOptions :: CommandLineOptions
- data ArgDescr a
  - = NoArg a
  - | ReqArg (String -> a) String
  - | OptArg (Maybe String -> a) String
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- type Flag opts = opts -> OptM opts
- optCountClusters :: PragmaOptions -> Bool
- data WarningMode = WarningMode {
  - _warningSet :: Set WarningName
  - _warn2Error :: Bool
  }
- parseVerboseKey :: VerboseKey -> [VerboseKeyItem]
- data UnicodeOrAscii
  - = UnicodeOk
  - | AsciiOnly
- optPolarity :: PragmaOptions -> Bool
- optUseUnicode :: PragmaOptions -> UnicodeOrAscii
- defaultCutOff :: CutOff
- optTerminationDepth :: PragmaOptions -> CutOff
- optRewriting :: PragmaOptions -> Bool
- optQualifiedInstances :: PragmaOptions -> Bool
- lensOptExperimentalLazyInstances :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- optFirstOrder :: PragmaOptions -> Bool
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
- data ConfluenceCheck
  - = LocalConfluenceCheck
  - | GlobalConfluenceCheck
- optInjectiveTypeConstructors :: PragmaOptions -> Bool
- optCumulativity :: PragmaOptions -> Bool
- optAllowExec :: PragmaOptions -> Bool
- data PragmaOptions = PragmaOptions {
  - _optShowImplicit :: WithDefault 'False
  - _optShowGeneralized :: WithDefault 'True
  - _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
  - _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
  - _optWithoutK :: WithDefault 'False
  - _optCubicalCompatible :: WithDefault 'False
  - _optCopatterns :: WithDefault 'True
  - _optPatternMatching :: WithDefault 'True
  - _optExactSplit :: WithDefault 'False
  - _optHiddenArgumentPuns :: WithDefault 'False
  - _optEta :: WithDefault 'True
  - _optForcing :: WithDefault 'True
  - _optProjectionLike :: WithDefault 'True
  - _optErasure :: WithDefault 'False
  - _optErasedMatches :: WithDefault 'True
  - _optEraseRecordParameters :: WithDefault 'False
  - _optRewriting :: WithDefault 'False
  - _optCubical :: Maybe Cubical
  - _optGuarded :: WithDefault 'False
  - _optFirstOrder :: WithDefault 'False
  - _optRequireUniqueMetaSolutions :: WithDefault 'True
  - _optPostfixProjections :: WithDefault 'True
  - _optKeepPatternVariables :: WithDefault 'True
  - _optInferAbsurdClauses :: WithDefault 'True
  - _optInstanceSearchDepth :: Int
  - _optBacktrackingInstances :: WithDefault 'False
  - _optQualifiedInstances :: WithDefault 'True
  - _optInversionMaxDepth :: Int
  - _optSafe :: WithDefault 'False
  - _optDoubleCheck :: WithDefault 'False
  - _optSyntacticEquality :: !(Maybe Int)
  - _optWarningMode :: WarningMode
  - _optCompileMain :: WithDefault 'True
  - _optCaching :: WithDefault 'True
  - _optCountClusters :: WithDefault 'False
  - _optAutoInline :: WithDefault 'False
  - _optPrintPatternSynonyms :: WithDefault 'True
  - _optFastReduce :: WithDefault 'True
  - _optCallByName :: WithDefault 'False
  - _optConfluenceCheck :: Maybe ConfluenceCheck
  - _optCohesion :: WithDefault 'False
  - _optFlatSplit :: WithDefault 'False
  - _optPolarity :: WithDefault 'False
  - _optImportSorts :: WithDefault 'True
  - _optLoadPrimitives :: WithDefault 'True
  - _optAllowExec :: WithDefault 'False
  - _optSaveMetas :: WithDefault 'False
  - _optShowIdentitySubstitutions :: WithDefault 'False
  - _optKeepCoveringClauses :: WithDefault 'False
  - _optLargeIndices :: WithDefault 'False
  - _optForcedArgumentRecursion :: WithDefault 'True
  - _optExperimentalLazyInstances :: WithDefault 'False
  }
- type OptionError = String
- data OptionWarning
  - = OptionRenamed {
    - oldOptionName :: String
    - newOptionName :: String
    }
  - | WarningProblem WarningModeError
- optionWarningName :: OptionWarning -> WarningName
- data OptM a
- runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)
- data DiagnosticsColours
  - = AlwaysColour
  - | NeverColour
  - | AutoColour
- data EmacsModeCommand
  - = EmacsModeCompile
  - | EmacsModeSetup
  - | EmacsModeLocate
- data PrintAgdaVersion
  - = PrintAgdaVersion
  - | PrintAgdaNumericVersion
- checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions
- parsePragmaOptions :: OptionsPragma -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- stripRTS :: [String] -> [String]
- defaultInteractionOptions :: PragmaOptions
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: PragmaOptions -> [String]
- recheckBecausePragmaOptionsChanged :: PragmaOptions -> PragmaOptions -> Bool
- data InfectiveCoinfective
  - = Infective
  - | Coinfective
- data InfectiveCoinfectiveOption = ICOption {
  - icOptionActive :: PragmaOptions -> Bool
  - icOptionDescription :: String
  - icOptionKind :: InfectiveCoinfective
  - icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
  - icOptionWarning :: TopLevelModuleName -> Doc
  }
- infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption]
- data ImpliedPragmaOption where
  - ImpliesPragmaOption :: forall (a :: Bool) (b :: Bool). String -> Bool -> (PragmaOptions -> WithDefault a) -> String -> Bool -> (PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
- impliedPragmaOptions :: [ImpliedPragmaOption]
- safeFlag :: Flag PragmaOptions
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> String -> Help -> String
- inputFlag :: FilePath -> Flag CommandLineOptions
- standardOptions :: [OptDescr (Flag CommandLineOptions)]
- deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
- getOptSimple :: [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
- lensOptShowImplicit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptShowIrrelevant :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptUseUnicode :: Functor f => (WithDefault' UnicodeOrAscii 'True -> f (WithDefault' UnicodeOrAscii 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptVerbose :: Functor f => (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions
- lensOptProfiling :: Functor f => (ProfileOptions -> f ProfileOptions) -> PragmaOptions -> f PragmaOptions
- lensOptProp :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptLevelUniverse :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptTwoLevel :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptAllowUnsolved :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptAllowIncompleteMatch :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptPositivityCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptTerminationCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptTerminationDepth :: Functor f => (CutOff -> f CutOff) -> PragmaOptions -> f PragmaOptions
- lensOptUniverseCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptNoUniverseCheck :: Functor f => (WithDefault' Bool 'True -> f (WithDefault' Bool 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptOmegaInOmega :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptCumulativity :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptSizedTypes :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptGuardedness :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptInjectiveTypeConstructors :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptUniversePolymorphism :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptIrrelevantProjections :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptExperimentalIrrelevance :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptWithoutK :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptCubicalCompatible :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptCopatterns :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptPatternMatching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptExactSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptHiddenArgumentPuns :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptEta :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptForcing :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptProjectionLike :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptErasure :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptErasedMatches :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptEraseRecordParameters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptRewriting :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptCubical :: Functor f => (Maybe Cubical -> f (Maybe Cubical)) -> PragmaOptions -> f PragmaOptions
- lensOptGuarded :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptFirstOrder :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptRequireUniqueMetaSolutions :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptPostfixProjections :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptKeepPatternVariables :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptInferAbsurdClauses :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptInstanceSearchDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions
- lensOptBacktrackingInstances :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptQualifiedInstances :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptInversionMaxDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions
- lensOptSafe :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptDoubleCheck :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptSyntacticEquality :: Functor f => (Maybe Int -> f (Maybe Int)) -> PragmaOptions -> f PragmaOptions
- lensOptWarningMode :: Functor f => (WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions
- lensOptCompileMain :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptCaching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptCountClusters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptAutoInline :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptPrintPatternSynonyms :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptFastReduce :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptCallByName :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptConfluenceCheck :: Functor f => (Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)) -> PragmaOptions -> f PragmaOptions
- lensOptCohesion :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptFlatSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptPolarity :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptImportSorts :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptLoadPrimitives :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions
- lensOptAllowExec :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptSaveMetas :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptShowIdentitySubstitutions :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- lensOptKeepCoveringClauses :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
- optShowImplicit :: PragmaOptions -> Bool
- optShowGeneralized :: PragmaOptions -> Bool
- optShowIrrelevant :: PragmaOptions -> Bool
- optProp :: PragmaOptions -> Bool
- optLevelUniverse :: PragmaOptions -> Bool
- optTwoLevel :: PragmaOptions -> Bool
- optAllowUnsolved :: PragmaOptions -> Bool
- optAllowIncompleteMatch :: PragmaOptions -> Bool
- optPositivityCheck :: PragmaOptions -> Bool
- optTerminationCheck :: PragmaOptions -> Bool
- optUniverseCheck :: PragmaOptions -> Bool
- optOmegaInOmega :: PragmaOptions -> Bool
- optSizedTypes :: PragmaOptions -> Bool
- optGuardedness :: PragmaOptions -> Bool
- optUniversePolymorphism :: PragmaOptions -> Bool
- optIrrelevantProjections :: PragmaOptions -> Bool
- optExperimentalIrrelevance :: PragmaOptions -> Bool
- optWithoutK :: PragmaOptions -> Bool
- optCubicalCompatible :: PragmaOptions -> Bool
- optCopatterns :: PragmaOptions -> Bool
- optPatternMatching :: PragmaOptions -> Bool
- optHiddenArgumentPuns :: PragmaOptions -> Bool
- optEta :: PragmaOptions -> Bool
- optForcing :: PragmaOptions -> Bool
- optProjectionLike :: PragmaOptions -> Bool
- optErasure :: PragmaOptions -> Bool
- optErasedMatches :: PragmaOptions -> Bool
- optEraseRecordParameters :: PragmaOptions -> Bool
- optGuarded :: PragmaOptions -> Bool
- optRequireUniqueMetaSolutions :: PragmaOptions -> Bool
- optPostfixProjections :: PragmaOptions -> Bool
- optKeepPatternVariables :: PragmaOptions -> Bool
- optInferAbsurdClauses :: PragmaOptions -> Bool
- optBacktrackingInstances :: PragmaOptions -> Bool
- optSafe :: PragmaOptions -> Bool
- optDoubleCheck :: PragmaOptions -> Bool
- optCompileNoMain :: PragmaOptions -> Bool
- optCaching :: PragmaOptions -> Bool
- optAutoInline :: PragmaOptions -> Bool
- optPrintPatternSynonyms :: PragmaOptions -> Bool
- optFastReduce :: PragmaOptions -> Bool
- optCallByName :: PragmaOptions -> Bool
- optCohesion :: PragmaOptions -> Bool
- optFlatSplit :: PragmaOptions -> Bool
- optImportSorts :: PragmaOptions -> Bool
- optLoadPrimitives :: PragmaOptions -> Bool
- optSaveMetas :: PragmaOptions -> Bool
- optShowIdentitySubstitutions :: PragmaOptions -> Bool
- optKeepCoveringClauses :: PragmaOptions -> Bool
- optLargeIndices :: PragmaOptions -> Bool
- optForcedArgumentRecursion :: PragmaOptions -> Bool
- optConfluenceCheck :: PragmaOptions -> Maybe ConfluenceCheck
- optCubical :: PragmaOptions -> Maybe Cubical
- optInstanceSearchDepth :: PragmaOptions -> Int
- optInversionMaxDepth :: PragmaOptions -> Int
- optProfiling :: PragmaOptions -> ProfileOptions
- optSyntacticEquality :: PragmaOptions -> Maybe Int
- optVerbose :: PragmaOptions -> Verbosity
- optWarningMode :: PragmaOptions -> WarningMode
- class (Functor m, Applicative m, Monad m) => HasOptions (m :: Type -> Type) where
  - pragmaOptions :: m PragmaOptions
  - commandLineOptions :: m CommandLineOptions
- data CommandLineOptions = Options {
  - optProgramName :: String
  - optInputFile :: Maybe FilePath
  - optIncludePaths :: [FilePath]
  - optAbsoluteIncludePaths :: [AbsolutePath]
  - optLibraries :: [LibName]
  - optOverrideLibrariesFile :: Maybe FilePath
  - optDefaultLibs :: Bool
  - optUseLibs :: Bool
  - optTraceImports :: Integer
  - optTrustedExecutables :: Map ExeName FilePath
  - optPrintAgdaDataDir :: Bool
  - optPrintAgdaAppDir :: Bool
  - optPrintVersion :: Maybe PrintAgdaVersion
  - optPrintHelp :: Maybe Help
  - optBuildLibrary :: Bool
  - optSetup :: Bool
  - optEmacsMode :: Set EmacsModeCommand
  - optInteractive :: Bool
  - optGHCiInteraction :: Bool
  - optJSONInteraction :: Bool
  - optExitOnError :: !Bool
  - optCompileDir :: Maybe FilePath
  - optGenerateVimFile :: Bool
  - optIgnoreInterfaces :: Bool
  - optIgnoreAllInterfaces :: Bool
  - optPragmaOptions :: PragmaOptions
  - optOnlyScopeChecking :: Bool
  - optTransliterate :: Bool
  - optDiagnosticsColour :: DiagnosticsColours
  }
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
- class LensPragmaOptions a where
  - getPragmaOptions :: a -> PragmaOptions
  - setPragmaOptions :: PragmaOptions -> a -> a
  - mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> a -> a
  - lensPragmaOptions :: Lens' a PragmaOptions
- data ConfluenceCheck
  - = LocalConfluenceCheck
  - | GlobalConfluenceCheck
- data PragmaOptions = PragmaOptions {
  - _optShowImplicit :: WithDefault 'False
  - _optShowGeneralized :: WithDefault 'True
  - _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
  - _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
  - _optWithoutK :: WithDefault 'False
  - _optCubicalCompatible :: WithDefault 'False
  - _optCopatterns :: WithDefault 'True
  - _optPatternMatching :: WithDefault 'True
  - _optExactSplit :: WithDefault 'False
  - _optHiddenArgumentPuns :: WithDefault 'False
  - _optEta :: WithDefault 'True
  - _optForcing :: WithDefault 'True
  - _optProjectionLike :: WithDefault 'True
  - _optErasure :: WithDefault 'False
  - _optErasedMatches :: WithDefault 'True
  - _optEraseRecordParameters :: WithDefault 'False
  - _optRewriting :: WithDefault 'False
  - _optCubical :: Maybe Cubical
  - _optGuarded :: WithDefault 'False
  - _optFirstOrder :: WithDefault 'False
  - _optRequireUniqueMetaSolutions :: WithDefault 'True
  - _optPostfixProjections :: WithDefault 'True
  - _optKeepPatternVariables :: WithDefault 'True
  - _optInferAbsurdClauses :: WithDefault 'True
  - _optInstanceSearchDepth :: Int
  - _optBacktrackingInstances :: WithDefault 'False
  - _optQualifiedInstances :: WithDefault 'True
  - _optInversionMaxDepth :: Int
  - _optSafe :: WithDefault 'False
  - _optDoubleCheck :: WithDefault 'False
  - _optSyntacticEquality :: !(Maybe Int)
  - _optWarningMode :: WarningMode
  - _optCompileMain :: WithDefault 'True
  - _optCaching :: WithDefault 'True
  - _optCountClusters :: WithDefault 'False
  - _optAutoInline :: WithDefault 'False
  - _optPrintPatternSynonyms :: WithDefault 'True
  - _optFastReduce :: WithDefault 'True
  - _optCallByName :: WithDefault 'False
  - _optConfluenceCheck :: Maybe ConfluenceCheck
  - _optCohesion :: WithDefault 'False
  - _optFlatSplit :: WithDefault 'False
  - _optPolarity :: WithDefault 'False
  - _optImportSorts :: WithDefault 'True
  - _optLoadPrimitives :: WithDefault 'True
  - _optAllowExec :: WithDefault 'False
  - _optSaveMetas :: WithDefault 'False
  - _optShowIdentitySubstitutions :: WithDefault 'False
  - _optKeepCoveringClauses :: WithDefault 'False
  - _optLargeIndices :: WithDefault 'False
  - _optForcedArgumentRecursion :: WithDefault 'True
  - _optExperimentalLazyInstances :: WithDefault 'False
  }
- data DiagnosticsColours
  - = AlwaysColour
  - | NeverColour
  - | AutoColour
- data EmacsModeCommand
  - = EmacsModeCompile
  - | EmacsModeSetup
  - | EmacsModeLocate
- data PrintAgdaVersion
  - = PrintAgdaVersion
  - | PrintAgdaNumericVersion
- data InfectiveCoinfective
  - = Infective
  - | Coinfective
- type VerboseKeyItem = String1

# Documentation

data CommandLineOptions Source #

Constructors

Options |

Fields

- 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.

#### Instances

Instances details

LensIncludePaths CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath] Source #

setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions Source #

mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions Source #

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source #

setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions Source #

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions Source #

LensPersistentVerbosity CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensSafeMode CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions Source #
NFData CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: CommandLineOptions -> () Source #
Generic CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep CommandLineOptions |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))))

Methods

from :: CommandLineOptions -> Rep CommandLineOptions x Source #

to :: Rep CommandLineOptions x -> CommandLineOptions Source #

Show CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> CommandLineOptions -> ShowS Source # show :: CommandLineOptions -> String Source # showList :: [CommandLineOptions] -> ShowS Source #
type Rep CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))))

defaultOptions :: CommandLineOptions Source #

data ArgDescr a Source #

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

#### Instances

Instances details

Functor ArgDescr Source # |
Instance details Defined in Agda.Utils.GetOpt Methods fmap :: (a -> b) -> ArgDescr a -> ArgDescr b Source # (<$) :: a -> ArgDescr b -> ArgDescr a Source #

data OptDescr a Source #

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 | description of a single options:

Fields

- [Char]

  list of short option characters

- [String]

  list of long option strings (without "--")

- (ArgDescr a)

  argument descriptor

- String

  explanation of option for user

#### Instances

Instances details

Functor OptDescr Source # |
Instance details Defined in Agda.Utils.GetOpt Methods fmap :: (a -> b) -> OptDescr a -> OptDescr b Source # (<$) :: a -> OptDescr b -> OptDescr a Source #

type Flag opts = opts -> OptM opts Source #

`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

optCountClusters :: PragmaOptions -> Bool Source #

data WarningMode Source #

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 |

Fields

- _warningSet :: Set WarningName
- _warn2Error :: Bool

#### Instances

Instances details

EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Word32 Source # icod_ :: WarningMode -> S Word32 Source # value :: Word32 -> R WarningMode Source #
NFData WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () Source #
Generic WarningMode Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningMode |

Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: WarningMode -> Rep WarningMode x Source #

to :: Rep WarningMode x -> WarningMode Source #

Show WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS Source # show :: WarningMode -> String Source # showList :: [WarningMode] -> ShowS Source #
Eq WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool Source # (/=) :: WarningMode -> WarningMode -> Bool Source #
type Rep WarningMode Source # |

Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

parseVerboseKey :: VerboseKey -> [VerboseKeyItem] Source #

data UnicodeOrAscii Source #

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.

#### Instances

Instances details

EmbPrj UnicodeOrAscii Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UnicodeOrAscii -> S Word32 Source # icod_ :: UnicodeOrAscii -> S Word32 Source # value :: Word32 -> R UnicodeOrAscii Source #
Boolean UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

fromBool :: Bool -> UnicodeOrAscii Source #

true :: UnicodeOrAscii Source #

false :: UnicodeOrAscii Source #

not :: UnicodeOrAscii -> UnicodeOrAscii Source #

(&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

(||) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

IsBool UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods toBool :: UnicodeOrAscii -> Bool Source # ifThenElse :: UnicodeOrAscii -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii Source # fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #
NFData UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods rnf :: UnicodeOrAscii -> () Source #
Bounded UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods minBound :: UnicodeOrAscii Source # maxBound :: UnicodeOrAscii Source #
Enum UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

succ :: UnicodeOrAscii -> UnicodeOrAscii Source #

pred :: UnicodeOrAscii -> UnicodeOrAscii Source #

toEnum :: Int -> UnicodeOrAscii Source #

fromEnum :: UnicodeOrAscii -> Int Source #

enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromThenTo :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

Generic UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Associated Types

type Rep UnicodeOrAscii |
Instance details Defined in Agda.Syntax.Concrete.Glyph type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: UnicodeOrAscii -> Rep UnicodeOrAscii x Source #

to :: Rep UnicodeOrAscii x -> UnicodeOrAscii Source #

Show UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods showsPrec :: Int -> UnicodeOrAscii -> ShowS Source # show :: UnicodeOrAscii -> String Source # showList :: [UnicodeOrAscii] -> ShowS Source #
Eq UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods (==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source # (/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source #
type Rep UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

optPolarity :: PragmaOptions -> Bool Source #

optUseUnicode :: PragmaOptions -> UnicodeOrAscii Source #

defaultCutOff :: CutOff Source #

The default termination depth.

optTerminationDepth :: PragmaOptions -> CutOff Source #

optRewriting :: PragmaOptions -> Bool Source #

optQualifiedInstances :: PragmaOptions -> Bool Source #

lensOptExperimentalLazyInstances :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

optFirstOrder :: PragmaOptions -> Bool Source #

type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel) Source #

`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.

type VerboseKey = String Source #

type VerboseLevel = Int Source #

data ConfluenceCheck Source #

Constructors

LocalConfluenceCheck |
GlobalConfluenceCheck |

#### Instances

Instances details

EmbPrj ConfluenceCheck Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Word32 Source # icod_ :: ConfluenceCheck -> S Word32 Source # value :: Word32 -> R ConfluenceCheck Source #
NFData ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: ConfluenceCheck -> () Source #
Generic ConfluenceCheck Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep ConfluenceCheck |
Instance details Defined in Agda.Interaction.Options.Types type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ConfluenceCheck -> Rep ConfluenceCheck x Source #

to :: Rep ConfluenceCheck x -> ConfluenceCheck Source #

Show ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> ConfluenceCheck -> ShowS Source # show :: ConfluenceCheck -> String Source # showList :: [ConfluenceCheck] -> ShowS Source #
Eq ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source # (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source #
type Rep ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

optInjectiveTypeConstructors :: PragmaOptions -> Bool Source #

optCumulativity :: PragmaOptions -> Bool Source #

optAllowExec :: PragmaOptions -> Bool Source #

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions |

Fields

- _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

#### Instances

Instances details

LensPersistentVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Word32 Source # icod_ :: PragmaOptions -> S Word32 Source # value :: Word32 -> R PragmaOptions Source #
NFData PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: PragmaOptions -> () Source #
Generic PragmaOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep PragmaOptions |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))))

Methods

from :: PragmaOptions -> Rep PragmaOptions x Source #

to :: Rep PragmaOptions x -> PragmaOptions Source #

Show PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> PragmaOptions -> ShowS Source # show :: PragmaOptions -> String Source # showList :: [PragmaOptions] -> ShowS Source #
Eq PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: PragmaOptions -> PragmaOptions -> Bool Source # (/=) :: PragmaOptions -> PragmaOptions -> Bool Source #
type Rep PragmaOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))))

type OptionError = String Source #

data OptionWarning Source #

Warnings when parsing options.

Constructors

OptionRenamed | Name of option changed in a newer version of Agda.

Fields

- oldOptionName :: String
- newOptionName :: String

WarningProblem WarningModeError | A problem with setting or unsetting a warning.

#### Instances

Instances details

Pretty OptionWarning Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods pretty :: OptionWarning -> Doc Source # prettyPrec :: Int -> OptionWarning -> Doc Source # prettyList :: [OptionWarning] -> Doc Source #
EmbPrj OptionWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OptionWarning -> S Word32 Source # icod_ :: OptionWarning -> S Word32 Source # value :: Word32 -> R OptionWarning Source #
NFData OptionWarning Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: OptionWarning -> () Source #
Generic OptionWarning Source # |

Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep OptionWarning |

Instance details

Defined in Agda.Interaction.Options.Base

type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningModeError)))

Methods

from :: OptionWarning -> Rep OptionWarning x Source #

to :: Rep OptionWarning x -> OptionWarning Source #

Show OptionWarning Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> OptionWarning -> ShowS Source # show :: OptionWarning -> String Source # showList :: [OptionWarning] -> ShowS Source #
type Rep OptionWarning Source # |

Instance details

Defined in Agda.Interaction.Options.Base

type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningModeError)))

optionWarningName :: OptionWarning -> WarningName Source #

data OptM a Source #

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

#### Instances

Instances details

Applicative OptM Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods pure :: a -> OptM a Source # (<*>) :: OptM (a -> b) -> OptM a -> OptM b Source # liftA2 :: (a -> b -> c) -> OptM a -> OptM b -> OptM c Source # (*>) :: OptM a -> OptM b -> OptM b Source # (<*) :: OptM a -> OptM b -> OptM a Source #
Functor OptM Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods fmap :: (a -> b) -> OptM a -> OptM b Source # (<$) :: a -> OptM b -> OptM a Source #
Monad OptM Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods (>>=) :: OptM a -> (a -> OptM b) -> OptM b Source # (>>) :: OptM a -> OptM b -> OptM b Source # return :: a -> OptM a Source #
MonadError OptionError OptM Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods throwError :: OptionError -> OptM a Source # catchError :: OptM a -> (OptionError -> OptM a) -> OptM a Source #

runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings) Source #

data DiagnosticsColours Source #

Constructors

AlwaysColour |
NeverColour |
AutoColour |

#### Instances

Instances details

NFData DiagnosticsColours Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: DiagnosticsColours -> () Source #
Generic DiagnosticsColours Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep DiagnosticsColours |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: DiagnosticsColours -> Rep DiagnosticsColours x Source #

to :: Rep DiagnosticsColours x -> DiagnosticsColours Source #

Show DiagnosticsColours Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> DiagnosticsColours -> ShowS Source # show :: DiagnosticsColours -> String Source # showList :: [DiagnosticsColours] -> ShowS Source #
type Rep DiagnosticsColours Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) (U1 :: Type -> Type)))

data EmacsModeCommand Source #

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`.

#### Instances

Instances details

NFData EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: EmacsModeCommand -> () Source #
Generic EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep EmacsModeCommand |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: EmacsModeCommand -> Rep EmacsModeCommand x Source #

to :: Rep EmacsModeCommand x -> EmacsModeCommand Source #

Show EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> EmacsModeCommand -> ShowS Source # show :: EmacsModeCommand -> String Source # showList :: [EmacsModeCommand] -> ShowS Source #
Eq EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source # (/=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #
Ord EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Methods

compare :: EmacsModeCommand -> EmacsModeCommand -> Ordering Source #

(<) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(<=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(>) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(>=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

max :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand Source #

min :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand Source #

type Rep EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) (U1 :: Type -> Type)))

data PrintAgdaVersion Source #

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

Constructors

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

#### Instances

Instances details

NFData PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: PrintAgdaVersion -> () Source #
Generic PrintAgdaVersion Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep PrintAgdaVersion |
Instance details Defined in Agda.Interaction.Options.Types type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: PrintAgdaVersion -> Rep PrintAgdaVersion x Source #

to :: Rep PrintAgdaVersion x -> PrintAgdaVersion Source #

Show PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> PrintAgdaVersion -> ShowS Source # show :: PrintAgdaVersion -> String Source # showList :: [PrintAgdaVersion] -> ShowS Source #
type Rep PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions Source #

Checks that the given options are consistent. Also makes adjustments (e.g. when one option implies another).

parsePragmaOptions Source #

Arguments

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

Parse options from an options pragma.

parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts Source #

Parse options for a plugin.

stripRTS :: [String] -> [String] Source #

Removes RTS options from a list of options.

defaultInteractionOptions :: PragmaOptions Source #

defaultPragmaOptions :: PragmaOptions Source #

standardOptions_ :: [OptDescr ()] Source #

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

unsafePragmaOptions :: PragmaOptions -> [String] Source #

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

recheckBecausePragmaOptionsChanged Source #

Arguments

:: 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.

data InfectiveCoinfective Source #

Infective or coinfective?

Constructors

Infective |
Coinfective |

#### Instances

Instances details

EmbPrj InfectiveCoinfective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Word32 Source # icod_ :: InfectiveCoinfective -> S Word32 Source # value :: Word32 -> R InfectiveCoinfective Source #
NFData InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: InfectiveCoinfective -> () Source #
Generic InfectiveCoinfective Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep InfectiveCoinfective |
Instance details Defined in Agda.Interaction.Options.Types type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: InfectiveCoinfective -> Rep InfectiveCoinfective x Source #

to :: Rep InfectiveCoinfective x -> InfectiveCoinfective Source #

Show InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> InfectiveCoinfective -> ShowS Source # show :: InfectiveCoinfective -> String Source # showList :: [InfectiveCoinfective] -> ShowS Source #
Eq InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool Source # (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool Source #
type Rep InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

data InfectiveCoinfectiveOption Source #

Descriptions of infective and coinfective options.

Constructors

ICOption |

Fields

- 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.

infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption] Source #

Infective and coinfective options.

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.

data ImpliedPragmaOption where Source #

Constructors

ImpliesPragmaOption |

Fields

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

  The first option having the given value implies the second option having its given value. For instance, `ImpliesPragmaOption "lossy-unification" True _optFirstOrder "require-unique-meta-solutions" False _optRequireUniqueMetaSolutions` encodes the fact that --lossy-unification implies --no-require-unique-meta-solutions.

impliedPragmaOptions :: [ImpliedPragmaOption] Source #

safeFlag :: Flag PragmaOptions Source #

mapFlag :: (String -> String) -> OptDescr a -> OptDescr a Source #

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

usage :: [OptDescr ()] -> String -> Help -> String Source #

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

inputFlag :: FilePath -> Flag CommandLineOptions Source #

standardOptions :: [OptDescr (Flag CommandLineOptions)] Source #

deadStandardOptions :: [OptDescr (Flag CommandLineOptions)] Source #

Command line options of previous versions of Agda. Should not be listed in the usage info, put parsed by GetOpt for good error messaging.

getOptSimple Source #

Arguments

:: [String] | command line argument words
-> [OptDescr (Flag opts)] | options handlers
-> (String -> Flag opts) | handler of non-options (only one is allowed)
-> Flag opts | combined opts data structure transformer

Simple interface for Agda.Utils.GetOpt Could be moved to Agda.Utils.Options (does not exist yet)

lensOptShowImplicit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptShowIrrelevant :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

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

lensOptVerbose :: Functor f => (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions Source #

lensOptProfiling :: Functor f => (ProfileOptions -> f ProfileOptions) -> PragmaOptions -> f PragmaOptions Source #

lensOptProp :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptLevelUniverse :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptTwoLevel :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptAllowUnsolved :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptAllowIncompleteMatch :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptPositivityCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptTerminationCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptTerminationDepth :: Functor f => (CutOff -> f CutOff) -> PragmaOptions -> f PragmaOptions Source #

lensOptUniverseCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

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

lensOptOmegaInOmega :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCumulativity :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptSizedTypes :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptGuardedness :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptInjectiveTypeConstructors :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptUniversePolymorphism :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptIrrelevantProjections :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptExperimentalIrrelevance :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptWithoutK :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCubicalCompatible :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCopatterns :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptPatternMatching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptExactSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptHiddenArgumentPuns :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptEta :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptForcing :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptProjectionLike :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptErasure :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptErasedMatches :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptEraseRecordParameters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptRewriting :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCubical :: Functor f => (Maybe Cubical -> f (Maybe Cubical)) -> PragmaOptions -> f PragmaOptions Source #

lensOptGuarded :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptFirstOrder :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptRequireUniqueMetaSolutions :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptPostfixProjections :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptKeepPatternVariables :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptInferAbsurdClauses :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptInstanceSearchDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions Source #

lensOptBacktrackingInstances :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptQualifiedInstances :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptInversionMaxDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions Source #

lensOptSafe :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptDoubleCheck :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptSyntacticEquality :: Functor f => (Maybe Int -> f (Maybe Int)) -> PragmaOptions -> f PragmaOptions Source #

lensOptWarningMode :: Functor f => (WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions Source #

lensOptCompileMain :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCaching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCountClusters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptAutoInline :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptPrintPatternSynonyms :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptFastReduce :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCallByName :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptConfluenceCheck :: Functor f => (Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)) -> PragmaOptions -> f PragmaOptions Source #

lensOptCohesion :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptFlatSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptPolarity :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptImportSorts :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptLoadPrimitives :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions Source #

lensOptAllowExec :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptSaveMetas :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptShowIdentitySubstitutions :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

lensOptKeepCoveringClauses :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions Source #

optShowImplicit :: PragmaOptions -> Bool Source #

optShowGeneralized :: PragmaOptions -> Bool Source #

optShowIrrelevant :: PragmaOptions -> Bool Source #

optProp :: PragmaOptions -> Bool Source #

optLevelUniverse :: PragmaOptions -> Bool Source #

optTwoLevel :: PragmaOptions -> Bool Source #

optAllowUnsolved :: PragmaOptions -> Bool Source #

optAllowIncompleteMatch :: PragmaOptions -> Bool Source #

optPositivityCheck :: PragmaOptions -> Bool Source #

optTerminationCheck :: PragmaOptions -> Bool Source #

optUniverseCheck :: PragmaOptions -> Bool Source #

optOmegaInOmega :: PragmaOptions -> Bool Source #

optSizedTypes :: PragmaOptions -> Bool Source #

optGuardedness :: PragmaOptions -> Bool Source #

optUniversePolymorphism :: PragmaOptions -> Bool Source #

optIrrelevantProjections :: PragmaOptions -> Bool Source #

optExperimentalIrrelevance :: PragmaOptions -> Bool Source #

optWithoutK :: PragmaOptions -> Bool Source #

optCubicalCompatible :: PragmaOptions -> Bool Source #

optCopatterns :: PragmaOptions -> Bool Source #

optPatternMatching :: PragmaOptions -> Bool Source #

optHiddenArgumentPuns :: PragmaOptions -> Bool Source #

optEta :: PragmaOptions -> Bool Source #

optForcing :: PragmaOptions -> Bool Source #

optProjectionLike :: PragmaOptions -> Bool Source #

optErasure :: PragmaOptions -> Bool Source #

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

optErasedMatches :: PragmaOptions -> Bool Source #

optEraseRecordParameters :: PragmaOptions -> Bool Source #

optGuarded :: PragmaOptions -> Bool Source #

optRequireUniqueMetaSolutions :: PragmaOptions -> Bool Source #

optPostfixProjections :: PragmaOptions -> Bool Source #

optKeepPatternVariables :: PragmaOptions -> Bool Source #

optInferAbsurdClauses :: PragmaOptions -> Bool Source #

optBacktrackingInstances :: PragmaOptions -> Bool Source #

optSafe :: PragmaOptions -> Bool Source #

optDoubleCheck :: PragmaOptions -> Bool Source #

optCompileNoMain :: PragmaOptions -> Bool Source #

optCaching :: PragmaOptions -> Bool Source #

optAutoInline :: PragmaOptions -> Bool Source #

optPrintPatternSynonyms :: PragmaOptions -> Bool Source #

optFastReduce :: PragmaOptions -> Bool Source #

optCallByName :: PragmaOptions -> Bool Source #

optCohesion :: PragmaOptions -> Bool Source #

`optCohesion` is implied by `optFlatSplit`.

optFlatSplit :: PragmaOptions -> Bool Source #

optImportSorts :: PragmaOptions -> Bool Source #

`optImportSorts` requires `optLoadPrimitives`.

optLoadPrimitives :: PragmaOptions -> Bool Source #

optSaveMetas :: PragmaOptions -> Bool Source #

optShowIdentitySubstitutions :: PragmaOptions -> Bool Source #

optKeepCoveringClauses :: PragmaOptions -> Bool Source #

optLargeIndices :: PragmaOptions -> Bool Source #

optForcedArgumentRecursion :: PragmaOptions -> Bool Source #

optConfluenceCheck :: PragmaOptions -> Maybe ConfluenceCheck Source #

optCubical :: PragmaOptions -> Maybe Cubical Source #

optInstanceSearchDepth :: PragmaOptions -> Int Source #

optInversionMaxDepth :: PragmaOptions -> Int Source #

optProfiling :: PragmaOptions -> ProfileOptions Source #

optSyntacticEquality :: PragmaOptions -> Maybe Int Source #

optVerbose :: PragmaOptions -> Verbosity Source #

optWarningMode :: PragmaOptions -> WarningMode Source #

class (Functor m, Applicative m, Monad m) => HasOptions (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

default pragmaOptions :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions Source #

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

default commandLineOptions :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions Source #

#### Instances

Instances details

HasOptions IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods pragmaOptions :: IM PragmaOptions Source # commandLineOptions :: IM CommandLineOptions Source #
HasOptions TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions Source # commandLineOptions :: TerM CommandLineOptions Source #
HasOptions ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReduceM PragmaOptions Source # commandLineOptions :: ReduceM CommandLineOptions Source #
HasOptions NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods pragmaOptions :: NLM PragmaOptions Source # commandLineOptions :: NLM CommandLineOptions Source #
HasOptions m => HasOptions (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods pragmaOptions :: PureConversionT m PragmaOptions Source # commandLineOptions :: PureConversionT m CommandLineOptions Source #
HasOptions m => HasOptions (BlockT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: BlockT m PragmaOptions Source # commandLineOptions :: BlockT m CommandLineOptions Source #
MonadIO m => HasOptions (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions Source # commandLineOptions :: TCMT m CommandLineOptions Source #
HasOptions m => HasOptions (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods pragmaOptions :: NamesT m PragmaOptions Source # commandLineOptions :: NamesT m CommandLineOptions Source #
HasOptions m => HasOptions (ListT m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ListT m PragmaOptions Source # commandLineOptions :: ListT m CommandLineOptions Source #
HasOptions m => HasOptions (ChangeT m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ChangeT m PragmaOptions Source # commandLineOptions :: ChangeT m CommandLineOptions Source #
HasOptions m => HasOptions (MaybeT m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: MaybeT m PragmaOptions Source # commandLineOptions :: MaybeT m CommandLineOptions Source #
HasOptions m => HasOptions (ExceptT e m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source #
HasOptions m => HasOptions (IdentityT m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: IdentityT m PragmaOptions Source # commandLineOptions :: IdentityT m CommandLineOptions Source #
HasOptions m => HasOptions (ReaderT r m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ReaderT r m PragmaOptions Source # commandLineOptions :: ReaderT r m CommandLineOptions Source #
HasOptions m => HasOptions (StateT s m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: StateT s m PragmaOptions Source # commandLineOptions :: StateT s m CommandLineOptions Source #
(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source # |
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: WriterT w m PragmaOptions Source # commandLineOptions :: WriterT w m CommandLineOptions Source #

data CommandLineOptions Source #

Constructors

Options |

Fields

- 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.

#### Instances

Instances details

LensIncludePaths CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath] Source #

setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions Source #

mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions Source #

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source #

setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions Source #

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions Source #

LensPersistentVerbosity CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensSafeMode CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions Source #
NFData CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: CommandLineOptions -> () Source #
Generic CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep CommandLineOptions |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))))

Methods

from :: CommandLineOptions -> Rep CommandLineOptions x Source #

to :: Rep CommandLineOptions x -> CommandLineOptions Source #

Show CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> CommandLineOptions -> ShowS Source # show :: CommandLineOptions -> String Source # showList :: [CommandLineOptions] -> ShowS Source #
type Rep CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))))

type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel) Source #

`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.

type VerboseKey = String Source #

type VerboseLevel = Int Source #

class LensPragmaOptions a where Source #

Minimal complete definition

lensPragmaOptions

Methods

getPragmaOptions :: a -> PragmaOptions Source #

setPragmaOptions :: PragmaOptions -> a -> a Source #

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> a -> a Source #

lensPragmaOptions :: Lens' a PragmaOptions Source #

#### Instances

Instances details

LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions Source #
LensPragmaOptions PreScopeState Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getPragmaOptions :: PreScopeState -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> PreScopeState -> PreScopeState Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> PreScopeState -> PreScopeState Source # lensPragmaOptions :: Lens' PreScopeState PragmaOptions Source #
LensPragmaOptions TCState Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getPragmaOptions :: TCState -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> TCState -> TCState Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState Source # lensPragmaOptions :: Lens' TCState PragmaOptions Source #

data ConfluenceCheck Source #

Constructors

LocalConfluenceCheck |
GlobalConfluenceCheck |

#### Instances

Instances details

EmbPrj ConfluenceCheck Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Word32 Source # icod_ :: ConfluenceCheck -> S Word32 Source # value :: Word32 -> R ConfluenceCheck Source #
NFData ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: ConfluenceCheck -> () Source #
Generic ConfluenceCheck Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep ConfluenceCheck |
Instance details Defined in Agda.Interaction.Options.Types type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ConfluenceCheck -> Rep ConfluenceCheck x Source #

to :: Rep ConfluenceCheck x -> ConfluenceCheck Source #

Show ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> ConfluenceCheck -> ShowS Source # show :: ConfluenceCheck -> String Source # showList :: [ConfluenceCheck] -> ShowS Source #
Eq ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source # (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source #
type Rep ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions |

Fields

- _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

#### Instances

Instances details

LensPersistentVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Word32 Source # icod_ :: PragmaOptions -> S Word32 Source # value :: Word32 -> R PragmaOptions Source #
NFData PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: PragmaOptions -> () Source #
Generic PragmaOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep PragmaOptions |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))))

Methods

from :: PragmaOptions -> Rep PragmaOptions x Source #

to :: Rep PragmaOptions x -> PragmaOptions Source #

Show PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> PragmaOptions -> ShowS Source # show :: PragmaOptions -> String Source # showList :: [PragmaOptions] -> ShowS Source #
Eq PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: PragmaOptions -> PragmaOptions -> Bool Source # (/=) :: PragmaOptions -> PragmaOptions -> Bool Source #
type Rep PragmaOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))))

data DiagnosticsColours Source #

Constructors

AlwaysColour |
NeverColour |
AutoColour |

#### Instances

Instances details

NFData DiagnosticsColours Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: DiagnosticsColours -> () Source #
Generic DiagnosticsColours Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep DiagnosticsColours |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: DiagnosticsColours -> Rep DiagnosticsColours x Source #

to :: Rep DiagnosticsColours x -> DiagnosticsColours Source #

Show DiagnosticsColours Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> DiagnosticsColours -> ShowS Source # show :: DiagnosticsColours -> String Source # showList :: [DiagnosticsColours] -> ShowS Source #
type Rep DiagnosticsColours Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) (U1 :: Type -> Type)))

data EmacsModeCommand Source #

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`.

#### Instances

Instances details

NFData EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: EmacsModeCommand -> () Source #
Generic EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep EmacsModeCommand |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: EmacsModeCommand -> Rep EmacsModeCommand x Source #

to :: Rep EmacsModeCommand x -> EmacsModeCommand Source #

Show EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> EmacsModeCommand -> ShowS Source # show :: EmacsModeCommand -> String Source # showList :: [EmacsModeCommand] -> ShowS Source #
Eq EmacsModeCommand Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source # (/=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #
Ord EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Methods

compare :: EmacsModeCommand -> EmacsModeCommand -> Ordering Source #

(<) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(<=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(>) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

(>=) :: EmacsModeCommand -> EmacsModeCommand -> Bool Source #

max :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand Source #

min :: EmacsModeCommand -> EmacsModeCommand -> EmacsModeCommand Source #

type Rep EmacsModeCommand Source # |

Instance details

Defined in Agda.Interaction.Options.Types

type Rep EmacsModeCommand = D1 ('MetaData "EmacsModeCommand" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "EmacsModeCompile" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmacsModeSetup" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EmacsModeLocate" 'PrefixI 'False) (U1 :: Type -> Type)))

data PrintAgdaVersion Source #

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

Constructors

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

#### Instances

Instances details

NFData PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: PrintAgdaVersion -> () Source #
Generic PrintAgdaVersion Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep PrintAgdaVersion |
Instance details Defined in Agda.Interaction.Options.Types type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: PrintAgdaVersion -> Rep PrintAgdaVersion x Source #

to :: Rep PrintAgdaVersion x -> PrintAgdaVersion Source #

Show PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> PrintAgdaVersion -> ShowS Source # show :: PrintAgdaVersion -> String Source # showList :: [PrintAgdaVersion] -> ShowS Source #
type Rep PrintAgdaVersion Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

data InfectiveCoinfective Source #

Infective or coinfective?

Constructors

Infective |
Coinfective |

#### Instances

Instances details

EmbPrj InfectiveCoinfective Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Word32 Source # icod_ :: InfectiveCoinfective -> S Word32 Source # value :: Word32 -> R InfectiveCoinfective Source #
NFData InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods rnf :: InfectiveCoinfective -> () Source #
Generic InfectiveCoinfective Source # |

Instance details

Defined in Agda.Interaction.Options.Types

Associated Types

type Rep InfectiveCoinfective |
Instance details Defined in Agda.Interaction.Options.Types type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: InfectiveCoinfective -> Rep InfectiveCoinfective x Source #

to :: Rep InfectiveCoinfective x -> InfectiveCoinfective Source #

Show InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods showsPrec :: Int -> InfectiveCoinfective -> ShowS Source # show :: InfectiveCoinfective -> String Source # showList :: [InfectiveCoinfective] -> ShowS Source #
Eq InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types Methods (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool Source # (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool Source #
type Rep InfectiveCoinfective Source # |
Instance details Defined in Agda.Interaction.Options.Types type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

type VerboseKeyItem = String1 Source #