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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Warnings

Synopsis

- genericWarning :: MonadTCM tcm => Doc -> tcm ()
- genericNonFatalError :: MonadTCM tcm => Doc -> tcm ()
- warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
- applyWarningMode :: WarningMode -> Warning -> Maybe Warning
- warnings :: MonadTCM tcm => [Warning] -> tcm ()
- warning :: MonadTCM tcm => Warning -> tcm ()
- data WhichWarnings
  - = ErrorWarnings
  - | AllWarnings
- isUnsolvedWarning :: Warning -> Bool
- classifyWarning :: Warning -> WhichWarnings
- onlyOnce :: Warning -> Bool
- onlyShowIfUnsolved :: Warning -> Bool
- classifyWarnings :: [TCWarning] -> ([TCWarning], [TCWarning])
- runPM :: PM a -> TCM a

# Documentation

genericWarning :: MonadTCM tcm => Doc -> tcm () Source #

genericNonFatalError :: MonadTCM tcm => Doc -> tcm () Source #

warning_ :: MonadTCM tcm => Warning -> tcm TCWarning Source #

applyWarningMode :: WarningMode -> Warning -> Maybe Warning Source #

`applyWarningMode` filters out the warnings the user has not requested Users are not allowed to ignore non-fatal errors.

warnings :: MonadTCM tcm => [Warning] -> tcm () Source #

warning :: MonadTCM tcm => Warning -> tcm () Source #

data WhichWarnings Source #

Classifying warnings: some are benign, others are (non-fatal) errors

Constructors

ErrorWarnings | warnings that will be turned into errors
AllWarnings | all warnings, including errors and benign ones Note: order of constructors is important for the derived Ord instance

Instances

Eq WhichWarnings Source # |
Instance details Defined in Agda.TypeChecking.Warnings Methods (==) :: WhichWarnings -> WhichWarnings -> Bool Source # (/=) :: WhichWarnings -> WhichWarnings -> Bool Source #
Ord WhichWarnings Source # |

Instance details

Defined in Agda.TypeChecking.Warnings

Methods

compare :: WhichWarnings -> WhichWarnings -> Ordering Source #

(<) :: WhichWarnings -> WhichWarnings -> Bool Source #

(<=) :: WhichWarnings -> WhichWarnings -> Bool Source #

(>) :: WhichWarnings -> WhichWarnings -> Bool Source #

(>=) :: WhichWarnings -> WhichWarnings -> Bool Source #

max :: WhichWarnings -> WhichWarnings -> WhichWarnings Source #

min :: WhichWarnings -> WhichWarnings -> WhichWarnings Source #

isUnsolvedWarning :: Warning -> Bool Source #

classifyWarning :: Warning -> WhichWarnings Source #

onlyOnce :: Warning -> Bool Source #

Should we only emit a single warning with this constructor.

onlyShowIfUnsolved :: Warning -> Bool Source #

classifyWarnings :: [TCWarning] -> ([TCWarning], [TCWarning]) Source #

runPM :: PM a -> TCM a Source #

running the Parse monad