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 --build-library 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, [1], [2], [3], [4] --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 --emacs-mode 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 --experimental-lazy-instances 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 --ghc-trace 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 --literate-markdown-only-agda-blocks command line option --load-primitives command line option --local-confluence-check command line option --local-rewriting 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-experimental-lazy-instances 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-literate-markdown-only-agda-blocks command line option --no-load-primitives command line option --no-local-rewriting command line option --no-lossy-unification command line option, [1] --no-main command line option --no-occurrence-analysis command line option --no-omega-in-omega command line option --no-pattern-matching command line option --no-polarity 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-quote-metas 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 --no-write-interfaces command line option --numeric-version command line option --occurrence-analysis command line option --omega-in-omega command line option --only-scope-checking command line option --parallel command line option --pattern-matching command line option --polarity 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-options 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 --quote-metas command line option --require-unique-meta-solutions command line option --rewriting command line option --safe command line option --save-metas command line option --setup 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 -j[N] command line option -l command line option -V command line option -v command line option -W command line option

A

AbstractInLetBindings command line option 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 --build-library --caching --call-by-name --cohesion --color --colour --compile --compile-dir --confluence-check --copatterns --count-clusters --css --cubical, [1], [2], [3], [4] --cubical-compatible --cumulativity --dependency-graph --dependency-graph-include --double-check --emacs-mode --erase-record-parameters --erased-cubical --erased-matches --erasure --eta-equality --exact-split --experimental-irrelevance --experimental-lazy-instances --fast-reduce --flat-split --forced-argument-recursion --forcing --ghc --ghc-dont-call-ghc --ghc-flag --ghc-strict --ghc-strict-data --ghc-trace --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 --literate-markdown-only-agda-blocks --load-primitives --local-confluence-check --local-rewriting --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-experimental-lazy-instances --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-literate-markdown-only-agda-blocks --no-load-primitives --no-local-rewriting --no-lossy-unification, [1] --no-main --no-occurrence-analysis --no-omega-in-omega --no-pattern-matching --no-polarity --no-positivity-check --no-postfix-projections --no-print-pattern-synonyms --no-projection-like --no-prop --no-qualified-instances --no-quote-metas --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 --no-write-interfaces --numeric-version --occurrence-analysis --omega-in-omega --only-scope-checking --parallel --pattern-matching --polarity --positivity-check --postfix-projections --print-agda-app-dir --print-agda-data-dir --print-agda-dir --print-options --print-pattern-synonyms --profile, [1], [2], [3] --projection-like --prop --qualified-instances --quote-metas --require-unique-meta-solutions --rewriting --safe --save-metas --setup --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 -j[N] -l -V -v -W AbstractInLetBindings AbsurdPatternRequiresAbsentRHS all AsPatternShadowsConstructorOrPatternSynonym BuiltinDeclaresIdentifier CantGeneralizeOverSorts ClashesViaRenaming CoinductiveEtaRecord CoInfectiveImport ConflictingPragmaOptions ConfluenceCheckingIncompleteBecauseOfMeta ConfluenceForCubicalNotSupported ConstructorDoesNotFitInData CoverageIssue CoverageNoExactSplit CustomBackendWarning DefinitionBeforeDeclaration DeprecationWarning DivergentModalityInClause DuplicateFields DuplicateRecordDirective DuplicateRewriteRule DuplicateUsing EmptyAbstract EmptyConstructor EmptyField EmptyGeneralize EmptyInstance EmptyMacro EmptyMutual EmptyPolarityPragma EmptyPostulate EmptyPrimitive EmptyPrivate EmptyRewritePragma EmptyWhere FaceConstraintCannotBeHidden FaceConstraintCannotBeNamed FixingCohesion FixingPolarity FixingRelevance FixityInRenamingModule HiddenGeneralize HiddenNotInArgumentPosition ignore IllegalDeclarationInDataDefinition IllformedAsClause InfectiveImport InferredLocalRewrite InlineNoExactSplit InstanceArgWithExplicitArg InstanceNoOutputTypeName InstanceNotInArgumentPosition InstanceWithExplicitArg InteractionMetaBoundaries InvalidCatchallPragma InvalidCharacterLiteral InvalidConstructorBlock InvalidCoverageCheckPragma InvalidDataOrRecDefParameter InvalidDisplayForm InvalidEtaEqualityPragma InvalidNoPositivityCheckPragma InvalidNoUniverseCheckPragma InvalidTacticAttribute InvalidTerminationCheckPragma InversionDepthReached LibUnknownField LocalRewriteOutsideTelescope LocalRewritingConfluenceCheck MacroInLetBindings MismatchedBrackets MisplacedAttributes MisplacedRewrite MissingDataDeclaration MissingDefinitions MissingTypeSignatureForOpaque ModuleDoesntExport MultipleAttributes NoMain NotAffectedByOpaque NotAllowedInMutual NotARewriteRule NotInScope NotStrictlyPositive OldBuiltin OpenImportAbstract OpenImportPrivate OptionRenamed OverlappingTokensWarning PatternShadowsConstructor PlentyInHardCompileTimeMode PolarityPragmasButNotPostulates PragmaCompiled PragmaCompileErased PragmaCompileList PragmaCompileMaybe PragmaCompileUnparsable PragmaCompileWrong PragmaCompileWrongName PragmaExpectsDefinedSymbol PragmaExpectsUnambiguousConstructorOrFunction PragmaExpectsUnambiguousProjectionOrFunction PragmaNoTerminationCheck RecursiveRecordNeedsInductivity RewriteAmbiguousRules RewriteBeforeFunctionDefinition RewriteBeforeMutualFunctionDefinition RewriteBlockedOnProblems RewriteConstructorParametersNotGeneral RewriteContainsUnsolvedMetaVariables RewriteDoesNotTargetRewriteRelation RewriteHeadSymbolContainsMetas RewriteHeadSymbolIsProjectionLikeFunction RewriteHeadSymbolIsTypeConstructor RewriteLHSNotDefinitionOrConstructor RewriteLHSReduces RewriteMaybeNonConfluent RewriteMissingRule RewriteNonConfluent RewriteRequiresDefinitions RewritesNothing RewriteVariablesBoundInSingleton RewriteVariablesBoundMoreThanOnce RewriteVariablesNotBoundByLHS SafeFlagInjective SafeFlagNoCoverageCheck SafeFlagNonTerminating SafeFlagNoPositivityCheck SafeFlagNoUniverseCheck SafeFlagPolarity SafeFlagPostulate SafeFlagPragma SafeFlagTerminating SafeFlagWithoutKFlagPrimEraseEquality ShadowingInTelescope ShouldBeEtaRecordPattern TerminationIssue TooManyArgumentsToSort TooManyFields TooManyPolarities TopLevelPolarity UnfoldingWrongName UnfoldTransparentName UnguardedEtaRecord UnknownAttribute UnknownFixityInMixfixDecl UnknownJSPrimitive UnknownNamesInFixityDecl UnknownNamesInPolarityPragmas UnknownPolarity UnreachableClauses UnsolvedConstraints UnsolvedInteractionMetas UnsolvedMetaVariables UnsupportedAttribute UnsupportedIndexedMatch UnusedImports, [1] UnusedVariablesInDisplayForm UselessAbstract UselessHiding UselessImport UselessInline UselessInstance UselessMacro UselessOpaque UselessPatternDeclarationForRecord UselessPragma UselessPrivate UselessPublic UselessTactic 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

DefinitionBeforeDeclaration command line option DeprecationWarning command line option DivergentModalityInClause command line option DuplicateFields 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 environment variable Agda_datadir AGDA_DIR, [1], [2], [3], [4]

F

FaceConstraintCannotBeHidden command line option FaceConstraintCannotBeNamed command line option FixingCohesion command line option

FixingPolarity command line option FixingRelevance command line option FixityInRenamingModule command line option

H

HiddenGeneralize command line option

HiddenNotInArgumentPosition command line option

I

ignore command line option IllegalDeclarationInDataDefinition command line option IllformedAsClause command line option InfectiveImport command line option InferredLocalRewrite command line option InlineNoExactSplit command line option InstanceArgWithExplicitArg command line option InstanceNoOutputTypeName command line option InstanceNotInArgumentPosition 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 InvalidDataOrRecDefParameter command line option InvalidDisplayForm command line option InvalidEtaEqualityPragma command line option InvalidNoPositivityCheckPragma command line option InvalidNoUniverseCheckPragma command line option InvalidTacticAttribute command line option InvalidTerminationCheckPragma command line option InversionDepthReached command line option

L

LibUnknownField command line option LocalRewriteOutsideTelescope command line option

LocalRewritingConfluenceCheck command line option

M

MacroInLetBindings command line option MismatchedBrackets command line option MisplacedAttributes command line option MisplacedRewrite command line option MissingDataDeclaration command line option

MissingDefinitions command line option MissingTypeSignatureForOpaque command line option ModuleDoesntExport command line option MultipleAttributes command line option

N

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 OpenImportAbstract command line option OpenImportPrivate 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

RecursiveRecordNeedsInductivity command line option 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 RewritesNothing command line option RewriteVariablesBoundInSingleton command line option RewriteVariablesBoundMoreThanOnce command line option RewriteVariablesNotBoundByLHS command line option

S

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 ShouldBeEtaRecordPattern command line option

T

TerminationIssue command line option TooManyArgumentsToSort command line option TooManyFields command line option

TooManyPolarities command line option TopLevelPolarity command line option

U

UnfoldingWrongName command line option UnfoldTransparentName command line option UnguardedEtaRecord command line option UnknownAttribute command line option UnknownFixityInMixfixDecl command line option UnknownJSPrimitive command line option UnknownNamesInFixityDecl command line option UnknownNamesInPolarityPragmas command line option UnknownPolarity 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

UnusedImports command line option, [1] UnusedVariablesInDisplayForm command line option UselessAbstract command line option UselessHiding command line option UselessImport 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 UselessTactic 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