Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Options.Warnings

Synopsis

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.

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

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_ 

Instances

Instances details
Bounded WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Enum WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Eq WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Ord WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Read WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Show WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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