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

Agda.TypeChecking.Pretty.Warning

Synopsis

Documentation

prettyWarningName :: MonadPretty m => WarningName -> m Doc Source #

Prefix for a warning text showing name of the warning. E.g. warning: -W[no]warning_name

prettyNotInScopeNames Source #

Arguments

:: (MonadPretty m, Pretty a, HasRange a) 
=> Bool

Print range?

-> (a -> m Doc)

Correction suggestion generator.

-> [a]

Names that are not in scope.

-> m Doc 

Report a number of names that are not in scope.

didYouMean Source #

Arguments

:: (MonadPretty m, Pretty a, Pretty b) 
=> [QName]

Names in scope.

-> (a -> b)

Canonization function for similarity search.

-> a

A name which is not in scope.

-> Maybe (m Doc)

"did you mean" hint.

Suggest some corrections to a misspelled name.

filterTCWarnings :: [TCWarning] -> [TCWarning] Source #

If there are several warnings, remove the unsolved-constraints warning in case there are no interesting constraints to list.

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, MonadTCM m) => WhichWarnings -> m [TCWarning] Source #

Collect all warnings that have accumulated in the state.

Orphan instances

PrettyTCM TCWarning Source # 
Instance details