Agda-2.8.0: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - O

O | Agda.TypeChecking.SizedTypes.Syntax
obj | Agda.Interaction.JSON
Object |
1 (Data Constructor) | Agda.Interaction.JSON
2 (Type/Class) | Agda.Interaction.JSON
3 (Data Constructor) | Agda.Compiler.JS.Syntax
object |
1 (Function) | Agda.Interaction.JSON
2 (Function) | Agda.Compiler.JS.Substitution
ObjectWithSingleField | Agda.Interaction.JSON
observeHiding | Agda.Syntax.Concrete
observeModifiers | Agda.Syntax.Concrete
observeRelevance | Agda.Syntax.Concrete
occCxtSize | Agda.TypeChecking.MetaVars.Occurs
OccEnv |
1 (Type/Class) | Agda.TypeChecking.Positivity
2 (Data Constructor) | Agda.TypeChecking.Positivity
OccM | Agda.TypeChecking.Positivity
occMeta | Agda.TypeChecking.MetaVars.Occurs
occRHS | Agda.TypeChecking.MetaVars.Occurs
occUnfold | Agda.TypeChecking.MetaVars.Occurs
Occurrence | Agda.TypeChecking.Positivity.Occurrence
Occurrences | Agda.TypeChecking.Positivity
occurrences | Agda.TypeChecking.Positivity
OccurrencesBuilder | Agda.TypeChecking.Positivity
OccurrencesBuilder' | Agda.TypeChecking.Positivity
Occurs |
1 (Type/Class) | Agda.Compiler.Treeless.Subst
2 (Data Constructor) | Agda.Compiler.Treeless.Subst
3 (Type/Class) | Agda.TypeChecking.MetaVars.Occurs
occurs | Agda.TypeChecking.MetaVars.Occurs
OccursAs | Agda.TypeChecking.Positivity
OccursAs' | Agda.TypeChecking.Positivity
OccursCheck | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
occursCheck | Agda.TypeChecking.MetaVars.Occurs
OccursCtx | Agda.TypeChecking.MetaVars.Occurs
OccursExtra |
1 (Type/Class) | Agda.TypeChecking.MetaVars.Occurs
2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs
OccursHere | Agda.TypeChecking.Positivity
OccursHere' | Agda.TypeChecking.Positivity
occursIn | Agda.Compiler.Treeless.Subst
OccursM | Agda.TypeChecking.MetaVars.Occurs
OccursWhere |
1 (Type/Class) | Agda.TypeChecking.Positivity.Occurrence
2 (Data Constructor) | Agda.TypeChecking.Positivity.Occurrence
occurs_ | Agda.TypeChecking.MetaVars.Occurs
occVars | Agda.TypeChecking.MetaVars.Occurs
ofExpr | Agda.Interaction.Base
Offset |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class) | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Data Constructor) | Agda.TypeChecking.SizedTypes.WarshallSolver
offset | Agda.TypeChecking.SizedTypes.Syntax
offsideRule | Agda.Syntax.Parser.Layout
ofName | Agda.Interaction.Base
OfType | Agda.Interaction.Base
OfType' | Agda.Interaction.Base
OIrrDot | Agda.Syntax.Common
OIrrInferred | Agda.Syntax.Common
OIrrIrr | Agda.Syntax.Common
OIrrIrrelevant | Agda.Syntax.Common
OldBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OldBuiltin_ | Agda.Interaction.Options.Warnings
oldCanonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes
oldComputeSizeConstraint | Agda.TypeChecking.SizedTypes
oldComputeSizeConstraints | Agda.TypeChecking.SizedTypes
OldInteractionScopes | Agda.Interaction.Base
oldInteractionScopes | Agda.Interaction.Base
oldOptionName | Agda.Interaction.Options
OldSizeConstraint | Agda.TypeChecking.SizedTypes
OldSizeExpr | Agda.TypeChecking.SizedTypes
oldSizeExpr | Agda.TypeChecking.SizedTypes
omegaFlexRig | Agda.TypeChecking.Free.Lazy
omitField | Agda.Interaction.JSON
omitField1 | Agda.Interaction.JSON
omitField2 | Agda.Interaction.JSON
omitNothingFields | Agda.Interaction.JSON
omittedField | Agda.Interaction.JSON
omittedField1 | Agda.Interaction.JSON
omittedField2 | Agda.Interaction.JSON
on | Agda.Utils.Function
onBlockingMetasM | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
once | Agda.Compiler.Treeless.Subst
One |
1 (Type/Class) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Utils.Three
oneFlexRig | Agda.TypeChecking.Free.Lazy
oneFreeVariable | Agda.Syntax.Common
OneHole | Agda.Utils.AffineHole
OneLineMode | Agda.Syntax.Common.Pretty
oneVarOcc | Agda.TypeChecking.Free.Lazy
onLetBindingType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyErased | Agda.Syntax.Parser.Helpers
OnlyLazy |
1 (Type/Class) | Agda.TypeChecking.Patterns.Match
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match
OnlyReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyReduceProjections | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyReduceTypes | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyShowIfUnsolved | Agda.TypeChecking.Warnings
OnlyVarsUpTo | Agda.TypeChecking.Positivity
onReduceEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
oone | Agda.Utils.SemiRing
Op | Agda.TypeChecking.Primitive
OpApp |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Concrete
OpAppArgs | Agda.Syntax.Concrete
OpAppArgs' | Agda.Syntax.Concrete
OpAppArgs0 | Agda.Syntax.Concrete
OpAppP | Agda.Syntax.Concrete
OpAppV | Agda.Syntax.Concrete.Operators.Parser
Opaque | Agda.Syntax.Concrete
OpaqueBlock |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opaqueDecls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpaqueDef | Agda.Syntax.Common
OpaqueId |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
opaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpaqueInMutual | Agda.Syntax.Concrete.Definitions.Errors
OpaqueInMutual_ | Agda.Interaction.Options.Errors
opaqueParent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opaqueRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opaqueUnfolding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opBrackets | Agda.Syntax.Fixity
opBrackets' | Agda.Syntax.Fixity
Open |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
open | Agda.TypeChecking.Names
Opened | Agda.Syntax.Scope.Base
OpenImportAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
OpenImportAbstract_ | Agda.Interaction.Options.Warnings
OpenImportPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
OpenImportPrivate_ | Agda.Interaction.Options.Warnings
OpenKind | Agda.Syntax.Scope.Monad
OpenMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openMetasToPostulates | Agda.TypeChecking.MetaVars
openModule | Agda.Syntax.Scope.Monad
openModule_ | Agda.Syntax.Scope.Monad
OpenNotImport | Agda.Syntax.Concrete.Definitions.Errors
OpenOrImport | Agda.Syntax.Concrete.Definitions.Errors
OpenS | Agda.Syntax.Abstract
OpenShortHand | Agda.Syntax.Concrete
OpenThing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingCheckpoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingCheckpointMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openVerboseBracket | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OperatorInformation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OperatorsExpr | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
OperatorsPattern | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
OperatorType | Agda.Syntax.Concrete.Operators.Parser
oplus | Agda.Utils.SemiRing
opP | Agda.Syntax.Concrete.Operators.Parser
oppositeDAG | Agda.Utils.Graph.AdjacencyMap.Unidirectional
oppPO | Agda.Utils.PartialOrd
optAbsoluteIncludePaths | Agda.Interaction.Options
optAllowExec | Agda.Interaction.Options
optAllowIncompleteMatch | Agda.Interaction.Options
optAllowUnsolved | Agda.Interaction.Options
OptArg | Agda.Utils.GetOpt, Agda.Interaction.Options
optAutoInline | Agda.Interaction.Options
optBacktrackingInstances | Agda.Interaction.Options
optBuildLibrary | Agda.Interaction.Options
optCaching | Agda.Interaction.Options
optCallByName | Agda.Interaction.Options
optCohesion | Agda.Interaction.Options
optCompileDir | Agda.Interaction.Options
optCompileNoMain | Agda.Interaction.Options
optConfluenceCheck | Agda.Interaction.Options
optCopatterns | Agda.Interaction.Options
optCountClusters | Agda.Interaction.Options
optCubical | Agda.Interaction.Options
optCubicalCompatible | Agda.Interaction.Options
optCumulativity | Agda.Interaction.Options
optDefaultLibs | Agda.Interaction.Options
OptDescr | Agda.Utils.GetOpt, Agda.Interaction.Options
optDiagnosticsColour | Agda.Interaction.Options
optDoubleCheck | Agda.Interaction.Options
optEmacsMode | Agda.Interaction.Options
optErasedMatches | Agda.Interaction.Options
optEraseRecordParameters | Agda.Interaction.Options
optErasure | Agda.Interaction.Options
optEta | Agda.Interaction.Options
optExitOnError | Agda.Interaction.Options
optExperimentalIrrelevance | Agda.Interaction.Options
optExplicitHints | Agda.Mimer.Options
optFastReduce | Agda.Interaction.Options
optFirstOrder | Agda.Interaction.Options
optFlatSplit | Agda.Interaction.Options
optForcedArgumentRecursion | Agda.Interaction.Options
optForcing | Agda.Interaction.Options
optGenerateVimFile | Agda.Interaction.Options
optGhcBin | Agda.Compiler.MAlonzo.Misc
optGhcCallGhc | Agda.Compiler.MAlonzo.Misc
optGhcCompileDir | Agda.Compiler.MAlonzo.Misc
optGhcFlags | Agda.Compiler.MAlonzo.Misc
optGHCiInteraction | Agda.Interaction.Options
optGhcStrict | Agda.Compiler.MAlonzo.Misc
optGhcStrictData | Agda.Compiler.MAlonzo.Misc
optGuarded | Agda.Interaction.Options
optGuardedness | Agda.Interaction.Options
optHiddenArgumentPuns | Agda.Interaction.Options
optHintMode | Agda.Mimer.Options
optIgnoreAllInterfaces | Agda.Interaction.Options
optIgnoreInterfaces | Agda.Interaction.Options
optImportSorts | Agda.Interaction.Options
optIncludePaths | Agda.Interaction.Options
optInferAbsurdClauses | Agda.Interaction.Options
optInjectiveTypeConstructors | Agda.Interaction.Options
optInputFile | Agda.Interaction.Options
optInstanceSearchDepth | Agda.Interaction.Options
optInteractive | Agda.Interaction.Options
optInversionMaxDepth | Agda.Interaction.Options
Option | Agda.Utils.GetOpt, Agda.Interaction.Options
OptionError |
1 (Data Constructor) | Agda.Interaction.ExitCode
2 (Type/Class) | Agda.Interaction.Options
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
optionError | Agda.Main
OptionError_ | Agda.Interaction.Options.Errors
OptionRenamed | Agda.Interaction.Options
OptionRenamed_ | Agda.Interaction.Options.Warnings
Options |
1 (Type/Class) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Interaction.Options
3 (Type/Class) | Agda.Mimer.Options
4 (Data Constructor) | Agda.Mimer.Options
options | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
optionsOnReload | Agda.Interaction.Base
OptionsPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library
3 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library
4 (Data Constructor) | Agda.Syntax.Abstract
OptionWarning |
1 (Type/Class) | Agda.Interaction.Options
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
optionWarningName | Agda.Interaction.Options
optIrrelevantProjections | Agda.Interaction.Options
optJSCompile | Agda.Compiler.JS.Compiler
optJSMinify | Agda.Compiler.JS.Compiler
optJSModuleStyle | Agda.Compiler.JS.Compiler
optJSONInteraction | Agda.Interaction.Options
optJSOptimize | Agda.Compiler.JS.Compiler
optJSVerify | Agda.Compiler.JS.Compiler
optKeepCoveringClauses | Agda.Interaction.Options
optKeepPatternVariables | Agda.Interaction.Options
optLargeIndices | Agda.Interaction.Options
optLevelUniverse | Agda.Interaction.Options
optLibraries | Agda.Interaction.Options
optList | Agda.Mimer.Options
optLoadPrimitives | Agda.Interaction.Options
OptM | Agda.Interaction.Options
optOmegaInOmega | Agda.Interaction.Options
optOnlyScopeChecking | Agda.Interaction.Options
optOverrideLibrariesFile | Agda.Interaction.Options
optPatternMatching | Agda.Interaction.Options
optPolarity | Agda.Interaction.Options
optPositivityCheck | Agda.Interaction.Options
optPostfixProjections | Agda.Interaction.Options
optPragmaOptions | Agda.Interaction.Options
optPrintAgdaAppDir | Agda.Interaction.Options
optPrintAgdaDataDir | Agda.Interaction.Options
optPrintHelp | Agda.Interaction.Options
optPrintPatternSynonyms | Agda.Interaction.Options
optPrintVersion | Agda.Interaction.Options
optProfiling | Agda.Interaction.Options
optProgramName | Agda.Interaction.Options
optProjectionLike | Agda.Interaction.Options
optProp | Agda.Interaction.Options
optQualifiedInstances | Agda.Interaction.Options
optRequireUniqueMetaSolutions | Agda.Interaction.Options
optRewriting | Agda.Interaction.Options
optSafe | Agda.Interaction.Options
optSaveMetas | Agda.Interaction.Options
optSetup | Agda.Interaction.Options
optShowGeneralized | Agda.Interaction.Options
optShowIdentitySubstitutions | Agda.Interaction.Options
optShowImplicit | Agda.Interaction.Options
optShowIrrelevant | Agda.Interaction.Options
optSizedTypes | Agda.Interaction.Options
optSkip | Agda.Mimer.Options
optSyntacticEquality | Agda.Interaction.Options
optTerminationCheck | Agda.Interaction.Options
optTerminationDepth | Agda.Interaction.Options
optTimeout | Agda.Mimer.Options
optTraceImports | Agda.Interaction.Options
optTransliterate | Agda.Interaction.Options
optTrustedExecutables | Agda.Interaction.Options
optTwoLevel | Agda.Interaction.Options
optUniverseCheck | Agda.Interaction.Options
optUniversePolymorphism | Agda.Interaction.Options
optUseLibs | Agda.Interaction.Options
optUseUnicode | Agda.Interaction.Options
optVerbose | Agda.Interaction.Options
optWarningMode | Agda.Interaction.Options
optWithoutK | Agda.Interaction.Options
or2M | Agda.Utils.Monad
Order | Agda.Termination.Order
OrderCandidates | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
orderFields | Agda.TypeChecking.Records
orderFieldsFail | Agda.TypeChecking.Records
orderFieldsWarn | Agda.TypeChecking.Records
orderMat | Agda.Termination.Order
orderSemiring | Agda.Termination.Order
Ordinary | Agda.Syntax.Concrete
orEitherM | Agda.Utils.Monad
ORelInferred | Agda.Syntax.Common
ORelRelevant | Agda.Syntax.Common
OrgFileType | Agda.Syntax.Common
Origin | Agda.Syntax.Common
OriginIrrelevant | Agda.Syntax.Common
OriginRelevant | Agda.Syntax.Common
OriginShapeIrrelevant | Agda.Syntax.Common
origProjection | Agda.TypeChecking.Records
orM | Agda.Utils.Monad
orPO | Agda.Utils.PartialOrd
OShIrrDotDot | Agda.Syntax.Common
OShIrrInferred | Agda.Syntax.Common
OShIrrShapeIrrelevant | Agda.Syntax.Common
OShIrrShIrr | Agda.Syntax.Common
ostar | Agda.Utils.SemiRing
OTerm | Agda.Syntax.Internal
OtherAspect | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
otherAspects | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
OtherBackend | Agda.Interaction.Base
OtherDefName | Agda.Syntax.Scope.Base
OtherFlex | Agda.TypeChecking.Rules.LHS.Problem
otherPatterns | Agda.TypeChecking.Rules.LHS.Problem
OtherPragma | Agda.Utils.Haskell.Syntax
OtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OtherType | Agda.Syntax.Internal
OtherV | Agda.Syntax.Concrete.Operators.Parser
otherValue | Agda.Utils.Graph.AdjacencyMap.Unidirectional
otimes | Agda.Utils.SemiRing
OType | Agda.Syntax.Internal
outFile | Agda.Compiler.JS.Compiler
outgoing | Agda.TypeChecking.SizedTypes.WarshallSolver
OutputConstraint | Agda.Interaction.Output
OutputConstraint' | Agda.Interaction.Base
OutputConstraint_boot | Agda.Interaction.Base
OutputContextEntry | Agda.Interaction.Base
OutputForm |
1 (Data Constructor) | Agda.Interaction.Base
2 (Type/Class) | Agda.Interaction.Output
outputFormId | Agda.Interaction.BasicOps
OutputForm_boot | Agda.Interaction.Base
OutputTypeName |
1 (Type/Class) | Agda.TypeChecking.InstanceArguments
2 (Data Constructor) | Agda.TypeChecking.InstanceArguments
OutputTypeNameNotYetKnown | Agda.TypeChecking.InstanceArguments
OutputTypeVar | Agda.TypeChecking.InstanceArguments
OutputTypeVisiblePi | Agda.TypeChecking.InstanceArguments
outsideLocalVars | Agda.Syntax.Scope.Monad
over | Agda.Utils.Lens
Overapplied |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
overCallSites | Agda.Utils.CallStack
OverlapMode | Agda.Syntax.Common
Overlappable |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Common
Overlapping | Agda.Syntax.Common
overlapping | Agda.Interaction.Highlighting.Range
OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OverlappingProjects_ | Agda.Interaction.Options.Errors
overlappings | Agda.Interaction.Highlighting.Range
OverlappingTokensError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarning | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarning_ | Agda.Interaction.Options.Warnings
OverlapPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Overlaps | Agda.Syntax.Common
ozero | Agda.Utils.SemiRing