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

Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Errors

Contents

Orphan instances

Synopsis

renderError :: MonadTCM tcm => TCErr -> tcm String
prettyError :: MonadTCM tcm => TCErr -> tcm Doc
tcErrString :: TCErr -> String
prettyTCWarnings' :: [TCWarning] -> TCM [Doc]
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, MonadTCM m) => m [TCWarning]
getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
dropTopLevelModule :: MonadPretty m => QName -> m QName
topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
stringTCErr :: String -> TCErr
explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc
class Verbalize a where
- verbalize :: a -> String

Documentation

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

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

tcErrString :: TCErr -> String Source #

prettyTCWarnings' :: [TCWarning] -> TCM [Doc] 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, MonadTCM m) => m [TCWarning] Source #

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

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

Collect all warnings that have accumulated in the state.

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

dropTopLevelModule :: MonadPretty m => QName -> m 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 #

explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc Source #

class Verbalize a where Source #

Methods

verbalize :: a -> String Source #

Instances

Instances details

Verbalize Cohesion Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Cohesion -> String Source #
Verbalize Hiding Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Hiding -> String Source #
Verbalize Modality Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Modality -> String Source #
Verbalize Quantity Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Quantity -> String Source #
Verbalize Relevance Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Relevance -> String 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 #