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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Errors

Contents

Synopsis

Documentation

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

prettyWarning :: MonadTCM tcm => Warning -> tcm Doc #

tcErrString :: TCErr -> String #

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

prettyTCWarnings :: [TCWarning] -> TCM String #

tcWarningsToError :: [TCWarning] -> TCM a #

Turns all warnings into errors.

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

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

dropTopLevelModule :: QName -> TCM QName #

Drops the filename component of the qualified name.

stringTCErr :: String -> TCErr #

sayWhen :: Range -> Maybe (Closure Call) -> TCM Doc -> TCM Doc #

Orphan instances

PrettyTCM TCErr # 
Instance details

Methods

prettyTCM :: TCErr -> TCM Doc #

PrettyTCM TypeError # 
Instance details

Methods

prettyTCM :: TypeError -> TCM Doc #

PrettyTCM UnificationFailure # 
Instance details

Methods

prettyTCM :: UnificationFailure -> TCM Doc #

PrettyTCM NegativeUnification # 
Instance details

Methods

prettyTCM :: NegativeUnification -> TCM Doc #

PrettyTCM SplitError # 
Instance details

Methods

prettyTCM :: SplitError -> TCM Doc #

PrettyTCM CallInfo # 
Instance details

Methods

prettyTCM :: CallInfo -> TCM Doc #

PrettyTCM TCWarning # 
Instance details

Methods

prettyTCM :: TCWarning -> TCM Doc #

PrettyTCM Warning # 
Instance details

Methods

prettyTCM :: Warning -> TCM Doc #

PrettyTCM Call # 
Instance details

Methods

prettyTCM :: Call -> TCM Doc #