Agda.TypeChecking.Warnings

Documentation

genericWarning :: MonadTCM tcm => Doc -> tcm ()

genericNonFatalError :: MonadTCM tcm => Doc -> tcm ()

warning_ :: MonadTCM tcm => Warning -> tcm TCWarning

warning :: MonadTCM tcm => Warning -> tcm ()

data 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

Instances

Eq WhichWarnings

Methods

(==) :: WhichWarnings -> WhichWarnings -> Bool

(/=) :: WhichWarnings -> WhichWarnings -> Bool

Ord WhichWarnings

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

isUnsolvedWarning :: Warning -> Bool

classifyWarning :: Warning -> WhichWarnings

classifyWarnings :: [TCWarning] -> ([TCWarning], [TCWarning])

runPM :: PM a -> TCM a

running the Parse monad