Agda.TypeChecking.Errors

Documentation

prettyError :: MonadTCM tcm => TCErr -> tcm String

prettyWarning :: MonadPretty m => Warning -> m Doc

tcErrString :: TCErr -> String

prettyTCWarnings' :: [TCWarning] -> TCM [String]

prettyTCWarnings :: [TCWarning] -> TCM String

tcWarningsToError :: [TCWarning] -> TCM a

Turns all warnings into errors.

applyFlagsToTCWarnings' :: MainInterface -> [TCWarning] -> TCM [TCWarning]

Depending which flags are set, one may happily ignore some warnings.

applyFlagsToTCWarnings :: [TCWarning] -> TCM [TCWarning]

dropTopLevelModule :: QName -> TCM QName

Drops the filename component of the qualified name.

topLevelModuleDropper :: (MonadTCEnv m, ReadTCState m) => m (QName -> QName)

Produces a function which drops the filename component of the qualified name.

stringTCErr :: String -> TCErr

Orphan instances

PrettyTCM TCErr

Methods

prettyTCM :: MonadPretty m => TCErr -> m Doc

PrettyTCM TypeError

Methods

prettyTCM :: MonadPretty m => TypeError -> m Doc

PrettyTCM UnificationFailure

Methods

prettyTCM :: MonadPretty m => UnificationFailure -> m Doc

PrettyTCM NegativeUnification

Methods

prettyTCM :: MonadPretty m => NegativeUnification -> m Doc

PrettyTCM SplitError

Methods

prettyTCM :: MonadPretty m => SplitError -> m Doc