ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Options.Warnings

Synopsis

data WarningMode
value warningSet
value warn2Error
value lensSingleWarning
value defaultWarningSet
value allWarnings
value usualWarnings
value noWarnings
value unsolvedWarnings
value incompleteMatchWarnings
value errorWarnings
value exactSplitWarnings
value defaultWarningMode
data WarningModeError
value prettyWarningModeError
value warningModeUpdate
value warningSets
data WarningName
value warningName2String
value string2WarningName
value usageWarning

PackageAgda-2.8.0.2
Exports21
LanguageHaskell2010
LicenceMIT
SourceWarnings.hs

datadata WarningMode

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

Constructors

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

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

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

valuewarningSet :: Lens' WarningMode (Set WarningName)

valuewarn2Error :: Lens' WarningMode Bool

valuelensSingleWarning :: WarningName -> Lens' WarningMode Bool

valuedefaultWarningSet :: String

Source#

The defaultWarningMode is a curated set of warnings covering non-fatal errors and disabling style-related ones

valueallWarnings :: Set WarningName

valueusualWarnings :: Set WarningName

valuenoWarnings :: Set WarningName

valueunsolvedWarnings :: Set WarningName

valueincompleteMatchWarnings :: Set WarningName

valueerrorWarnings :: Set WarningName

valueexactSplitWarnings :: Set WarningName

Source#

Warnings enabled by --exact-split.

valuedefaultWarningMode :: WarningMode

datadata WarningModeError

Source#

Some warnings are errors and cannot be turned off.

Constructors

Unknown Text
Unknown warning.
NoNoError Text
Warning that cannot be disabled.

Instances5Show, Generic, NFData, EmbPrj, Rep

Show WarningModeErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Generic WarningModeErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
NFData WarningModeErrorDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
EmbPrj WarningModeErrorDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep WarningModeError = D1 ('MetaData "WarningModeError" "Agda.Interaction.Options.Warnings" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Unknown" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "NoNoError" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings

valueprettyWarningModeError :: WarningModeError -> Text

valuewarningModeUpdate :: String -> Either WarningModeError WarningModeUpdate

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

valuewarningSets :: [(String, (Set WarningName, String))]

Source#

Common sets of warnings

datadata WarningName

Source#

The WarningName data enumeration is meant to have a one-to-one correspondance to existing warnings in the codebase.

Constructors

OptionRenamed_
WarningProblem_
Some warning could not be set or unset. Parser Warnings
OverlappingTokensWarning_
MisplacedAttributes_
UnknownPolarity_
UnknownAttribute_
UnsupportedAttribute_
MultipleAttributes_
LibUnknownField_
EmptyAbstract_
EmptyConstructor_
EmptyField_
EmptyGeneralize_
EmptyInstance_
EmptyMacro_
EmptyMutual_
EmptyPostulate_
EmptyPrimitive_
EmptyPrivate_
EmptyRewritePragma_
EmptyWhere_
EmptyPolarityPragma_
HiddenGeneralize_
InvalidCatchallPragma_
InvalidConstructorBlock_
InvalidCoverageCheckPragma_
InvalidNoPositivityCheckPragma_
InvalidNoUniverseCheckPragma_
DuplicateRecordDirective_
InvalidTerminationCheckPragma_
MissingDataDeclaration_
MissingDefinitions_
NotAllowedInMutual_
OpenImportAbstract_
OpenImportPrivate_
PolarityPragmasButNotPostulates_
PragmaCompiled_
PragmaNoTerminationCheck_
ShadowingInTelescope_
UnknownFixityInMixfixDecl_
UnknownNamesInFixityDecl_
UnknownNamesInPolarityPragmas_
UselessAbstract_
UselessInstance_
UselessMacro_
UselessPrivate_
AbsurdPatternRequiresAbsentRHS_
AsPatternShadowsConstructorOrPatternSynonym_
PatternShadowsConstructor_
CantGeneralizeOverSorts_
ClashesViaRenaming_
CoverageIssue_
CoverageNoExactSplit_
InlineNoExactSplit_
DeprecationWarning_
DuplicateUsing_
FixingCohesion_
FixingPolarity_
FixingRelevance_
FixityInRenamingModule_
InvalidCharacterLiteral_
UselessPragma_
IllformedAsClause_
InstanceArgWithExplicitArg_
InstanceWithExplicitArg_
InstanceNoOutputTypeName_
InteractionMetaBoundaries_
InversionDepthReached_
ModuleDoesntExport_
NotInScope_
NotStrictlyPositive_
ConstructorDoesNotFitInData_
CoinductiveEtaRecord_
UnsupportedIndexedMatch_
OldBuiltin_
BuiltinDeclaresIdentifier_
PlentyInHardCompileTimeMode_
PragmaCompileErased_
PragmaCompileList_
PragmaCompileMaybe_
PragmaCompileUnparsable_
PragmaCompileWrong_
PragmaCompileWrongName_
PragmaExpectsDefinedSymbol_
PragmaExpectsUnambiguousConstructorOrFunction_
PragmaExpectsUnambiguousProjectionOrFunction_
NoMain_
NotARewriteRule_
RewriteLHSNotDefinitionOrConstructor_
RewriteVariablesNotBoundByLHS_
RewriteVariablesBoundMoreThanOnce_
RewriteLHSReduces_
RewriteHeadSymbolIsProjectionLikeFunction_
RewriteHeadSymbolIsTypeConstructor_
RewriteHeadSymbolContainsMetas_
RewriteConstructorParametersNotGeneral_
RewriteContainsUnsolvedMetaVariables_
RewriteBlockedOnProblems_
RewriteRequiresDefinitions_
RewriteDoesNotTargetRewriteRelation_
RewriteBeforeFunctionDefinition_
RewriteBeforeMutualFunctionDefinition_
ConfluenceCheckingIncompleteBecauseOfMeta_
ConfluenceForCubicalNotSupported_
RewriteMaybeNonConfluent_
RewriteNonConfluent_
RewriteAmbiguousRules_
RewriteMissingRule_
DuplicateRewriteRule_
SafeFlagEta_
SafeFlagInjective_
SafeFlagNoCoverageCheck_
SafeFlagNonTerminating_
SafeFlagNoPositivityCheck_
SafeFlagNoUniverseCheck_
SafeFlagPolarity_
SafeFlagPostulate_
SafeFlagPragma_
SafeFlagTerminating_
SafeFlagWithoutKFlagPrimEraseEquality_
TerminationIssue_
TooManyArgumentsToSort_
UnreachableClauses_
UnsolvedConstraints_
UnsolvedInteractionMetas_
UnsolvedMetaVariables_
UselessHiding_
UselessInline_
UselessPatternDeclarationForRecord_
UselessPublic_
UselessTactic_
UserWarning_
InvalidDisplayForm_
UnusedVariablesInDisplayForm_
RewritesNothing_
WithClauseProjectionFixityMismatch_
WithoutKFlagPrimEraseEquality_
ConflictingPragmaOptions_
WrongInstanceDeclaration_
TooManyPolarities_
TopLevelPolarity_
CoInfectiveImport_
InfectiveImport_
DuplicateFields_
TooManyFields_
MissingTypeSignatureForOpaque_
NotAffectedByOpaque_
UnfoldingWrongName_
UnfoldTransparentName_
UselessOpaque_
HiddenNotInArgumentPosition_
InstanceNotInArgumentPosition_
MacroInLetBindings_
AbstractInLetBindings_
FaceConstraintCannotBeHidden_
FaceConstraintCannotBeNamed_
CustomBackendWarning_

Instances10Bounded, Enum, Eq, Ord, Read, Show, …

Bounded WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Enum WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Eq WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Ord WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Read WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Show WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
Generic WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
NFData WarningNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings
EmbPrj WarningNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep WarningName = D1 ('MetaData "WarningName" "Agda.Interaction.Options.Warnings" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (((((((C1 ('MetaCons "OptionRenamed_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WarningProblem_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "OverlappingTokensWarning_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MisplacedAttributes_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "UnknownPolarity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnknownAttribute_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnsupportedAttribute_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MultipleAttributes_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "LibUnknownField_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "EmptyAbstract_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyConstructor_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "EmptyField_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "EmptyGeneralize_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyInstance_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "EmptyMacro_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyMutual_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "EmptyPostulate_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "EmptyPrimitive_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyPrivate_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "EmptyRewritePragma_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyWhere_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "EmptyPolarityPragma_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "HiddenGeneralize_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidCatchallPragma_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "InvalidConstructorBlock_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidCoverageCheckPragma_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InvalidNoPositivityCheckPragma_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "InvalidNoUniverseCheckPragma_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateRecordDirective_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "InvalidTerminationCheckPragma_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MissingDataDeclaration_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "MissingDefinitions_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotAllowedInMutual_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OpenImportAbstract_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "OpenImportPrivate_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PolarityPragmasButNotPostulates_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "PragmaCompiled_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "PragmaNoTerminationCheck_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ShadowingInTelescope_" 'PrefixI 'False) U1)))))) :+: (((((C1 ('MetaCons "UnknownFixityInMixfixDecl_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnknownNamesInFixityDecl_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnknownNamesInPolarityPragmas_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UselessAbstract_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "UselessInstance_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UselessMacro_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UselessPrivate_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "AbsurdPatternRequiresAbsentRHS_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AsPatternShadowsConstructorOrPatternSynonym_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "PatternShadowsConstructor_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CantGeneralizeOverSorts_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ClashesViaRenaming_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CoverageIssue_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CoverageNoExactSplit_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "InlineNoExactSplit_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DeprecationWarning_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DuplicateUsing_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "FixingCohesion_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FixingPolarity_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "FixingRelevance_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FixityInRenamingModule_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InvalidCharacterLiteral_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "UselessPragma_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllformedAsClause_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "InstanceArgWithExplicitArg_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InstanceWithExplicitArg_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InstanceNoOutputTypeName_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "InteractionMetaBoundaries_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InversionDepthReached_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "ModuleDoesntExport_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotInScope_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NotStrictlyPositive_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ConstructorDoesNotFitInData_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CoinductiveEtaRecord_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "UnsupportedIndexedMatch_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OldBuiltin_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "BuiltinDeclaresIdentifier_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "PlentyInHardCompileTimeMode_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PragmaCompileErased_" 'PrefixI 'False) U1))))))) :+: ((((((C1 ('MetaCons "PragmaCompileList_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PragmaCompileMaybe_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "PragmaCompileUnparsable_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PragmaCompileWrong_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "PragmaCompileWrongName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PragmaExpectsDefinedSymbol_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "PragmaExpectsUnambiguousConstructorOrFunction_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "PragmaExpectsUnambiguousProjectionOrFunction_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoMain_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "NotARewriteRule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteLHSNotDefinitionOrConstructor_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RewriteVariablesNotBoundByLHS_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "RewriteVariablesBoundMoreThanOnce_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteLHSReduces_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "RewriteHeadSymbolIsProjectionLikeFunction_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteHeadSymbolIsTypeConstructor_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RewriteHeadSymbolContainsMetas_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "RewriteConstructorParametersNotGeneral_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteContainsUnsolvedMetaVariables_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "RewriteBlockedOnProblems_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteRequiresDefinitions_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RewriteDoesNotTargetRewriteRelation_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "RewriteBeforeFunctionDefinition_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteBeforeMutualFunctionDefinition_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "ConfluenceCheckingIncompleteBecauseOfMeta_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConfluenceForCubicalNotSupported_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RewriteMaybeNonConfluent_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "RewriteNonConfluent_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RewriteAmbiguousRules_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "RewriteMissingRule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateRewriteRule_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SafeFlagEta_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "SafeFlagInjective_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SafeFlagNoCoverageCheck_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "SafeFlagNonTerminating_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SafeFlagNoPositivityCheck_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SafeFlagNoUniverseCheck_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "SafeFlagPolarity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SafeFlagPostulate_" 'PrefixI 'False) U1)))))) :+: (((((C1 ('MetaCons "SafeFlagPragma_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SafeFlagTerminating_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SafeFlagWithoutKFlagPrimEraseEquality_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "TerminationIssue_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "TooManyArgumentsToSort_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "UnreachableClauses_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnsolvedConstraints_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnsolvedInteractionMetas_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "UnsolvedMetaVariables_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UselessHiding_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "UselessInline_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UselessPatternDeclarationForRecord_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UselessPublic_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "UselessTactic_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UserWarning_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "InvalidDisplayForm_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnusedVariablesInDisplayForm_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RewritesNothing_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "WithClauseProjectionFixityMismatch_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WithoutKFlagPrimEraseEquality_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "ConflictingPragmaOptions_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongInstanceDeclaration_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "TooManyPolarities_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "TopLevelPolarity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CoInfectiveImport_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "InfectiveImport_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MissingTypeSignatureForOpaque_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotAffectedByOpaque_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "UnfoldingWrongName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnfoldTransparentName_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UselessOpaque_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "HiddenNotInArgumentPosition_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InstanceNotInArgumentPosition_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "MacroInLetBindings_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AbstractInLetBindings_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "FaceConstraintCannotBeHidden_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "FaceConstraintCannotBeNamed_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CustomBackendWarning_" 'PrefixI 'False) U1))))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Warnings

valuewarningName2String :: WarningName -> String

valuestring2WarningName :: String -> Maybe WarningName

Source#

The flag corresponding to a warning is precisely the name of the constructor minus the trailing underscore.

valueusageWarning :: String

Source#

warningUsage generated using warningNameDescription