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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Errors

Synopsis

Documentation

prettyError :: MonadTCM tcm => TCErr -> tcm String

data Warnings

Warnings.

Invariant: The fields are never empty at the same time.

Constructors

Warnings 

Fields

unsolvedMetaVariables :: [Range]

Meta-variable problems are reported as type errors unless optAllowUnsolved is True.

unsolvedConstraints :: Constraints

Same as unsolvedMetaVariables.

warningsToError :: Warnings -> TCM a

Turns warnings into an error. Even if several errors are possible only one is raised.