| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Options.Warnings
Synopsis
- data WarningMode = WarningMode {}
- warningSet :: Lens' (Set WarningName) WarningMode
- warn2Error :: Lens' Bool WarningMode
- defaultWarningSet :: String
- allWarnings :: Set WarningName
- usualWarnings :: Set WarningName
- noWarnings :: Set WarningName
- unsolvedWarnings :: Set WarningName
- incompleteMatchWarnings :: Set WarningName
- errorWarnings :: Set WarningName
- defaultWarningMode :: WarningMode
- warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode)
- warningSets :: [(String, (Set WarningName, String))]
- data WarningName
- = OverlappingTokensWarning_
- | LibUnknownField_
- | EmptyAbstract_
- | EmptyField_
- | EmptyGeneralize_
- | EmptyInstance_
- | EmptyMacro_
- | EmptyMutual_
- | EmptyPostulate_
- | EmptyPrimitive_
- | EmptyPrivate_
- | EmptyRewritePragma_
- | InvalidCatchallPragma_
- | InvalidCoverageCheckPragma_
- | InvalidNoPositivityCheckPragma_
- | InvalidNoUniverseCheckPragma_
- | InvalidTerminationCheckPragma_
- | MissingDefinitions_
- | NotAllowedInMutual_
- | OpenPublicAbstract_
- | OpenPublicPrivate_
- | PolarityPragmasButNotPostulates_
- | PragmaCompiled_
- | PragmaNoTerminationCheck_
- | ShadowingInTelescope_
- | UnknownFixityInMixfixDecl_
- | UnknownNamesInFixityDecl_
- | UnknownNamesInPolarityPragmas_
- | UselessAbstract_
- | UselessInstance_
- | UselessPrivate_
- | AbsurdPatternRequiresNoRHS_
- | CantGeneralizeOverSorts_
- | ClashesViaRenaming_
- | CoverageIssue_
- | CoverageNoExactSplit_
- | DeprecationWarning_
- | FixityInRenamingModule_
- | GenericNonFatalError_
- | GenericWarning_
- | IllformedAsClause_
- | InstanceArgWithExplicitArg_
- | InstanceWithExplicitArg_
- | InstanceNoOutputTypeName_
- | InversionDepthReached_
- | ModuleDoesntExport_
- | NotInScope_
- | NotStrictlyPositive_
- | OldBuiltin_
- | PragmaCompileErased_
- | RewriteMaybeNonConfluent_
- | RewriteNonConfluent_
- | SafeFlagEta_
- | SafeFlagInjective_
- | SafeFlagNoCoverageCheck_
- | SafeFlagNonTerminating_
- | SafeFlagNoPositivityCheck_
- | SafeFlagNoUniverseCheck_
- | SafeFlagPolarity_
- | SafeFlagPostulate_
- | SafeFlagPragma_
- | SafeFlagTerminating_
- | SafeFlagWithoutKFlagPrimEraseEquality_
- | TerminationIssue_
- | UnreachableClauses_
- | UnsolvedConstraints_
- | UnsolvedInteractionMetas_
- | UnsolvedMetaVariables_
- | UselessInline_
- | UselessPublic_
- | UserWarning_
- | WithoutKFlagPrimEraseEquality_
- | WrongInstanceDeclaration_
- | CoInfectiveImport_
- | InfectiveImport_
- warningName2String :: WarningName -> String
- string2WarningName :: String -> Maybe WarningName
- usageWarning :: String
Documentation
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
| Eq WarningMode Source # | |
Defined in Agda.Interaction.Options.Warnings | |
| Show WarningMode Source # | |
Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS # show :: WarningMode -> String # showList :: [WarningMode] -> ShowS # | |
| EmbPrj WarningMode Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
defaultWarningSet :: String Source #
The defaultWarningMode is a curated set of warnings covering non-fatal
errors and disabling style-related ones
warningModeUpdate :: String -> Maybe (WarningMode -> WarningMode) Source #
warningModeUpdate str computes the action of str over the current
WarningMode: it may reset the set of warnings, add or remove a specific
flag or demand that any warning be turned into an error
warningSets :: [(String, (Set WarningName, String))] Source #
Common sets of warnings
data WarningName Source #
The WarningName data enumeration is meant to have a one-to-one correspondance
to existing warnings in the codebase.
Constructors
Instances
string2WarningName :: String -> Maybe WarningName Source #
The flag corresponding to a warning is precisely the name of the constructor minus the trailing underscore.
usageWarning :: String Source #
warningUsage generated using warningNameDescription