Agda
v2.7.0.1
Overview
Getting Started
Language Reference
Tools
Contribute
The Agda Team and License
Agda
Index
Index
Symbols
|
A
|
B
|
C
|
D
|
E
|
F
|
H
|
I
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
W
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-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
AbsurdPatternRequiresNoRHS
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-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
AbsurdPatternRequiresNoRHS
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
EmptyPostulate
EmptyPrimitive
EmptyPrivate
EmptyRewritePragma
EmptyWhere
enable-cluster-counting
FaceConstraintCannotBeHidden
FaceConstraintCannotBeNamed
FixityInRenamingModule
HiddenGeneralize
ignore
IllformedAsClause
InfectiveImport
InlineNoExactSplit
InstanceArgWithExplicitArg
InstanceNoOutputTypeName
InstanceWithExplicitArg
InteractionMetaBoundaries
InvalidCatchallPragma
InvalidCharacterLiteral
InvalidConstructor
InvalidConstructorBlock
InvalidCoverageCheckPragma
InvalidNoPositivityCheckPragma
InvalidNoUniverseCheckPragma
InvalidTerminationCheckPragma
InversionDepthReached
LibUnknownField
MissingDeclarations
MissingDefinitions
MissingTypeSignatureForOpaque
ModuleDoesntExport
MultipleAttributes
NoGuardednessFlag
NoMain
NotAffectedByOpaque
NotAllowedInMutual
NotInScope
NotStrictlyPositive
OldBuiltin
OpenPublicAbstract
OpenPublicPrivate
optimise-heavily
OptionRenamed
OverlappingTokensWarning
PatternShadowsConstructor
PlentyInHardCompileTimeMode
PolarityPragmasButNotPostulates
PragmaCompiled
PragmaCompileErased
PragmaCompileList
PragmaCompileMaybe
PragmaNoTerminationCheck
RewriteAmbiguousRules
RewriteBeforeFunctionDefinition
RewriteBeforeMutualFunctionDefinition
RewriteBlockedOnProblems
RewriteConstructorParametersNotGeneral
RewriteContainsUnsolvedMetaVariables
RewriteDoesNotTargetRewriteRelation
RewriteHeadSymbolContainsMetas
RewriteHeadSymbolIsProjection
RewriteHeadSymbolIsProjectionLikeFunction
RewriteHeadSymbolIsTypeConstructor
RewriteLHSNotDefinitionOrConstructor
RewriteLHSReduces
RewriteMaybeNonConfluent
RewriteMissingRule
RewriteNonConfluent
RewriteRequiresDefinitions
RewriteVariablesBoundMoreThanOnce
RewriteVariablesNotBoundByLHS
SafeFlagEta
SafeFlagInjective
SafeFlagNoCoverageCheck
SafeFlagNonTerminating
SafeFlagNoPositivityCheck
SafeFlagNoUniverseCheck
SafeFlagPolarity
SafeFlagPostulate
SafeFlagPragma
SafeFlagTerminating
SafeFlagWithoutKFlagPrimEraseEquality
ShadowingInTelescope
TerminationIssue
TooManyFields
UnfoldTransparentName
UnknownFixityInMixfixDecl
UnknownNamesInFixityDecl
UnknownNamesInPolarityPragmas
UnreachableClauses
UnsolvedConstraints
UnsolvedInteractionMetas
UnsolvedMetaVariables
UnsupportedAttribute
UnsupportedIndexedMatch
UselessAbstract
UselessHiding
UselessInline
UselessInstance
UselessMacro
UselessOpaque
UselessPatternDeclarationForRecord
UselessPragma
UselessPrivate
UselessPublic
UserWarning
warn
WarningProblem
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
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
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
InvalidConstructor
command line option
InvalidConstructorBlock
command line option
InvalidCoverageCheckPragma
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
MissingDeclarations
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
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
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
RewriteHeadSymbolIsProjection
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
TooManyFields
command line option
U
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
WithoutKFlagPrimEraseEquality
command line option
WrongInstanceDeclaration
command line option