Index

Symbols

+RTS command line option --allow-exec command line option --allow-incomplete-matches command line option --allow-unsolved-metas command line option --auto-inline command line option --backtracking-instance-search command line option --caching command line option --call-by-name command line option --cohesion command line option --color command line option --colour command line option --compile command line option --compile-dir command line option --confluence-check command line option --copatterns command line option --count-clusters command line option --css command line option --cubical command line option --cubical-compatible command line option --cumulativity command line option --dependency-graph command line option --dependency-graph-include command line option --double-check command line option --erase-record-parameters command line option --erased-cubical command line option --erased-matches command line option --erasure command line option --eta-equality command line option --exact-split command line option --experimental-irrelevance command line option --fast-reduce command line option --flat-split command line option --forced-argument-recursion command line option --forcing command line option --ghc command line option --ghc-dont-call-ghc command line option --ghc-flag command line option --ghc-strict command line option --ghc-strict-data command line option --guarded command line option --guardedness command line option --help command line option --hidden-argument-puns command line option --highlight-occurrences command line option --html command line option --html-dir command line option --html-highlight command line option --ignore-all-interfaces command line option --ignore-interfaces command line option --import-sorts command line option --include-path command line option --infer-absurd-clauses command line option --injective-type-constructors command line option --instance-search-depth command line option --interaction command line option --interaction-exit-on-error command line option --interaction-json command line option --interactive command line option --inversion-max-depth command line option --irrelevant-projections command line option --js command line option --js-amd command line option --js-cjs command line option --js-es6 command line option --js-minify command line option --js-optimize command line option --js-verify command line option --keep-covering-clauses command line option --keep-pattern-variables command line option --large-indices command line option --latex command line option --latex-dir command line option --level-universe command line option --library command line option --library-file command line option --load-primitives command line option --local-confluence-check command line option --local-interfaces command line option --lossy-unification command line option, [1] --main command line option --no-allow-exec command line option --no-allow-incomplete-matches command line option --no-allow-unsolved-metas command line option --no-auto-inline command line option --no-backtracking-instance-search command line option --no-caching command line option --no-call-by-name command line option --no-cohesion command line option --no-confluence-check command line option --no-copatterns command line option --no-count-clusters command line option --no-cumulativity command line option --no-default-libraries command line option

--no-double-check command line option --no-erase-record-parameters command line option --no-erased-matches command line option --no-erasure command line option --no-eta-equality command line option --no-exact-split command line option --no-experimental-irrelevance command line option --no-fast-reduce command line option --no-flat-split command line option --no-forced-argument-recursion command line option --no-forcing command line option --no-guarded command line option --no-guardedness command line option --no-hidden-argument-puns command line option --no-import-sorts command line option --no-infer-absurd-clauses command line option --no-injective-type-constructors command line option --no-irrelevant-projections command line option --no-keep-covering-clauses command line option --no-keep-pattern-variables command line option --no-large-indices command line option --no-level-universe command line option --no-libraries command line option --no-load-primitives command line option --no-lossy-unification command line option, [1] --no-main command line option --no-omega-in-omega command line option --no-pattern-matching command line option --no-positivity-check command line option --no-postfix-projections command line option --no-print-pattern-synonyms command line option --no-projection-like command line option --no-prop command line option --no-qualified-instances command line option --no-require-unique-meta-solutions command line option --no-rewriting command line option --no-save-metas command line option --no-show-identity-substitutions command line option --no-show-implicit command line option --no-show-irrelevant command line option --no-sized-types command line option --no-syntactic-equality command line option --no-termination-check command line option --no-two-level command line option --no-type-in-type command line option --no-unicode command line option --no-universe-polymorphism command line option --numeric-version command line option --omega-in-omega command line option --only-scope-checking command line option --pattern-matching command line option --positivity-check command line option --postfix-projections command line option --print-agda-app-dir command line option --print-agda-data-dir command line option --print-agda-dir command line option --print-pattern-synonyms command line option --profile command line option, [1], [2], [3] --projection-like command line option --prop command line option --qualified-instances command line option --require-unique-meta-solutions command line option --rewriting command line option --safe command line option --save-metas command line option --show-identity-substitutions command line option --show-implicit command line option --show-irrelevant command line option --sized-types command line option --syntactic-equality command line option --termination-check command line option --termination-depth command line option --trace-imports command line option --transliterate command line option --two-level command line option --type-in-type command line option --unicode command line option --universe-polymorphism command line option --verbose command line option --version command line option --vim command line option --warning command line option --with-compiler command line option --with-K command line option --without-K command line option -?[{TOPIC}] command line option -I command line option -i command line option -l command line option -V command line option -v command line option -W command line option

A

AbsurdPatternRequiresAbsentRHS command line option Agda_datadir AGDA_DIR, [1], [2], [3], [4]

all command line option AsPatternShadowsConstructorOrPatternSynonym command line option

B

BuiltinDeclaresIdentifier command line option

C

CantGeneralizeOverSorts command line option ClashesViaRenaming command line option CoinductiveEtaRecord command line option CoInfectiveImport command line option command line option +RTS --allow-exec --allow-incomplete-matches --allow-unsolved-metas --auto-inline --backtracking-instance-search --caching --call-by-name --cohesion --color --colour --compile --compile-dir --confluence-check --copatterns --count-clusters --css --cubical --cubical-compatible --cumulativity --dependency-graph --dependency-graph-include --double-check --erase-record-parameters --erased-cubical --erased-matches --erasure --eta-equality --exact-split --experimental-irrelevance --fast-reduce --flat-split --forced-argument-recursion --forcing --ghc --ghc-dont-call-ghc --ghc-flag --ghc-strict --ghc-strict-data --guarded --guardedness --help --hidden-argument-puns --highlight-occurrences --html --html-dir --html-highlight --ignore-all-interfaces --ignore-interfaces --import-sorts --include-path --infer-absurd-clauses --injective-type-constructors --instance-search-depth --interaction --interaction-exit-on-error --interaction-json --interactive --inversion-max-depth --irrelevant-projections --js --js-amd --js-cjs --js-es6 --js-minify --js-optimize --js-verify --keep-covering-clauses --keep-pattern-variables --large-indices --latex --latex-dir --level-universe --library --library-file --load-primitives --local-confluence-check --local-interfaces --lossy-unification, [1] --main --no-allow-exec --no-allow-incomplete-matches --no-allow-unsolved-metas --no-auto-inline --no-backtracking-instance-search --no-caching --no-call-by-name --no-cohesion --no-confluence-check --no-copatterns --no-count-clusters --no-cumulativity --no-default-libraries --no-double-check --no-erase-record-parameters --no-erased-matches --no-erasure --no-eta-equality --no-exact-split --no-experimental-irrelevance --no-fast-reduce --no-flat-split --no-forced-argument-recursion --no-forcing --no-guarded --no-guardedness --no-hidden-argument-puns --no-import-sorts --no-infer-absurd-clauses --no-injective-type-constructors --no-irrelevant-projections --no-keep-covering-clauses --no-keep-pattern-variables --no-large-indices --no-level-universe --no-libraries --no-load-primitives --no-lossy-unification, [1] --no-main --no-omega-in-omega --no-pattern-matching --no-positivity-check --no-postfix-projections --no-print-pattern-synonyms --no-projection-like --no-prop --no-qualified-instances --no-require-unique-meta-solutions --no-rewriting --no-save-metas --no-show-identity-substitutions --no-show-implicit --no-show-irrelevant --no-sized-types --no-syntactic-equality --no-termination-check --no-two-level --no-type-in-type --no-unicode --no-universe-polymorphism --numeric-version --omega-in-omega --only-scope-checking --pattern-matching --positivity-check --postfix-projections --print-agda-app-dir --print-agda-data-dir --print-agda-dir --print-pattern-synonyms --profile, [1], [2], [3] --projection-like --prop --qualified-instances --require-unique-meta-solutions --rewriting --safe --save-metas --show-identity-substitutions --show-implicit --show-irrelevant --sized-types --syntactic-equality --termination-check --termination-depth --trace-imports --transliterate --two-level --type-in-type --unicode --universe-polymorphism --verbose --version --vim --warning --with-compiler --with-K --without-K -?[{TOPIC}] -I -i -l -V -v -W AbsurdPatternRequiresAbsentRHS all AsPatternShadowsConstructorOrPatternSynonym BuiltinDeclaresIdentifier CantGeneralizeOverSorts ClashesViaRenaming CoinductiveEtaRecord CoInfectiveImport ConflictingPragmaOptions ConfluenceCheckingIncompleteBecauseOfMeta ConfluenceForCubicalNotSupported ConstructorDoesNotFitInData CoverageIssue CoverageNoExactSplit CustomBackendWarning debug debug-parsing debug-serialisation DeprecationWarning DuplicateFields DuplicateInterfaceFiles DuplicateRecordDirective DuplicateRewriteRule DuplicateUsing EmptyAbstract EmptyConstructor EmptyField EmptyGeneralize EmptyInstance EmptyMacro EmptyMutual EmptyPolarityPragma EmptyPostulate EmptyPrimitive EmptyPrivate EmptyRewritePragma EmptyWhere enable-cluster-counting FaceConstraintCannotBeHidden FaceConstraintCannotBeNamed FixingRelevance FixityInRenamingModule HiddenGeneralize ignore IllformedAsClause InfectiveImport InlineNoExactSplit InstanceArgWithExplicitArg InstanceNoOutputTypeName InstanceWithExplicitArg InteractionMetaBoundaries InvalidCatchallPragma InvalidCharacterLiteral InvalidConstructorBlock InvalidCoverageCheckPragma InvalidDisplayForm InvalidNoPositivityCheckPragma InvalidNoUniverseCheckPragma InvalidTerminationCheckPragma InversionDepthReached LibUnknownField MissingDataDeclaration MissingDefinitions MissingTypeSignatureForOpaque ModuleDoesntExport MultipleAttributes NoGuardednessFlag NoMain NotAffectedByOpaque NotAllowedInMutual NotARewriteRule NotInScope NotStrictlyPositive OldBuiltin OpenPublicAbstract OpenPublicPrivate optimise-heavily OptionRenamed OverlappingTokensWarning PatternShadowsConstructor PlentyInHardCompileTimeMode PolarityPragmasButNotPostulates PragmaCompiled PragmaCompileErased PragmaCompileList PragmaCompileMaybe PragmaCompileUnparsable PragmaCompileWrong PragmaCompileWrongName PragmaExpectsDefinedSymbol PragmaExpectsUnambiguousConstructorOrFunction PragmaExpectsUnambiguousProjectionOrFunction PragmaNoTerminationCheck RewriteAmbiguousRules RewriteBeforeFunctionDefinition RewriteBeforeMutualFunctionDefinition RewriteBlockedOnProblems RewriteConstructorParametersNotGeneral RewriteContainsUnsolvedMetaVariables RewriteDoesNotTargetRewriteRelation RewriteHeadSymbolContainsMetas RewriteHeadSymbolIsProjectionLikeFunction RewriteHeadSymbolIsTypeConstructor RewriteLHSNotDefinitionOrConstructor RewriteLHSReduces RewriteMaybeNonConfluent RewriteMissingRule RewriteNonConfluent RewriteRequiresDefinitions RewriteVariablesBoundMoreThanOnce RewriteVariablesNotBoundByLHS SafeFlagEta SafeFlagInjective SafeFlagNoCoverageCheck SafeFlagNonTerminating SafeFlagNoPositivityCheck SafeFlagNoUniverseCheck SafeFlagPolarity SafeFlagPostulate SafeFlagPragma SafeFlagTerminating SafeFlagWithoutKFlagPrimEraseEquality ShadowingInTelescope TerminationIssue TooManyArgumentsToSort TooManyFields UnfoldingWrongName UnfoldTransparentName UnknownFixityInMixfixDecl UnknownNamesInFixityDecl UnknownNamesInPolarityPragmas UnreachableClauses UnsolvedConstraints UnsolvedInteractionMetas UnsolvedMetaVariables UnsupportedAttribute UnsupportedIndexedMatch UselessAbstract UselessHiding UselessInline UselessInstance UselessMacro UselessOpaque UselessPatternDeclarationForRecord UselessPragma UselessPrivate UselessPublic UserWarning warn WarningProblem WithClauseProjectionFixityMismatch WithoutKFlagPrimEraseEquality WrongInstanceDeclaration

ConflictingPragmaOptions command line option ConfluenceCheckingIncompleteBecauseOfMeta command line option ConfluenceForCubicalNotSupported command line option ConstructorDoesNotFitInData command line option CoverageIssue command line option CoverageNoExactSplit command line option CustomBackendWarning command line option

D

debug command line option debug-parsing command line option debug-serialisation command line option DeprecationWarning command line option DuplicateFields command line option

DuplicateInterfaceFiles command line option DuplicateRecordDirective command line option DuplicateRewriteRule command line option DuplicateUsing command line option

E

EmptyAbstract command line option EmptyConstructor command line option EmptyField command line option EmptyGeneralize command line option EmptyInstance command line option EmptyMacro command line option EmptyMutual command line option EmptyPolarityPragma command line option

EmptyPostulate command line option EmptyPrimitive command line option EmptyPrivate command line option EmptyRewritePragma command line option EmptyWhere command line option enable-cluster-counting command line option environment variable Agda_datadir AGDA_DIR, [1], [2], [3], [4]

F

FaceConstraintCannotBeHidden command line option FaceConstraintCannotBeNamed command line option

FixingRelevance command line option FixityInRenamingModule command line option

H

HiddenGeneralize command line option

I

ignore command line option IllformedAsClause command line option InfectiveImport command line option InlineNoExactSplit command line option InstanceArgWithExplicitArg command line option InstanceNoOutputTypeName command line option InstanceWithExplicitArg command line option InteractionMetaBoundaries command line option InvalidCatchallPragma command line option

InvalidCharacterLiteral command line option InvalidConstructorBlock command line option InvalidCoverageCheckPragma command line option InvalidDisplayForm command line option InvalidNoPositivityCheckPragma command line option InvalidNoUniverseCheckPragma command line option InvalidTerminationCheckPragma command line option InversionDepthReached command line option

L

LibUnknownField command line option

M

MissingDataDeclaration command line option MissingDefinitions command line option MissingTypeSignatureForOpaque command line option

ModuleDoesntExport command line option MultipleAttributes command line option

N

NoGuardednessFlag command line option NoMain command line option NotAffectedByOpaque command line option NotAllowedInMutual command line option

NotARewriteRule command line option NotInScope command line option NotStrictlyPositive command line option

O

OldBuiltin command line option OpenPublicAbstract command line option OpenPublicPrivate command line option

optimise-heavily command line option OptionRenamed command line option OverlappingTokensWarning command line option

P

PatternShadowsConstructor command line option PlentyInHardCompileTimeMode command line option PolarityPragmasButNotPostulates command line option PragmaCompiled command line option PragmaCompileErased command line option PragmaCompileList command line option PragmaCompileMaybe command line option

PragmaCompileUnparsable command line option PragmaCompileWrong command line option PragmaCompileWrongName command line option PragmaExpectsDefinedSymbol command line option PragmaExpectsUnambiguousConstructorOrFunction command line option PragmaExpectsUnambiguousProjectionOrFunction command line option PragmaNoTerminationCheck command line option

R

RewriteAmbiguousRules command line option RewriteBeforeFunctionDefinition command line option RewriteBeforeMutualFunctionDefinition command line option RewriteBlockedOnProblems command line option RewriteConstructorParametersNotGeneral command line option RewriteContainsUnsolvedMetaVariables command line option RewriteDoesNotTargetRewriteRelation command line option RewriteHeadSymbolContainsMetas command line option RewriteHeadSymbolIsProjectionLikeFunction command line option

RewriteHeadSymbolIsTypeConstructor command line option RewriteLHSNotDefinitionOrConstructor command line option RewriteLHSReduces command line option RewriteMaybeNonConfluent command line option RewriteMissingRule command line option RewriteNonConfluent command line option RewriteRequiresDefinitions command line option RewriteVariablesBoundMoreThanOnce command line option RewriteVariablesNotBoundByLHS command line option

S

SafeFlagEta command line option SafeFlagInjective command line option SafeFlagNoCoverageCheck command line option SafeFlagNonTerminating command line option SafeFlagNoPositivityCheck command line option SafeFlagNoUniverseCheck command line option

SafeFlagPolarity command line option SafeFlagPostulate command line option SafeFlagPragma command line option SafeFlagTerminating command line option SafeFlagWithoutKFlagPrimEraseEquality command line option ShadowingInTelescope command line option

T

TerminationIssue command line option TooManyArgumentsToSort command line option

TooManyFields command line option

U

UnfoldingWrongName command line option UnfoldTransparentName command line option UnknownFixityInMixfixDecl command line option UnknownNamesInFixityDecl command line option UnknownNamesInPolarityPragmas command line option UnreachableClauses command line option UnsolvedConstraints command line option UnsolvedInteractionMetas command line option UnsolvedMetaVariables command line option UnsupportedAttribute command line option UnsupportedIndexedMatch command line option

UselessAbstract command line option UselessHiding command line option UselessInline command line option UselessInstance command line option UselessMacro command line option UselessOpaque command line option UselessPatternDeclarationForRecord command line option UselessPragma command line option UselessPrivate command line option UselessPublic command line option UserWarning command line option

W

warn command line option WarningProblem command line option WithClauseProjectionFixityMismatch command line option

WithoutKFlagPrimEraseEquality command line option WrongInstanceDeclaration command line option