Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Errors

Synopsis

Documentation

tcWarningsToError :: [TCWarning] -> TCM a Source #

Turns all warnings into errors.

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

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

dropTopLevelModule :: QName -> TCM QName Source #

Drops the filename component of the qualified name.

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

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

Orphan instances

PrettyTCM TCErr Source # 
Instance details

Methods

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

PrettyTCM TypeError Source # 
Instance details

PrettyTCM UnificationFailure Source # 
Instance details

PrettyTCM NegativeUnification Source # 
Instance details

PrettyTCM SplitError Source # 
Instance details