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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Warnings

Synopsis

Documentation

genericWarning :: MonadTCM tcm => Doc -> tcm () 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

onlyOnce :: Warning -> Bool Source #

Should we only emit a single warning with this constructor.

runPM :: PM a -> TCM a Source #

running the Parse monad