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

Safe HaskellNone

Agda.TypeChecking.Errors

Synopsis

Documentation

data Warnings Source

Warnings.

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

Constructors

Warnings 

Fields

terminationProblems :: [TerminationError]

Termination checking problems are not reported if optTerminationCheck is False.

unsolvedMetaVariables :: [Range]

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

unsolvedConstraints :: Constraints

Same as unsolvedMetaVariables.

warningsToError :: Warnings -> TypeErrorSource

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