Agda.TypeChecking.Errors

Documentation

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

tcErrString :: TCErr -> 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.

Orphan instances

PrettyTCM TCErr

Methods

prettyTCM :: TCErr -> TCM Doc

PrettyTCM TypeError

Methods

prettyTCM :: TypeError -> TCM Doc

PrettyTCM SplitError

Methods

prettyTCM :: SplitError -> TCM Doc

PrettyTCM CallInfo

Methods

prettyTCM :: CallInfo -> TCM Doc

PrettyTCM Call

Methods

prettyTCM :: Call -> TCM Doc