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 --caching command line option --call-by-name command line option --cohesion 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 --forcing command line option --guarded command line option --guardedness command line option --help command line option --hidden-argument-puns 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 --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 --load-primitives command line option --local-confluence-check command line option --local-interfaces command line option --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-caching command line option --no-call-by-name command line option --no-cohesion 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-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-pattern-variables command line option --no-level-universe command line option --no-libraries command line option --no-load-primitives command line option --no-main command line option --no-omega-in-omega command line option --no-overlapping-instances 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-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 --omega-in-omega command line option --only-scope-checking command line option --overlapping-instances command line option --pattern-matching command line option --positivity-check command line option --postfix-projections 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 --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

AbsurdPatternRequiresNoRHS command line option

AGDA_DIR, [1], [2] all command line option

C

CantGeneralizeOverSorts command line option CoInfectiveImport command line option command line option +RTS --allow-exec --allow-incomplete-matches --allow-unsolved-metas --auto-inline --caching --call-by-name --cohesion --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 --forcing --guarded --guardedness --help --hidden-argument-puns --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 --keep-pattern-variables --latex --latex-dir --level-universe --library --library-file --load-primitives --local-confluence-check --local-interfaces --main --no-allow-exec --no-allow-incomplete-matches --no-allow-unsolved-metas --no-auto-inline --no-caching --no-call-by-name --no-cohesion --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-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-pattern-variables --no-level-universe --no-libraries --no-load-primitives --no-main --no-omega-in-omega --no-overlapping-instances --no-pattern-matching --no-positivity-check --no-postfix-projections --no-print-pattern-synonyms --no-projection-like --no-prop --no-qualified-instances --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 --omega-in-omega --only-scope-checking --overlapping-instances --pattern-matching --positivity-check --postfix-projections --print-agda-dir --print-pattern-synonyms --profile, [1], [2], [3] --projection-like --prop --qualified-instances --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 AbsurdPatternRequiresNoRHS all CantGeneralizeOverSorts CoInfectiveImport CoverageIssue CoverageNoExactSplit debug DeprecationWarning EmptyAbstract EmptyInstance EmptyMacro EmptyMutual EmptyPostulate EmptyPrimitive EmptyPrivate EmptyRewritePragma enable-cluster-counting ignore IllformedAsClause InfectiveImport InstanceArgWithExplicitArg InstanceNoOutputTypeName InstanceWithExplicitArg InvalidCatchallPragma InvalidNoPositivityCheckPragma InvalidTerminationCheckPragma InversionDepthReached LibUnknownField MissingDefinitions ModuleDoesntExport NotAllowedInMutual NotStrictlyPositive OldBuiltin optimise-heavily OverlappingTokensWarning PolarityPragmasButNotPostulates PragmaCompiled PragmaCompileErased PragmaNoTerminationCheck RewriteMaybeNonConfluent RewriteNonConfluent SafeFlagNonTerminating SafeFlagNoPositivityCheck SafeFlagNoUniverseCheck SafeFlagPolarity SafeFlagPostulate SafeFlagPragma SafeFlagTerminating SafeFlagWithoutKFlagPrimEraseEquality ShadowingInTelescope TerminationIssue UnknownFixityInMixfixDecl UnknownNamesInFixityDecl UnknownNamesInPolarityPragmas UnreachableClauses UnsolvedConstraints UnsolvedInteractionMetas UnsolvedMetaVariables UselessAbstract UselessInline UselessInstance UselessPrivate UselessPublic warn. WithoutKFlagPrimEraseEquality WrongInstanceDeclaration

CoverageIssue command line option CoverageNoExactSplit command line option

D

debug command line option

DeprecationWarning command line option

E

EmptyAbstract command line option EmptyInstance command line option EmptyMacro command line option EmptyMutual command line option EmptyPostulate command line option

EmptyPrimitive command line option EmptyPrivate command line option EmptyRewritePragma command line option enable-cluster-counting command line option environment variable AGDA_DIR, [1], [2]

I

ignore command line option IllformedAsClause command line option InfectiveImport command line option InstanceArgWithExplicitArg command line option InstanceNoOutputTypeName command line option

InstanceWithExplicitArg command line option InvalidCatchallPragma command line option InvalidNoPositivityCheckPragma command line option InvalidTerminationCheckPragma command line option InversionDepthReached command line option

L

LibUnknownField command line option

M

MissingDefinitions command line option

ModuleDoesntExport command line option

N

NotAllowedInMutual command line option

NotStrictlyPositive command line option

O

OldBuiltin command line option optimise-heavily command line option

OverlappingTokensWarning command line option

P

PolarityPragmasButNotPostulates command line option PragmaCompiled command line option

PragmaCompileErased command line option PragmaNoTerminationCheck command line option

R

RewriteMaybeNonConfluent command line option

RewriteNonConfluent command line option

S

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

U

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 UselessAbstract command line option UselessInline command line option UselessInstance command line option UselessPrivate command line option UselessPublic command line option

W

warn. command line option WithoutKFlagPrimEraseEquality command line option

WrongInstanceDeclaration command line option