ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Pretty.Warning

valueprettyWarningName :: MonadPretty m => WarningName -> m Doc

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

valueprettyWarning :: MonadPretty m => Warning -> m Doc

valueprettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc

valueprettyDuplicateFields :: MonadPretty m => [Name] -> m Doc

valueprettyTooManyFields :: MonadPretty m => QName -> [Name] -> [Name] -> m Doc

valueprettyNotInScopeNames

Report a number of names that are not in scope.

valuedidYouMean

Suggest some corrections to a misspelled name.

valueprettyTCWarnings :: [TCWarning] -> TCM String

valueprettyTCWarnings' :: [TCWarning] -> TCM [Doc]

valuefilterTCWarnings :: [TCWarning] -> [TCWarning]

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

valuetcWarningsToError :: [TCWarning] -> TCM ()

Turns warnings, if any, into errors.

valueapplyFlagsToTCWarningsPreserving

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

valueapplyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]

valueisBoundaryConstraint

valuegetAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]

valuegetAllWarnings

Collect all warnings that have accumulated in the state.

valuegetAllWarningsPreserving

valuegetAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]

Orphan instances

1 instance