Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Warnings

Synopsis

Documentation

class (MonadPretty m, MonadError TCErr m) => MonadWarning (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

addWarning :: TCWarning -> m () Source #

Store a warning and generate highlighting from it.

default addWarning :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (MonadWarning n, MonadTrans t, t n ~ m) => TCWarning -> m () Source #

Instances

Instances details
MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadWarning m => MonadWarning (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> ReaderT r m () Source #

MonadWarning m => MonadWarning (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> StateT s m () Source #

raiseWarningsOnUsage :: (MonadWarning m, ReadTCState m) => QName -> m () Source #

Raise every WARNING_ON_USAGE connected to a name.

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

data WarningsAndNonFatalErrors Source #

Assorted warnings and errors to be displayed to the user

emptyWarningsAndNonFatalErrors :: WarningsAndNonFatalErrors Source #

The only way to construct a empty WarningsAndNonFatalErrors

runPM :: PM a -> TCM a Source #

running the Parse monad