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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Errors

Synopsis

Documentation

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

class PrettyTCM a where Source

Methods

prettyTCM :: a -> TCM Doc Source

Instances

PrettyTCM Bool 
PrettyTCM Permutation 
PrettyTCM Range 
PrettyTCM Interval 
PrettyTCM Position 
PrettyTCM Nat 
PrettyTCM Relevance 
PrettyTCM Name 
PrettyTCM ModuleName 
PrettyTCM QName 
PrettyTCM Name 
PrettyTCM Literal 
PrettyTCM Expr 
PrettyTCM Pattern 
PrettyTCM ClauseBody 
PrettyTCM MetaId 
PrettyTCM Level 
PrettyTCM Sort 
PrettyTCM Telescope 
PrettyTCM Type 
PrettyTCM Elim 
PrettyTCM Term 
PrettyTCM ConHead 
PrettyTCM TCErr 
PrettyTCM TypeError 
PrettyTCM SplitError 
PrettyTCM CallInfo 
PrettyTCM Context 
PrettyTCM Call 
PrettyTCM Occurrence 
PrettyTCM DisplayTerm 
PrettyTCM TypeCheckingProblem 
PrettyTCM Comparison 
PrettyTCM Constraint 
PrettyTCM ProblemConstraint 
PrettyTCM NamedClause 
PrettyTCM PrettyContext 
PrettyTCM AsBinding 
PrettyTCM DotPatternInst 
PrettyTCM DeBruijnPat 
PrettyTCM Node 
PrettyTCM OccursWhere 
PrettyTCM HypSizeConstraint 
PrettyTCM SizeConstraint

Assumes we are in the right context.

PrettyTCM SizeMeta 
PrettyTCM a => PrettyTCM [a] 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) 
PrettyTCM a => PrettyTCM (Blocked a) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) 
PrettyTCM a => PrettyTCM (MaybeReduced a) 
PrettyTCM a => PrettyTCM (Closure a) 
PrettyTCM a => PrettyTCM (HomHet a) 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) 
(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) 
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) 
PrettyTCM n => PrettyTCM (WithNode n Occurrence) 
PrettyTCM n => PrettyTCM (WithNode n Edge) 

tcErrString :: TCErr -> String Source

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

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