Agda.Interaction.Options.Warnings

Documentation

data 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

Fields

• _warningSet :: Set WarningName
• _warn2Error :: Bool

Instances

Eq WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

(==) :: WarningMode -> WarningMode -> Bool

(/=) :: WarningMode -> WarningMode -> Bool

Show WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningMode -> ShowS

show :: WarningMode -> String

showList :: [WarningMode] -> ShowS

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

warningSet :: Lens' (Set WarningName) WarningMode

warn2Error :: Lens' Bool WarningMode

defaultWarningSet :: String

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

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)

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))]

Common sets of warnings

data WarningName

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

Bounded WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

minBound :: WarningName

maxBound :: WarningName

Enum WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

succ :: WarningName -> WarningName

pred :: WarningName -> WarningName

toEnum :: Int -> WarningName

fromEnum :: WarningName -> Int

enumFrom :: WarningName -> [WarningName]

enumFromThen :: WarningName -> WarningName -> [WarningName]

enumFromTo :: WarningName -> WarningName -> [WarningName]

enumFromThenTo :: WarningName -> WarningName -> WarningName -> [WarningName]

Eq WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

(==) :: WarningName -> WarningName -> Bool

(/=) :: WarningName -> WarningName -> Bool

Ord WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

compare :: WarningName -> WarningName -> Ordering

(<) :: WarningName -> WarningName -> Bool

(<=) :: WarningName -> WarningName -> Bool

(>) :: WarningName -> WarningName -> Bool

(>=) :: WarningName -> WarningName -> Bool

max :: WarningName -> WarningName -> WarningName

min :: WarningName -> WarningName -> WarningName

Read WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

readsPrec :: Int -> ReadS WarningName

readList :: ReadS [WarningName]

readPrec :: ReadPrec WarningName

readListPrec :: ReadPrec [WarningName]

Show WarningName

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningName -> ShowS

show :: WarningName -> String

showList :: [WarningName] -> ShowS

EmbPrj WarningName

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32

icod_ :: WarningName -> S Int32

value :: Int32 -> R WarningName

warningName2String :: WarningName -> String

string2WarningName :: String -> Maybe WarningName

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

usageWarning :: String

warningUsage generated using warningNameDescription