Agda-2.6.1.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 where Source #

Methods

addWarning :: TCWarning -> m () Source #

Render the warning

Instances

Instances details
MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

(MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins 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 #

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

Orphan instances

Semigroup (TCM Doc) Source # 
Instance details

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc #

stimes :: Integral b => b -> TCM Doc -> TCM Doc #

Applicative m => Semigroup (ReaderT s m Doc) Source # 
Instance details

Methods

(<>) :: ReaderT s m Doc -> ReaderT s m Doc -> ReaderT s m Doc #

sconcat :: NonEmpty (ReaderT s m Doc) -> ReaderT s m Doc #

stimes :: Integral b => b -> ReaderT s m Doc -> ReaderT s m Doc #

Monad m => Semigroup (StateT s m Doc) Source # 
Instance details

Methods

(<>) :: StateT s m Doc -> StateT s m Doc -> StateT s m Doc #

sconcat :: NonEmpty (StateT s m Doc) -> StateT s m Doc #

stimes :: Integral b => b -> StateT s m Doc -> StateT s m Doc #