ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Errors
Synopsis
- value renderError
- value prettyError
- value tcErrString
- value prettyTCWarnings'
- value prettyTCWarnings
- value tcWarningsToError
- value applyFlagsToTCWarningsPreserving
- value applyFlagsToTCWarnings
- value getAllUnsolvedWarnings
- value getAllWarningsPreserving
- value getAllWarnings
- value getAllWarningsOfTCErr
- value dropTopLevelModule
- value topLevelModuleDropper
- value explainWhyInScope
- class Verbalize
- PackageAgda-2.8.0.2
- Exports16
- LanguageHaskell2010
- LicenceMIT
- SourceWarning.hs
Turns warnings, if any, into errors.
Depending which flags are set, one may happily ignore some warnings.
Collect all warnings that have accumulated in the state.
Drops the filename component of the qualified name.
value
topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)Produces a function which drops the filename component of the qualified name.
Instances8Verbalize, …
Verbalize CohesionDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.ErrorsVerbalize a => Verbalize (Indefinite a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Errors