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

Safe Haskell | None

Agda.TypeChecking.Errors

Synopsis

- prettyError :: TCErr -> TCM String
- class PrettyTCM a where
  - prettyTCM :: a -> TCM Doc
- tcErrString :: TCErr -> String
- data Warnings = Warnings {
  - terminationProblems :: [TerminationError]
  - unsolvedMetaVariables :: [Range]
  - unsolvedConstraints :: Constraints
  }
- warningsToError :: Warnings -> TypeError

# Documentation

prettyError :: TCErr -> TCM String

class PrettyTCM a where

Methods

prettyTCM :: a -> TCM Doc

Instances

PrettyTCM Nat |
PrettyTCM Relevance |
PrettyTCM Name |
PrettyTCM ModuleName |
PrettyTCM QName |
PrettyTCM Name |
PrettyTCM Literal |
PrettyTCM ClauseBody |
PrettyTCM MetaId |
PrettyTCM Level |
PrettyTCM Sort |
PrettyTCM Telescope |
PrettyTCM Type |
PrettyTCM Elim |
PrettyTCM Term |
PrettyTCM Expr |
PrettyTCM TCErr |
PrettyTCM TypeError |
PrettyTCM Context |
PrettyTCM Call |
PrettyTCM Occurrence |
PrettyTCM DisplayTerm |
PrettyTCM Comparison |
PrettyTCM Constraint |
PrettyTCM ProblemConstraint |
PrettyTCM NamedClause |
PrettyTCM PrettyContext |
PrettyTCM Node |
PrettyTCM OccursWhere |
PrettyTCM AsBinding |
PrettyTCM DotPatternInst |
PrettyTCM SplitError |
PrettyTCM DeBruijnPat |
PrettyTCM a => PrettyTCM [a] |
(ReifyWhen a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) |
PrettyTCM a => PrettyTCM (Blocked a) |
PrettyTCM a => PrettyTCM (Closure a) |
PrettyTCM a => PrettyTCM (HomHet a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) |
PrettyTCM n => PrettyTCM (n, Occurrence) |
PrettyTCM n => PrettyTCM (n, Edge) |
(PrettyTCM n, PrettyTCM (n, e)) => PrettyTCM (Graph n e) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) |

tcErrString :: TCErr -> String

data Warnings

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 -> TypeError

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