| 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
- optInteractive :: Bool
- optGHCiInteraction :: Bool
- optJSONInteraction :: Bool
- optExitOnError :: !Bool
- optCompileDir :: Maybe FilePath
- optGenerateVimFile :: Bool
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optLocalInterfaces :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool
- optTransliterate :: Bool
- optDiagnosticsColour :: DiagnosticsColours
- type Flag opts = opts -> OptM opts
- data ArgDescr a
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- defaultOptions :: CommandLineOptions
- data WarningMode = WarningMode {
- _warningSet :: Set WarningName
- _warn2Error :: Bool
- parseVerboseKey :: VerboseKey -> [VerboseKeyItem]
- data UnicodeOrAscii
- optUseUnicode :: PragmaOptions -> UnicodeOrAscii
- defaultCutOff :: CutOff
- optTerminationDepth :: PragmaOptions -> CutOff
- optRewriting :: PragmaOptions -> Bool
- optQualifiedInstances :: PragmaOptions -> Bool
- optFirstOrder :: PragmaOptions -> Bool
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
- data ConfluenceCheck
- optInjectiveTypeConstructors :: PragmaOptions -> Bool
- optCumulativity :: PragmaOptions -> Bool
- optAllowExec :: PragmaOptions -> Bool
- optCountClusters :: 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 'True
- _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
- _optImportSorts :: WithDefault 'True
- _optLoadPrimitives :: WithDefault 'True
- _optAllowExec :: WithDefault 'False
- _optSaveMetas :: WithDefault 'True
- _optShowIdentitySubstitutions :: WithDefault 'False
- _optKeepCoveringClauses :: WithDefault 'False
- _optLargeIndices :: WithDefault 'False
- _optForcedArgumentRecursion :: WithDefault 'True
- data OptionWarning
- = OptionRenamed {
- oldOptionName :: String
- newOptionName :: String
- | WarningProblem WarningModeError
- = OptionRenamed {
- optionWarningName :: OptionWarning -> WarningName
- data OptM a
- runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)
- data PrintAgdaVersion
- data DiagnosticsColours
- 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
- 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 'True -> f (WithDefault 'True)) -> 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
- 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 'True -> f (WithDefault 'True)) -> 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
Documentation
data CommandLineOptions Source #
Constructors
| Options | |
Fields
| |
Instances
| LensIncludePaths CommandLineOptions Source # | |||||
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 # | |||||
Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source # | |||||
| LensPragmaOptions CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions Source # | |||||
| LensSafeMode CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source # | |||||
| NFData CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: CommandLineOptions -> () | |||||
| Generic CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
Methods from :: CommandLineOptions -> Rep CommandLineOptions x to :: Rep CommandLineOptions x -> CommandLineOptions | |||||
| Show CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> CommandLineOptions -> ShowS show :: CommandLineOptions -> String showList :: [CommandLineOptions] -> ShowS | |||||
| type Rep CommandLineOptions Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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 "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 "optLocalInterfaces") '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 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
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
| |
Instances
| EmbPrj WarningMode Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source # | |||||
| NFData WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () | |||||
| Generic WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings Associated Types
| |||||
| Show WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS show :: WarningMode -> String showList :: [WarningMode] -> ShowS | |||||
| Eq WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings | |||||
| type Rep WarningMode Source # | |||||
Defined in Agda.Interaction.Options.Warnings type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.20240714-inplace" '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.
Instances
defaultCutOff :: CutOff Source #
The default termination depth.
optRewriting :: PragmaOptions -> Bool Source #
optQualifiedInstances :: PragmaOptions -> Bool Source #
optFirstOrder :: PragmaOptions -> Bool Source #
type VerboseKey = String Source #
type VerboseLevel = Int Source #
data ConfluenceCheck Source #
Constructors
| LocalConfluenceCheck | |
| GlobalConfluenceCheck |
Instances
| EmbPrj ConfluenceCheck Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Int32 Source # icod_ :: ConfluenceCheck -> S Int32 Source # value :: Int32 -> R ConfluenceCheck Source # | |||||
| NFData ConfluenceCheck Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: ConfluenceCheck -> () | |||||
| Generic ConfluenceCheck Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
Methods from :: ConfluenceCheck -> Rep ConfluenceCheck x to :: Rep ConfluenceCheck x -> ConfluenceCheck | |||||
| Show ConfluenceCheck Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> ConfluenceCheck -> ShowS show :: ConfluenceCheck -> String showList :: [ConfluenceCheck] -> ShowS | |||||
| Eq ConfluenceCheck Source # | |||||
Defined in Agda.Interaction.Options.Base Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool | |||||
| type Rep ConfluenceCheck Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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 #
optCountClusters :: PragmaOptions -> Bool Source #
data PragmaOptions Source #
Options which can be set in a pragma.
Constructors
| PragmaOptions | |
Fields
| |
Instances
| LensPersistentVerbosity PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Lenses | |||||
| LensSafeMode PragmaOptions Source # | |||||
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 # | |||||
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 # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Int32 Source # icod_ :: PragmaOptions -> S Int32 Source # value :: Int32 -> R PragmaOptions Source # | |||||
| NFData PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: PragmaOptions -> () | |||||
| Generic PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
| |||||
| Show PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> PragmaOptions -> ShowS show :: PragmaOptions -> String showList :: [PragmaOptions] -> ShowS | |||||
| Eq PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Base | |||||
| type Rep PragmaOptions Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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 'True)) :*: 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 "_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 'True)) :*: 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)))))))))) | |||||
data OptionWarning Source #
Warnings when parsing options.
Constructors
| OptionRenamed | Name of option changed in a newer version of Agda. |
Fields
| |
| WarningProblem WarningModeError | A problem with setting or unsetting a warning. |
Instances
| Pretty OptionWarning Source # | |||||
Defined in Agda.Interaction.Options.Base Methods pretty :: OptionWarning -> Doc Source # prettyPrec :: Int -> OptionWarning -> Doc Source # prettyList :: [OptionWarning] -> Doc Source # | |||||
| EmbPrj OptionWarning Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OptionWarning -> S Int32 Source # icod_ :: OptionWarning -> S Int32 Source # value :: Int32 -> R OptionWarning Source # | |||||
| NFData OptionWarning Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: OptionWarning -> () | |||||
| Generic OptionWarning Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
| |||||
| Show OptionWarning Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> OptionWarning -> ShowS show :: OptionWarning -> String showList :: [OptionWarning] -> ShowS | |||||
| type Rep OptionWarning Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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))) | |||||
The options parse monad OptM collects warnings that are not discarded
when a fatal error occurrs
data PrintAgdaVersion Source #
Options --version and --numeric-version (last wins).
Constructors
| PrintAgdaVersion | Print Agda version information and exit. |
| PrintAgdaNumericVersion | Print Agda version number and exit. |
Instances
| NFData PrintAgdaVersion Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: PrintAgdaVersion -> () | |||||
| Generic PrintAgdaVersion Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
Methods from :: PrintAgdaVersion -> Rep PrintAgdaVersion x to :: Rep PrintAgdaVersion x -> PrintAgdaVersion | |||||
| Show PrintAgdaVersion Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> PrintAgdaVersion -> ShowS show :: PrintAgdaVersion -> String showList :: [PrintAgdaVersion] -> ShowS | |||||
| type Rep PrintAgdaVersion Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
data DiagnosticsColours Source #
Constructors
| AlwaysColour | |
| NeverColour | |
| AutoColour |
Instances
| NFData DiagnosticsColours Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: DiagnosticsColours -> () | |||||
| Generic DiagnosticsColours Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
Methods from :: DiagnosticsColours -> Rep DiagnosticsColours x to :: Rep DiagnosticsColours x -> DiagnosticsColours | |||||
| Show DiagnosticsColours Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> DiagnosticsColours -> ShowS show :: DiagnosticsColours -> String showList :: [DiagnosticsColours] -> ShowS | |||||
| type Rep DiagnosticsColours Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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))) | |||||
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).
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.
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
| EmbPrj InfectiveCoinfective Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Int32 Source # icod_ :: InfectiveCoinfective -> S Int32 Source # value :: Int32 -> R InfectiveCoinfective Source # | |||||
| NFData InfectiveCoinfective Source # | |||||
Defined in Agda.Interaction.Options.Base Methods rnf :: InfectiveCoinfective -> () | |||||
| Generic InfectiveCoinfective Source # | |||||
Defined in Agda.Interaction.Options.Base Associated Types
Methods from :: InfectiveCoinfective -> Rep InfectiveCoinfective x to :: Rep InfectiveCoinfective x -> InfectiveCoinfective | |||||
| Show InfectiveCoinfective Source # | |||||
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> InfectiveCoinfective -> ShowS show :: InfectiveCoinfective -> String showList :: [InfectiveCoinfective] -> ShowS | |||||
| Eq InfectiveCoinfective Source # | |||||
Defined in Agda.Interaction.Options.Base Methods (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool | |||||
| type Rep InfectiveCoinfective Source # | |||||
Defined in Agda.Interaction.Options.Base type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Base" "Agda-2.6.20240714-inplace" '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
| |
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
| |
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 #
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.
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 System.Console.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 'True -> f (WithDefault 'True)) -> 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 #
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 'True -> f (WithDefault 'True)) -> 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 #
optCubical :: PragmaOptions -> Maybe Cubical Source #
optInstanceSearchDepth :: PragmaOptions -> Int Source #
optInversionMaxDepth :: PragmaOptions -> Int Source #
optSyntacticEquality :: PragmaOptions -> Maybe Int Source #
optVerbose :: PragmaOptions -> Verbosity 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
| HasOptions IM Source # | |
Defined in Agda.Interaction.Monad Methods | |
| HasOptions AbsToCon Source # | |
| HasOptions TerM Source # | |
Defined in Agda.Termination.Monad Methods | |
| HasOptions ReduceM Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| HasOptions NLM Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods | |
| HasOptions m => HasOptions (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure | |
| HasOptions m => HasOptions (BlockT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| MonadIO m => HasOptions (TCMT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| HasOptions m => HasOptions (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names Methods | |
| HasOptions m => HasOptions (ListT m) Source # | |
Defined in Agda.Interaction.Options.HasOptions Methods | |
| HasOptions m => HasOptions (ChangeT m) Source # | |
Defined in Agda.Interaction.Options.HasOptions Methods | |
| HasOptions m => HasOptions (MaybeT m) Source # | |
Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: MaybeT m PragmaOptions Source # commandLineOptions :: MaybeT m CommandLineOptions Source # | |
| HasOptions m => HasOptions (ExceptT e m) Source # | |
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 # | |
Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: IdentityT m PragmaOptions Source # commandLineOptions :: IdentityT m CommandLineOptions Source # | |
| HasOptions m => HasOptions (ReaderT r m) Source # | |
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 # | |
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 # | |
Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: WriterT w m PragmaOptions Source # commandLineOptions :: WriterT w m CommandLineOptions Source # | |