ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Errors
- 1 class
- 16 values
- PackageAgda-2.7.0.1
- Exports17
- LanguageHaskell2010
- LicenceMIT
- SourceWarning.hs
Turns warnings, if any, into errors.
Depending which flags are set, one may happily ignore some warnings.
value
getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) => m [TCWarning]Collect all warnings that have accumulated in the state.
Drops the filename component of the qualified name.
Produces a function which drops the filename component of the qualified name.
Instances6Verbalize
Verbalize CohesionDefined in Agda-2.7.0.1 · Agda.TypeChecking.ErrorsVerbalize HidingDefined in Agda-2.7.0.1 · Agda.TypeChecking.ErrorsVerbalize ModalityDefined in Agda-2.7.0.1 · Agda.TypeChecking.ErrorsVerbalize QuantityDefined in Agda-2.7.0.1 · Agda.TypeChecking.ErrorsVerbalize RelevanceDefined in Agda-2.7.0.1 · Agda.TypeChecking.ErrorsVerbalize a => Verbalize (Indefinite a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Errors