Agda.TypeChecking.Warnings · Agda-2.7.0.1

classclass (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where

#

Methods

addWarning :: TCWarning -> m ()
Store a warning and generate highlighting from it.

Instances4MonadWarning

MonadWarning TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Warnings
(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
MonadWarning m => MonadWarning (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Warnings
MonadWarning m => MonadWarning (StateT s m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Warnings

valuewarning'_ :: MonadWarning m => CallStack -> Warning -> m TCWarning

#

valuewarning_ :: (HasCallStack, MonadWarning m) => Warning -> m TCWarning

#

valuewarning' :: MonadWarning m => CallStack -> Warning -> m ()

#

valuewarning :: (HasCallStack, MonadWarning m) => Warning -> m ()

#

valuewarnings :: (HasCallStack, MonadWarning m) => [Warning] -> m ()

#

valueraiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m ()

#

Raise every WARNING_ON_USAGE connected to a name.

valueisUnsolvedWarning :: Warning -> Bool

#

valueisMetaWarning :: Warning -> Bool

#

valueisMetaTCWarning :: TCWarning -> Bool

#

valueonlyShowIfUnsolved :: Warning -> Bool

#

datadata WhichWarnings

#

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

Instances2Eq, Ord

Eq WhichWarningsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Warnings
Ord WhichWarningsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Warnings

valueclassifyWarning :: Warning -> WhichWarnings

#

datadata WarningsAndNonFatalErrors

#

Assorted warnings and errors to be displayed to the user

Instances2EncodeTCM

EncodeTCM DisplayInfoDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM ResponseDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan

valuetcWarnings :: WarningsAndNonFatalErrors -> [TCWarning]

#

valuenonFatalErrors :: WarningsAndNonFatalErrors -> [TCWarning]

#

valueemptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors

#

The only way to construct a empty WarningsAndNonFatalErrors

valueclassifyWarnings :: [TCWarning] -> WarningsAndNonFatalErrors

#

valuerunPM :: PM a -> TCM a

#

running the Parse monad