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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Errors

Contents

- Orphan instances

Synopsis

- prettyError :: MonadTCM tcm => TCErr -> tcm String
- tcErrString :: TCErr -> String
- prettyTCWarnings' :: [TCWarning] -> TCM [String]
- prettyTCWarnings :: [TCWarning] -> TCM String
- tcWarningsToError :: [TCWarning] -> TCM ()
- applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]
- applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]
- getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning]
- getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning]
- getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning]
- getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
- dropTopLevelModule :: QName -> TCM QName
- topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
- stringTCErr :: String -> TCErr

# Documentation

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

tcErrString :: TCErr -> String Source #

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

prettyTCWarnings :: [TCWarning] -> TCM String Source #

tcWarningsToError :: [TCWarning] -> TCM () Source #

Turns warnings, if any, into errors.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning] Source #

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

applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning] Source #

getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning] Source #

getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning] Source #

getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning] Source #

Collect all warnings that have accumulated in the state.

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning] Source #

dropTopLevelModule :: QName -> TCM QName Source #

Drops the filename component of the qualified name.

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

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

stringTCErr :: String -> TCErr Source #

# Orphan instances

PrettyTCM NegativeUnification Source # |
Instance details Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source #
PrettyTCM SplitError Source # |
Instance details Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source #
PrettyTCM TCErr Source # |
Instance details Methods prettyTCM :: MonadPretty m => TCErr -> m Doc Source #
PrettyTCM TypeError Source # |
Instance details Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
PrettyTCM UnificationFailure Source # |
Instance details Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source #