| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Warnings
Contents
Synopsis
- class (MonadPretty m, MonadError TCErr m) => MonadWarning m where
- addWarning :: TCWarning -> m ()
- genericWarning :: MonadWarning m => Doc -> m ()
- genericNonFatalError :: MonadWarning m => Doc -> m ()
- warning_ :: MonadWarning m => Warning -> m TCWarning
- warning :: MonadWarning m => Warning -> m ()
- warnings :: MonadWarning m => [Warning] -> m ()
- isUnsolvedWarning :: Warning -> Bool
- isMetaWarning :: Warning -> Bool
- isMetaTCWarning :: TCWarning -> Bool
- onlyShowIfUnsolved :: Warning -> Bool
- data WhichWarnings
- classifyWarning :: Warning -> WhichWarnings
- data WarningsAndNonFatalErrors
- tcWarnings :: WarningsAndNonFatalErrors -> [TCWarning]
- nonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning]
- emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors
- classifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors
- runPM :: PM a -> TCM a
Documentation
class (MonadPretty m, MonadError TCErr m) => MonadWarning m where Source #
Instances
| MonadWarning TCM Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> TCM () Source # | |
| (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m) => MonadWarning (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods addWarning :: TCWarning -> PureConversionT m () Source # | |
| MonadWarning m => MonadWarning (ReaderT r m) Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> ReaderT r m () Source # | |
| MonadWarning m => MonadWarning (StateT s m) Source # | |
Defined in Agda.TypeChecking.Warnings Methods addWarning :: TCWarning -> StateT s m () Source # | |
genericWarning :: MonadWarning m => Doc -> m () Source #
genericNonFatalError :: MonadWarning m => Doc -> m () Source #
warning :: MonadWarning m => Warning -> m () Source #
warnings :: MonadWarning m => [Warning] -> m () Source #
isUnsolvedWarning :: Warning -> Bool Source #
isMetaWarning :: Warning -> Bool Source #
isMetaTCWarning :: TCWarning -> Bool Source #
onlyShowIfUnsolved :: Warning -> Bool 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 # | |
Defined in Agda.TypeChecking.Warnings Methods (==) :: WhichWarnings -> WhichWarnings -> Bool # (/=) :: WhichWarnings -> WhichWarnings -> Bool # | |
| Ord WhichWarnings Source # | |
Defined in Agda.TypeChecking.Warnings Methods compare :: WhichWarnings -> WhichWarnings -> Ordering # (<) :: WhichWarnings -> WhichWarnings -> Bool # (<=) :: WhichWarnings -> WhichWarnings -> Bool # (>) :: WhichWarnings -> WhichWarnings -> Bool # (>=) :: WhichWarnings -> WhichWarnings -> Bool # max :: WhichWarnings -> WhichWarnings -> WhichWarnings # min :: WhichWarnings -> WhichWarnings -> WhichWarnings # | |
data WarningsAndNonFatalErrors Source #
Assorted warnings and errors to be displayed to the user
emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors Source #
The only way to construct a empty WarningsAndNonFatalErrors