ModuleAgda-2.8.0.2Haskell2010

Agda.Interaction.Options.Errors

Provide names for the errors Agda throws.Options/Er

17 types
22 values

PackageAgda-2.8.0.2
Exports39
LanguageHaskell2010
LicenceMIT
SourceErrors.hs

datadata CannotQuoteTerm

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-3KZoCGOoan2Kayji4DU37s" '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_

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-3KZoCGOoan2Kayji4DU37s" '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

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-3KZoCGOoan2Kayji4DU37s" '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

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-3KZoCGOoan2Kayji4DU37s" '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

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-3KZoCGOoan2Kayji4DU37s" '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

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-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "MissingBody" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Interaction.Options.Errors

datadata ErrorName

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-3KZoCGOoan2Kayji4DU37s" '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_

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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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-3KZoCGOoan2Kayji4DU37s" '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

20 declarations

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

Print list of errors.

Print error messages

2 declarations

valueverbalizeNotAValidLetBinding :: NotAValidLetBinding -> String

valueverbalizeNotAValidLetExpression :: NotAValidLetExpression -> String

Orphan instances

2 instances

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