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 --color command line option --colour command line option --copatterns command line option --count-clusters command line option --css command line option --defaults-file command line option --dependency-graph command line option --dependency-graph-include command line option --double-check command line option --emacs-mode command line option --eta-equality command line option --exact-split command line option --experimental-lazy-instances command line option --fast-reduce command line option --forcing 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 --instance-search-depth command line option --interaction command line option --interaction-exit-on-error command line option --interaction-json command line option --inversion-max-depth command line option --keep-covering-clauses command line option --keep-pattern-variables 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 --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-copatterns command line option --no-count-clusters command line option --no-default-libraries command line option --no-double-check command line option --no-eta-equality command line option --no-exact-split command line option --no-experimental-lazy-instances command line option --no-fast-reduce command line option --no-forcing command line option

--no-hidden-argument-puns command line option --no-import-sorts command line option --no-infer-absurd-clauses command line option --no-keep-covering-clauses command line option --no-keep-pattern-variables 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-lossy-unification command line option, [1] --no-main command line option --no-occurrence-analysis 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-quote-metas command line option --no-require-unique-meta-solutions 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-termination-check command line option --no-unicode command line option --no-write-interfaces command line option --numeric-version command line option --occurrence-analysis command line option --only-scope-checking command line option --parallel command line option --pattern-matching command line option --positivity-check command line option --postfix-projections command line option --print-app-dir command line option --print-data-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 --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 --termination-check command line option --termination-depth command line option --trace-imports command line option --transliterate command line option --unicode command line option --verbose command line option --version command line option --vim command line option --warning command line option -?[{TOPIC}] 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_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 --color --colour --copatterns --count-clusters --css --defaults-file --dependency-graph --dependency-graph-include --double-check --emacs-mode --eta-equality --exact-split --experimental-lazy-instances --fast-reduce --forcing --help --hidden-argument-puns --highlight-occurrences --html --html-dir --html-highlight --ignore-all-interfaces --ignore-interfaces --import-sorts --include-path --infer-absurd-clauses --instance-search-depth --interaction --interaction-exit-on-error --interaction-json --inversion-max-depth --keep-covering-clauses --keep-pattern-variables --latex --latex-dir --level-universe --library --library-file --literate-markdown-only-agda-blocks --load-primitives --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-copatterns --no-count-clusters --no-default-libraries --no-double-check --no-eta-equality --no-exact-split --no-experimental-lazy-instances --no-fast-reduce --no-forcing --no-hidden-argument-puns --no-import-sorts --no-infer-absurd-clauses --no-keep-covering-clauses --no-keep-pattern-variables --no-level-universe --no-libraries --no-literate-markdown-only-agda-blocks --no-load-primitives --no-lossy-unification, [1] --no-main --no-occurrence-analysis --no-pattern-matching --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-save-metas --no-show-identity-substitutions --no-show-implicit --no-show-irrelevant --no-termination-check --no-unicode --no-write-interfaces --numeric-version --occurrence-analysis --only-scope-checking --parallel --pattern-matching --positivity-check --postfix-projections --print-app-dir --print-data-dir --print-options --print-pattern-synonyms --profile, [1], [2], [3] --projection-like --prop --qualified-instances --quote-metas --require-unique-meta-solutions --safe --save-metas --setup --show-identity-substitutions --show-implicit --show-irrelevant --termination-check --termination-depth --trace-imports --transliterate --unicode --verbose --version --vim --warning -?[{TOPIC}] -i -j[N] -l -V -v -W AbstractInLetBindings AbsurdPatternRequiresAbsentRHS all AsPatternShadowsConstructorOrPatternSynonym BuiltinDeclaresIdentifier CantGeneralizeOverSorts ClashesViaRenaming CoinductiveEtaRecord CoInfectiveImport ConflictingPragmaOptions ConstructorDoesNotFitInData CoverageIssue CoverageNoExactSplit CustomBackendWarning DefinitionBeforeDeclaration DeprecationWarning DuplicateFields DuplicateRecordDirective DuplicateUsing EmptyAbstract EmptyConstructor EmptyField EmptyGeneralize EmptyInstance EmptyMacro EmptyMutual EmptyPolarityPragma EmptyPostulate EmptyPrimitive EmptyPrivate EmptyWhere FaceConstraintCannotBeHidden FaceConstraintCannotBeNamed FixityInRenamingModule HiddenGeneralize HiddenNotInArgumentPosition ignore IllegalDeclarationInDataDefinition IllformedAsClause InfectiveImport InlineNoExactSplit InstanceArgWithExplicitArg InstanceNoOutputTypeName InstanceNotInArgumentPosition InstanceWithExplicitArg InteractionMetaBoundaries InvalidCatchallPragma InvalidCharacterLiteral InvalidConstructorBlock InvalidCoverageCheckPragma InvalidDataOrRecDefParameter InvalidDisplayForm InvalidNoPositivityCheckPragma InvalidNoUniverseCheckPragma InvalidTacticAttribute InvalidTerminationCheckPragma InversionDepthReached LibUnknownField MacroInLetBindings MismatchedBrackets MisplacedAttributes MissingDataDeclaration MissingDefinitions MissingTypeSignatureForOpaque ModuleDoesntExport NoMain NotAffectedByOpaque NotAllowedInMutual NotInScope NotStrictlyPositive OldBuiltin OpenImportAbstract OpenImportPrivate OptionRenamed OverlappingTokensWarning PatternShadowsConstructor PolarityPragmasButNotPostulates PragmaCompiled PragmaCompileWrongName PragmaExpectsDefinedSymbol PragmaExpectsUnambiguousConstructorOrFunction PragmaExpectsUnambiguousProjectionOrFunction PragmaNoTerminationCheck RecursiveRecordNeedsInductivity RewritesNothing SafeFlagEta SafeFlagInjective SafeFlagNoCoverageCheck SafeFlagNonTerminating SafeFlagNoPositivityCheck SafeFlagNoUniverseCheck SafeFlagPolarity SafeFlagPostulate SafeFlagPragma SafeFlagTerminating ShadowingInTelescope ShouldBeEtaRecordPattern TerminationIssue TooManyArgumentsToSort TooManyFields TooManyPolarities UnfoldingWrongName UnfoldTransparentName UnknownAttribute UnknownFixityInMixfixDecl 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 WrongInstanceDeclaration

ConflictingPragmaOptions 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 DuplicateFields command line option

DuplicateRecordDirective 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 EmptyWhere command line option environment variable AGDA_DIR, [1], [2], [3], [4] Mikan_datadir

F

FaceConstraintCannotBeHidden command line option FaceConstraintCannotBeNamed 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 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 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

M

MacroInLetBindings command line option Mikan_datadir MismatchedBrackets command line option MisplacedAttributes command line option

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

N

NoMain command line option NotAffectedByOpaque command line option NotAllowedInMutual 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 PolarityPragmasButNotPostulates command line option PragmaCompiled 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

RewritesNothing 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 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

U

UnfoldingWrongName command line option UnfoldTransparentName command line option UnknownAttribute command line option UnknownFixityInMixfixDecl 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 WrongInstanceDeclaration command line option