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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Pretty.Warning

Contents

- Orphan instances

Synopsis

- applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning)
- applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning)
- filterTCWarnings :: Set TCWarning -> TCM [TCWarning]
- getAllUnsolvedWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]
- getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning)
- getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning)
- getAllWarningsPreserving :: (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning)
- prettyDuplicateFields :: MonadPretty m => List1 Name -> m Doc
- prettyTCWarnings :: Set TCWarning -> TCM String
- prettyTCWarnings' :: Set TCWarning -> TCM [Doc]
- prettyTooManyFields :: MonadPretty m => QName -> [Name] -> List1 Name -> m Doc
- prettyWarning :: MonadPretty m => Warning -> m Doc
- tcWarningsToError :: [TCWarning] -> TCM ()

# Documentation

applyFlagsToTCWarnings :: HasOptions m => Set TCWarning -> m (Set TCWarning) Source #

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> Set TCWarning -> m (Set TCWarning) Source #

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

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

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

getAllUnsolvedWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning] Source #

getAllWarnings :: (ReadTCState m, MonadWarning m, MonadTCM m) => WhichWarnings -> m (Set TCWarning) Source #

Collect all warnings that have accumulated in the state.

getAllWarningsOfTCErr :: TCErr -> TCM (Set TCWarning) Source #

getAllWarningsPreserving :: (ReadTCState m, MonadWarning m, MonadTCM m) => Set WarningName -> WhichWarnings -> m (Set TCWarning) Source #

prettyDuplicateFields :: MonadPretty m => List1 Name -> m Doc Source #

prettyTCWarnings :: Set TCWarning -> TCM String Source #

prettyTCWarnings' :: Set TCWarning -> TCM [Doc] Source #

prettyTooManyFields :: MonadPretty m => QName -> [Name] -> List1 Name -> m Doc Source #

prettyWarning :: MonadPretty m => Warning -> m Doc Source #

tcWarningsToError :: [TCWarning] -> TCM () Source #

Turns warnings, if any, into errors.

# Orphan instances

PrettyTCM DataOrRecord_ Source # |
Instance details Methods prettyTCM :: MonadPretty m => DataOrRecord_ -> m Doc Source #
PrettyTCM TCWarning Source # |
Instance details Methods prettyTCM :: MonadPretty m => TCWarning -> m Doc Source #
PrettyTCM Warning Source # |
Instance details Methods prettyTCM :: MonadPretty m => Warning -> m Doc Source #