Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Errors

Synopsis

Documentation

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.

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

Collect all warnings that have accumulated in the state.

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.

class Verbalize a where Source #

Methods

verbalize :: a -> String Source #

Instances

Instances details
Verbalize Cohesion Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Verbalize Hiding Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Verbalize Modality Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Verbalize Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Verbalize Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Orphan instances

PrettyTCM NegativeUnification Source # 
Instance details

PrettyTCM SplitError Source # 
Instance details

PrettyTCM TCErr Source # 
Instance details

Methods

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

PrettyTCM TypeError Source # 
Instance details

PrettyTCM UnificationFailure Source # 
Instance details