| O | Agda.TypeChecking.SizedTypes.Syntax |
| obj | Agda.Interaction.JSON |
| Object | |
| 1 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 2 (Type/Class) | Agda.Interaction.JSON |
| 3 (Data Constructor) | Agda.Interaction.JSON |
| object | |
| 1 (Function) | Agda.Compiler.JS.Substitution |
| 2 (Function) | Agda.Interaction.JSON |
| 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 |
| 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 |
| 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 |
| OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract |
| oldOptionName | Agda.Interaction.Options |
| OldQName | Agda.Syntax.Translation.ConcreteToAbstract |
| 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 (Data Constructor) | Agda.Utils.Three |
| 2 (Type/Class) | Agda.Interaction.JSON |
| 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 |
| 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 |
| 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 |
| 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 |
| OpenPublicAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| OpenPublicAbstract_ | Agda.Interaction.Options.Warnings |
| OpenPublicPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| OpenPublicPrivate_ | Agda.Interaction.Options.Warnings |
| 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.Interaction.Options |
| optAutoInline | Agda.Interaction.Options |
| optBacktrackingInstances | 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.Interaction.Options |
| optDiagnosticsColour | Agda.Interaction.Options |
| optDoubleCheck | 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.Interaction.Options |
| OptionError | Agda.Interaction.ExitCode |
| optionError | Agda.Main |
| OptionRenamed | Agda.Interaction.Options |
| OptionRenamed_ | Agda.Interaction.Options.Warnings |
| Options | |
| 1 (Data Constructor) | Agda.Interaction.Options |
| 2 (Type/Class) | Agda.Interaction.JSON |
| 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 |
| optLocalInterfaces | Agda.Interaction.Options |
| OptM | Agda.Interaction.Options |
| optOmegaInOmega | Agda.Interaction.Options |
| optOnlyScopeChecking | Agda.Interaction.Options |
| optOverrideLibrariesFile | Agda.Interaction.Options |
| optPatternMatching | 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 |
| 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 |
| OrgFileType | Agda.Syntax.Common |
| Origin | Agda.Syntax.Common |
| origProjection | Agda.TypeChecking.Records |
| orM | Agda.Utils.Monad |
| orPO | Agda.Utils.PartialOrd |
| 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 |
| 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 |
| 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 |