ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Options.Errors

Provide names for the errors Agda throws.Options/Er

Contents

Printing error names
Print error messages

Synopsis

data CannotQuoteTerm
data DataRecOrFun_
data ErasedDatatypeReason
data NotAllowedInDotPatterns
data NotAValidLetBinding
data NotAValidLetExpression
data ErrorName
data DeclarationException_
data GHCBackendError_
data JSBackendError_
data InteractionError_
data NegativeUnification_
data NotAHaskellType_
data SplitError_
data CannotQuote_
data ExecError_
data UnquoteError_
value defaultErrorNameString
value erasedDatatypeReasonString
value errorNameString
value constructorOrPatternSynonymNameString
value dataRecOrFunString
value declarationExceptionNameString
value ghcBackendErrorNameString
value jsBackendErrorNameString
value interactionErrorNameString
value negativeUnificationErrorNameString
value notAHaskellTypeErrorNameString
value notAValidLetBindingString
value notAValidLetExpressionString
value notAllowedInDotPatternsString
value splitErrorNameString
value cannotQuoteNameString
value cannotQuoteTermNameString
value execErrorNameString
value unquoteErrorNameString
value helpErrors
value verbalizeNotAValidLetBinding
value verbalizeNotAValidLetExpression

PackageAgda-2.8.0.2
Exports39
LanguageHaskell2010
LicenceMIT
SourceErrors.hs

datadata CannotQuoteTerm

Source#

Extra information for error CannotQuoteTerm.

CannotQuoteTermHidden CannotQuoteTermNothing

Instances6Bounded, Enum, Show, Generic, NFData, Rep

Bounded CannotQuoteTermDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum CannotQuoteTermDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show CannotQuoteTermDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic CannotQuoteTermDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
NFData CannotQuoteTermDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep CannotQuoteTerm = D1 ('MetaData "CannotQuoteTerm" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "CannotQuoteTermHidden" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotQuoteTermNothing" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata DataRecOrFun_

Source#

What kind of declaration?

Constructors

DataName_
Name of a data type.
RecName_
Name of a record type.
FunName_
Name of a function.

Instances5Bounded, Enum, Show, Generic, Rep

Bounded DataRecOrFun_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum DataRecOrFun_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show DataRecOrFun_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic DataRecOrFun_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep DataRecOrFun_ = D1 ('MetaData "DataRecOrFun_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "DataName_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "RecName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FunName_" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata ErasedDatatypeReason

Source#

The reason for an ErasedDatatype error.

Constructors

SeveralConstructors
There are several constructors.
NoErasedMatches
The flag --erased-matches is not used.
NoK
The K rule is not activated.

Instances6Bounded, Enum, Show, Generic, NFData, Rep

Bounded ErasedDatatypeReasonDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum ErasedDatatypeReasonDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show ErasedDatatypeReasonDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic ErasedDatatypeReasonDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
NFData ErasedDatatypeReasonDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep ErasedDatatypeReason = D1 ('MetaData "ErasedDatatypeReason" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "SeveralConstructors" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NoErasedMatches" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoK" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata NotAllowedInDotPatterns

Source#

Things not allowed in dot patterns.

LetExpressions PatternLambdas

Instances6Bounded, Enum, Show, Generic, NFData, Rep

Bounded NotAllowedInDotPatternsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum NotAllowedInDotPatternsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show NotAllowedInDotPatternsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic NotAllowedInDotPatternsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
NFData NotAllowedInDotPatternsDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep NotAllowedInDotPatterns = D1 ('MetaData "NotAllowedInDotPatterns" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "LetExpressions" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PatternLambdas" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata NotAValidLetBinding

Source#

Reasons for error NotAValidLetBinding.

MissingRHS NotAValidLetPattern WhereClausesNotAllowed

Instances6Bounded, Enum, Show, Generic, NFData, Rep

Bounded NotAValidLetBindingDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum NotAValidLetBindingDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show NotAValidLetBindingDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic NotAValidLetBindingDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
NFData NotAValidLetBindingDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep NotAValidLetBinding = D1 ('MetaData "NotAValidLetBinding" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "MissingRHS" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotAValidLetPattern" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WhereClausesNotAllowed" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata NotAValidLetExpression

Source#

Reasons for error NotAValidLetExpression.

MissingBody

Instances6Bounded, Enum, Show, Generic, NFData, Rep

Bounded NotAValidLetExpressionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum NotAValidLetExpressionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show NotAValidLetExpressionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic NotAValidLetExpressionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
NFData NotAValidLetExpressionDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep NotAValidLetExpression = D1 ('MetaData "NotAValidLetExpression" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "MissingBody" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata ErrorName

Source#

Symbolic name of an Agda error.

Constructors

ExecError_ ExecError_
GHCBackendError_ GHCBackendError_
ImpossibleConstructor_ NegativeUnification_
InteractionError_ InteractionError_
JSBackendError_ JSBackendError_
NicifierError_ DeclarationException_
SplitError_ SplitError_
UnquoteError_ UnquoteError_
CompilationError_
CustomBackendError_
GenericError_
GenericDocError_
InternalError_
LibraryError_
NonFatalErrors_
NotImplemented_
NotSupported_
OptionError_
SyntaxError_
AbsentRHSRequiresAbsurdPattern_
AbstractConstructorNotInScope_
AmbiguousConstructor_
AmbiguousField_
AmbiguousModule_
AmbiguousName_
AmbiguousOverloadedProjection_
AmbiguousParseForApplication_
AmbiguousParseForLHS_
AmbiguousProjection_
AmbiguousTopLevelModuleName_
AsPatternInPatternSynonym_
AttributeKindNotEnabled_
BackendDoesNotSupportOnlyScopeChecking_
BadArgumentsToPatternSynonym_
BothWithAndRHS_
BuiltinInParameterisedModule_
BuiltinMustBeConstructor_
BuiltinMustBeData_
BuiltinMustBeDef_
BuiltinMustBeFunction_
BuiltinMustBePostulate_
CannotApply_
CannotEliminateWithPattern_
CannotEliminateWithProjection_
CannotGenerateHCompClause_
CannotGenerateTransportClause_
CannotQuote_ CannotQuote_
CannotQuoteTerm_ CannotQuoteTerm
CannotResolveAmbiguousPatternSynonym_
CannotRewriteByNonEquation_
CannotSolveSizeConstraints_
CantResolveOverloadedConstructorsTargetingSameDatatype_
ClashingDefinition_
ClashingModule_
ComatchingDisabledForRecord_
ConstructorDoesNotTargetGivenType_
ConstructorPatternInWrongDatatype_
ContradictorySizeConstraint_
CopatternHeadNotProjection_
CubicalCompilationNotSupported_
CubicalNotErasure_
CubicalPrimitiveNotFullyApplied_
CyclicModuleDependency_
DatatypeIndexPolarity_
DeBruijnIndexOutOfScope_
DeclarationsAfterTopLevelModule_
DefinitionInDifferentModule_
DefinitionIsErased_
DefinitionIsIrrelevant_
DoNotationError_
DoesNotMentionTicks_
DotPatternInPatternSynonym_
DuplicateBuiltinBinding_
DuplicateConstructors_
DuplicateFields_
DuplicateImports_
DuplicateOverlapPragma_
DuplicatePrimitiveBinding_
EmptyTypeOfSizes_
ExpectedBindingForParameter_
ExpectedIntervalLiteral_
FieldOutsideRecord_
FaceConstraintDisjunction_
FaceConstraintUnsatisfiable_
FileNotFound_
ForcedConstructorNotInstantiated_
FunctionTypeInSizeUniv_
GeneralizeCyclicDependency_
GeneralizeNotSupportedHere_
GeneralizedVarInLetOpenedModule_
ModuleNameHashCollision_
HidingMismatch_
IdiomBracketError_
InvalidBuiltin_
InvalidDottedExpression_
IllTypedPatternAfterWithAbstraction_
IllegalDeclarationBeforeTopLevelModule_
IllegalDeclarationInDataDefinition_
IllegalHidingInPostfixProjection_
IllegalInstanceVariableInPatternSynonym_
IllegalLetInTelescope_
IllegalPatternInTelescope_
IllformedProjectionPatternAbstract_
IllformedProjectionPatternConcrete_
IncorrectTypeForRewriteRelation_
InstanceNoCandidate_
InstanceSearchDepthExhausted_
InvalidFileName_
InvalidModalTelescopeUse_
InvalidPattern_
InvalidProjectionParameter_
InvalidPun_ ConstructorOrPatternSynonym
InvalidTypeSort_
LambdaIsErased_
LibTooFarDown_
LiteralTooBig_
MacroResultTypeMismatch_
MetaCannotDependOn_
MetaErasedSolution_
MetaIrrelevantSolution_
MismatchedProjectionsError_
MissingTypeSignature_ DataRecOrFun_
ModuleArityMismatch_
ModuleDefinedInOtherFile_
ModuleNameDoesntMatchFileName_
ModuleNameUnexpected_
MultipleFixityDecls_
MultiplePolarityPragmas_
ExplicitPolarityVsPragma_
ConstructorNameOfNonRecord_
NamedWhereModuleInRefinedContext_
NeedOptionAllowExec_
NeedOptionCopatterns_
NeedOptionCubical_
NeedOptionPatternMatching_
NeedOptionProp_
NeedOptionRewriting_
NeedOptionSizedTypes_
NeedOptionTwoLevel_
NeedOptionUniversePolymorphism_
NegativeLiteralInPattern_
NoBindingForBuiltin_
NoBindingForPrimitive_
NoKnownRecordWithSuchFields_
NoParameterOfName_
NoParseForApplication_
NoParseForLHS_
NoSuchBuiltinName_
NoSuchModule_
NoSuchPrimitiveFunction_
NotAValidLetBinding_ (Maybe NotAValidLetBinding)
NotAValidLetExpression_ NotAValidLetExpression
NotAllowedInDotPatterns_ NotAllowedInDotPatterns
NotAnExpression_
NotInScope_
NotLeqSort_
NotValidBeforeField_
OverlappingProjects_
PathAbstractionFailed_
PatternInPathLambda_
PatternInSystem_
PatternSynonymArgumentShadows_ ConstructorOrPatternSynonym
PostulatedSizeInModule_
PrivateRecordField_
ProjectionIsIrrelevant_
QualifiedLocalModule_
QuantityMismatch_
RecordIsErased_
RecursiveRecordNeedsInductivity_
ReferencesFutureVariables_
RelevanceMismatch_
RepeatedNamesInImportDirective_
RepeatedVariablesInPattern_
ShadowedModule_
ShouldBeASort_
ShouldBeEmpty_
ShouldBePath_
ShouldBePi_
ShouldBeRecordPattern_
ShouldBeRecordType_
ShouldEndInApplicationOfTheDatatype_
SolvedButOpenHoles_
SortCannotDependOnItsIndex_
SortDoesNotAdmitDataDefinitions_
SortOfSplitVarError_
SplitInProp_
SplitOnAbstract_
SplitOnCoinductive_
SplitOnIrrelevant_
SplitOnNonEtaRecord_
SplitOnNonVariable_
SplitOnPartial_
SplitOnUnchecked_
SplitOnUnusableCohesion_
SplitOnUnusablePolarity_
TacticAttributeNotAllowed_
TooFewArgumentsToPatternSynonym_
TooFewPatternsInWithClause_
TooManyFields_
TooManyPatternsInWithClause_
TriedToCopyConstrainedPrim_
InvalidInstanceHeadType_
UnboundVariablesInPatternSynonym_
UnequalCohesion_
UnequalFiniteness_
UnequalHiding_
UnequalLevel_
UnequalQuantity_
UnequalRelevance_
UnequalPolarity_
UnequalSorts_
UnequalTerms_
UnexpectedModalityAnnotationInParameter_
UnexpectedParameter_
UnexpectedTypeSignatureForParameter_
UnexpectedWithPatterns_
UnknownBackend_
UnusableAtModality_
UnusedVariableInPatternSynonym_
VariableIsErased_
VariableIsIrrelevant_
VariableIsOfUnusableCohesion_
VariableIsOfUnusablePolarity_
WithClausePatternMismatch_
WithOnFreeVariable_
WrongAnnotationInLambda_
WrongArgInfoForPrimitive_
WrongCohesionInLambda_
WrongPolarityInLambda_
WrongHidingInApplication_
WrongHidingInLHS_
WrongHidingInLambda_
WrongHidingInProjection_
WrongIrrelevanceInLambda_
WrongNamedArgument_
WrongNumberOfConstructorArguments_
WrongQuantityInLambda_
WrongSharpArity_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded ErrorNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum ErrorNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show ErrorNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic ErrorNameDefined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep ErrorName = D1 ('MetaData "ErrorName" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((((((C1 ('MetaCons "ExecError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExecError_)) :+: (C1 ('MetaCons "GHCBackendError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GHCBackendError_)) :+: C1 ('MetaCons "ImpossibleConstructor_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NegativeUnification_)))) :+: ((C1 ('MetaCons "InteractionError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionError_)) :+: C1 ('MetaCons "JSBackendError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 JSBackendError_))) :+: (C1 ('MetaCons "NicifierError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclarationException_)) :+: C1 ('MetaCons "SplitError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitError_))))) :+: ((C1 ('MetaCons "UnquoteError_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnquoteError_)) :+: (C1 ('MetaCons "CompilationError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CustomBackendError_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "GenericError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GenericDocError_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InternalError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "LibraryError_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "NonFatalErrors_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotImplemented_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotSupported_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "OptionError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SyntaxError_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "AbsentRHSRequiresAbsurdPattern_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AbstractConstructorNotInScope_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "AmbiguousConstructor_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AmbiguousField_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "AmbiguousModule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AmbiguousName_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "AmbiguousOverloadedProjection_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AmbiguousParseForApplication_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "AmbiguousParseForLHS_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AmbiguousProjection_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "AmbiguousTopLevelModuleName_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "AsPatternInPatternSynonym_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AttributeKindNotEnabled_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "BackendDoesNotSupportOnlyScopeChecking_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BadArgumentsToPatternSynonym_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "BothWithAndRHS_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BuiltinInParameterisedModule_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "BuiltinMustBeConstructor_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BuiltinMustBeData_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "BuiltinMustBeDef_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BuiltinMustBeFunction_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "BuiltinMustBePostulate_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotApply_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "CannotEliminateWithPattern_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotEliminateWithProjection_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "CannotGenerateHCompClause_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CannotGenerateTransportClause_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotQuote_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuote_)))) :+: ((C1 ('MetaCons "CannotQuoteTerm_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CannotQuoteTerm)) :+: C1 ('MetaCons "CannotResolveAmbiguousPatternSynonym_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "CannotRewriteByNonEquation_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotSolveSizeConstraints_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "CantResolveOverloadedConstructorsTargetingSameDatatype_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ClashingDefinition_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ClashingModule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ComatchingDisabledForRecord_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ConstructorDoesNotTargetGivenType_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConstructorPatternInWrongDatatype_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ContradictorySizeConstraint_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CopatternHeadNotProjection_" 'PrefixI 'False) U1)))))) :+: (((((C1 ('MetaCons "CubicalCompilationNotSupported_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CubicalNotErasure_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CubicalPrimitiveNotFullyApplied_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "CyclicModuleDependency_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DatatypeIndexPolarity_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DeBruijnIndexOutOfScope_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DeclarationsAfterTopLevelModule_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "DefinitionInDifferentModule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DefinitionIsErased_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DefinitionIsIrrelevant_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DoNotationError_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "DoesNotMentionTicks_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DotPatternInPatternSynonym_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DuplicateBuiltinBinding_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateConstructors_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "DuplicateFields_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "DuplicateImports_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateOverlapPragma_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "DuplicatePrimitiveBinding_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "EmptyTypeOfSizes_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ExpectedBindingForParameter_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ExpectedIntervalLiteral_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "FieldOutsideRecord_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FaceConstraintDisjunction_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "FaceConstraintUnsatisfiable_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FileNotFound_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ForcedConstructorNotInstantiated_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "FunctionTypeInSizeUniv_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "GeneralizeCyclicDependency_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "GeneralizeNotSupportedHere_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "GeneralizedVarInLetOpenedModule_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ModuleNameHashCollision_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "HidingMismatch_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "IdiomBracketError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidBuiltin_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InvalidDottedExpression_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllTypedPatternAfterWithAbstraction_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "IllegalDeclarationBeforeTopLevelModule_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllegalDeclarationInDataDefinition_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "IllegalHidingInPostfixProjection_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllegalInstanceVariableInPatternSynonym_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "IllegalLetInTelescope_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllegalPatternInTelescope_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "IllformedProjectionPatternAbstract_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IllformedProjectionPatternConcrete_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "IncorrectTypeForRewriteRelation_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "InstanceNoCandidate_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InstanceSearchDepthExhausted_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "InvalidFileName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidModalTelescopeUse_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "InvalidPattern_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidProjectionParameter_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "InvalidPun_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "InvalidTypeSort_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "LambdaIsErased_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "LibTooFarDown_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "LiteralTooBig_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MacroResultTypeMismatch_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "MetaCannotDependOn_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MetaErasedSolution_" 'PrefixI 'False) U1))))))) :+: ((((((C1 ('MetaCons "MetaIrrelevantSolution_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MismatchedProjectionsError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MissingTypeSignature_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataRecOrFun_)))) :+: ((C1 ('MetaCons "ModuleArityMismatch_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ModuleDefinedInOtherFile_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ModuleNameDoesntMatchFileName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ModuleNameUnexpected_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "MultipleFixityDecls_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MultiplePolarityPragmas_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ExplicitPolarityVsPragma_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ConstructorNameOfNonRecord_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NamedWhereModuleInRefinedContext_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NeedOptionAllowExec_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NeedOptionCopatterns_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "NeedOptionCubical_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NeedOptionPatternMatching_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NeedOptionProp_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "NeedOptionRewriting_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NeedOptionSizedTypes_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NeedOptionTwoLevel_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NeedOptionUniversePolymorphism_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "NegativeLiteralInPattern_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoBindingForBuiltin_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NoBindingForPrimitive_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoKnownRecordWithSuchFields_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "NoParameterOfName_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoParseForApplication_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NoParseForLHS_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoSuchBuiltinName_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "NoSuchModule_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NoSuchPrimitiveFunction_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotAValidLetBinding_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NotAValidLetBinding))))) :+: ((C1 ('MetaCons "NotAValidLetExpression_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAValidLetExpression)) :+: C1 ('MetaCons "NotAllowedInDotPatterns_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAllowedInDotPatterns))) :+: (C1 ('MetaCons "NotAnExpression_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotInScope_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "NotLeqSort_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotValidBeforeField_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "OverlappingProjects_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PathAbstractionFailed_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "PatternInPathLambda_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "PatternInSystem_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "PatternSynonymArgumentShadows_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstructorOrPatternSynonym)) :+: C1 ('MetaCons "PostulatedSizeInModule_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "PrivateRecordField_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ProjectionIsIrrelevant_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "QualifiedLocalModule_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "QuantityMismatch_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RecordIsErased_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RecursiveRecordNeedsInductivity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ReferencesFutureVariables_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "RelevanceMismatch_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RepeatedNamesInImportDirective_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "RepeatedVariablesInPattern_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ShadowedModule_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ShouldBeASort_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ShouldBeEmpty_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ShouldBePath_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ShouldBePi_" 'PrefixI 'False) U1)))))) :+: (((((C1 ('MetaCons "ShouldBeRecordPattern_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ShouldBeRecordType_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ShouldEndInApplicationOfTheDatatype_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "SolvedButOpenHoles_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SortCannotDependOnItsIndex_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SortDoesNotAdmitDataDefinitions_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SortOfSplitVarError_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "SplitInProp_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SplitOnAbstract_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SplitOnCoinductive_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SplitOnIrrelevant_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "SplitOnNonEtaRecord_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SplitOnNonVariable_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "SplitOnPartial_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "SplitOnUnchecked_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "SplitOnUnusableCohesion_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "SplitOnUnusablePolarity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "TacticAttributeNotAllowed_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "TooFewArgumentsToPatternSynonym_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "TooFewPatternsInWithClause_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "TooManyFields_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "TooManyPatternsInWithClause_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "TriedToCopyConstrainedPrim_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidInstanceHeadType_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnboundVariablesInPatternSynonym_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnequalCohesion_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "UnequalFiniteness_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnequalHiding_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnequalLevel_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnequalQuantity_" 'PrefixI 'False) U1))))) :+: ((((C1 ('MetaCons "UnequalRelevance_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "UnequalPolarity_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnequalSorts_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "UnequalTerms_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnexpectedModalityAnnotationInParameter_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnexpectedParameter_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnexpectedTypeSignatureForParameter_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "UnexpectedWithPatterns_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnknownBackend_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "UnusableAtModality_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnusedVariableInPatternSynonym_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "VariableIsErased_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "VariableIsIrrelevant_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "VariableIsOfUnusableCohesion_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "VariableIsOfUnusablePolarity_" 'PrefixI 'False) U1)))) :+: (((C1 ('MetaCons "WithClausePatternMismatch_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "WithOnFreeVariable_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongAnnotationInLambda_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "WrongArgInfoForPrimitive_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongCohesionInLambda_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "WrongPolarityInLambda_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongHidingInApplication_" 'PrefixI 'False) U1))) :+: (((C1 ('MetaCons "WrongHidingInLHS_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongHidingInLambda_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "WrongHidingInProjection_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongIrrelevanceInLambda_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "WrongNamedArgument_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongNumberOfConstructorArguments_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "WrongQuantityInLambda_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongSharpArity_" 'PrefixI 'False) U1))))))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata DeclarationException_

Source#

Nicifier errors.

AmbiguousConstructorN_AmbiguousFunClauses_BadMacroDef_DisallowedInterleavedMutual_DuplicateAnonDeclaration_DuplicateDefinition_InvalidMeasureMutual_MissingWithClauses_MultipleEllipses_OpaqueInMutual_UnfoldingOutsideOpaque_UnquoteDefRequiresSignature_WrongContentBlock_WrongDefinition_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded DeclarationException_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum DeclarationException_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show DeclarationException_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic DeclarationException_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep DeclarationException_ = D1 ('MetaData "DeclarationException_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "AmbiguousConstructorN_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "AmbiguousFunClauses_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BadMacroDef_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "DisallowedInterleavedMutual_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DuplicateAnonDeclaration_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DuplicateDefinition_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InvalidMeasureMutual_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "MissingWithClauses_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MultipleEllipses_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OpaqueInMutual_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "UnfoldingOutsideOpaque_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnquoteDefRequiresSignature_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "WrongContentBlock_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongDefinition_" 'PrefixI 'False) U1))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata GHCBackendError_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded GHCBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum GHCBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show GHCBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic GHCBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep GHCBackendError_ = D1 ('MetaData "GHCBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ConstructorCountMismatch_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotAHaskellType_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotAHaskellType_)) :+: C1 ('MetaCons "WrongTypeOfMain_" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata JSBackendError_

BadCompilePragma_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded JSBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum JSBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show JSBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic JSBackendError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep JSBackendError_ = D1 ('MetaData "JSBackendError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "BadCompilePragma_" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata InteractionError_

CannotGive_CannotRefine_CaseSplitError_ExpectedIdentifier_ExpectedApplication_NoActionForInteractionPoint_NoSuchInteractionPoint_UnexpectedWhere_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded InteractionError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum InteractionError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show InteractionError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic InteractionError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep InteractionError_ = D1 ('MetaData "InteractionError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "CannotGive_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotRefine_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "CaseSplitError_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ExpectedIdentifier_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ExpectedApplication_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoActionForInteractionPoint_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "NoSuchInteractionPoint_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnexpectedWhere_" 'PrefixI 'False) U1)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata NegativeUnification_

UnifyConflict_UnifyCycle_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded NegativeUnification_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum NegativeUnification_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show NegativeUnification_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic NegativeUnification_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep NegativeUnification_ = D1 ('MetaData "NegativeUnification_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "UnifyConflict_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnifyCycle_" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata NotAHaskellType_

BadDontCare_BadLambda_BadMeta_NoPragmaFor_NotCompiled_WrongPragmaFor_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded NotAHaskellType_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum NotAHaskellType_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show NotAHaskellType_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic NotAHaskellType_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep NotAHaskellType_ = D1 ('MetaData "NotAHaskellType_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) ((C1 ('MetaCons "BadDontCare_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "BadLambda_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BadMeta_" 'PrefixI 'False) U1)) :+: (C1 ('MetaCons "NoPragmaFor_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotCompiled_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "WrongPragmaFor_" 'PrefixI 'False) U1)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata SplitError_

Constructors

ErasedDatatype_ ErasedDatatypeReason
GenericSplitError_
BlockedType_
CannotCreateMissingClause_
CoinductiveDatatype_
CosplitCatchall_
CosplitNoRecordType_
CosplitNoTarget_
NotADatatype_
UnificationStuck_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded SplitError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum SplitError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show SplitError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic SplitError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep SplitError_ = D1 ('MetaData "SplitError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "ErasedDatatype_" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ErasedDatatypeReason)) :+: C1 ('MetaCons "GenericSplitError_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "BlockedType_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CannotCreateMissingClause_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CoinductiveDatatype_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "CosplitCatchall_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CosplitNoRecordType_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "CosplitNoTarget_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NotADatatype_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnificationStuck_" 'PrefixI 'False) U1))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata CannotQuote_

CannotQuoteAmbiguous_CannotQuoteExpression_CannotQuoteHidden_CannotQuoteNothing_CannotQuotePattern_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded CannotQuote_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum CannotQuote_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show CannotQuote_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic CannotQuote_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep CannotQuote_ = D1 ('MetaData "CannotQuote_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) ((C1 ('MetaCons "CannotQuoteAmbiguous_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotQuoteExpression_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "CannotQuoteHidden_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CannotQuoteNothing_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CannotQuotePattern_" 'PrefixI 'False) U1)))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata ExecError_

ExeNotTrusted_ExeNotFound_ExeNotExecutable_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded ExecError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum ExecError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show ExecError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic ExecError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep ExecError_ = D1 ('MetaData "ExecError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (C1 ('MetaCons "ExeNotTrusted_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ExeNotFound_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ExeNotExecutable_" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata UnquoteError_

BlockedOnMeta_CannotDeclareHiddenFunction_CommitAfterDef_ConInsteadOfDef_DefineDataNotData_DefInsteadOfCon_MissingDeclaration_MissingDefinition_NakedUnquote_NonCanonical_PatLamWithoutClauses_StaleMeta_TooManyParameters_UnboundName_

Instances5Bounded, Enum, Show, Generic, Rep

Bounded UnquoteError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Enum UnquoteError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Show UnquoteError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
Generic UnquoteError_Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors
type Rep UnquoteError_ = D1 ('MetaData "UnquoteError_" "Agda.Interaction.Options.Errors" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" 'False) (((C1 ('MetaCons "BlockedOnMeta_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "CannotDeclareHiddenFunction_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CommitAfterDef_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "ConInsteadOfDef_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "DefineDataNotData_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "DefInsteadOfCon_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MissingDeclaration_" 'PrefixI 'False) U1))) :+: ((C1 ('MetaCons "MissingDefinition_" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "NakedUnquote_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NonCanonical_" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "PatLamWithoutClauses_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "StaleMeta_" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "TooManyParameters_" 'PrefixI 'False) U1 :+: C1 ('MetaCons "UnboundName_" 'PrefixI 'False) U1))))Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

Printing error names

valuedefaultErrorNameString :: Show a => a -> String

valueerasedDatatypeReasonString :: ErasedDatatypeReason -> String

valueerrorNameString :: ErrorName -> String

valueconstructorOrPatternSynonymNameString

:: ConstructorOrPatternSynonym
-> String

valuedataRecOrFunString :: DataRecOrFun_ -> String

valuedeclarationExceptionNameString :: DeclarationException_ -> String

valueghcBackendErrorNameString :: GHCBackendError_ -> String

valuejsBackendErrorNameString :: JSBackendError_ -> String

valueinteractionErrorNameString :: InteractionError_ -> String

valuenegativeUnificationErrorNameString :: NegativeUnification_ -> String

valuenotAHaskellTypeErrorNameString :: NotAHaskellType_ -> String

valuenotAValidLetBindingString :: NotAValidLetBinding -> String

valuenotAValidLetExpressionString :: NotAValidLetExpression -> String

valuenotAllowedInDotPatternsString :: NotAllowedInDotPatterns -> String

valuesplitErrorNameString :: SplitError_ -> String

valuecannotQuoteNameString :: CannotQuote_ -> String

valuecannotQuoteTermNameString :: CannotQuoteTerm -> String

valueexecErrorNameString :: ExecError_ -> String

valueunquoteErrorNameString :: UnquoteError_ -> String

valuehelpErrors :: String

Source#

Print list of errors.

Print error messages

valueverbalizeNotAValidLetBinding :: NotAValidLetBinding -> String

valueverbalizeNotAValidLetExpression :: NotAValidLetExpression -> String

Orphan instances

2 instances

(Bounded a, Enum a) => Bounded (Maybe a)
(Bounded a, Enum a) => Enum (Maybe a)