Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
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.

Constructors

WarningMode 

Fields

Instances
Eq WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

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

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

Show WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningMode -> ShowS

show :: WarningMode -> String

showList :: [WarningMode] -> ShowS

EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32 Source #

icod_ :: WarningMode -> S Int32 Source #

value :: Int32 -> R WarningMode Source #

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.

Instances
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

Methods

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

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

Ord WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Read WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

readsPrec :: Int -> ReadS WarningName

readList :: ReadS [WarningName]

readPrec :: ReadPrec WarningName

readListPrec :: ReadPrec [WarningName]

Show WarningName Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningName -> ShowS

show :: WarningName -> String

showList :: [WarningName] -> ShowS

EmbPrj WarningName Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningName -> S Int32 Source #

icod_ :: WarningName -> S Int32 Source #

value :: Int32 -> R WarningName Source #

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