| O | Agda.Auto.Convert |
| Object | Agda.Compiler.JS.Syntax |
| object | |
| 1 (Function) | Agda.Compiler.JS.Substitution |
| 2 (Function) | Agda.Compiler.JS.Parser |
| Occ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccEnv | |
| 1 (Type/Class) | Agda.TypeChecking.Positivity |
| 2 (Data Constructor) | Agda.TypeChecking.Positivity |
| occFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccM | Agda.TypeChecking.Positivity |
| OccPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Occurrence | |
| 1 (Type/Class) | Agda.TypeChecking.Free |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occurrence | Agda.TypeChecking.Free |
| Occurrences | Agda.TypeChecking.Positivity |
| occurrences | Agda.TypeChecking.Positivity |
| Occurs | Agda.TypeChecking.MetaVars.Occurs |
| occurs | Agda.TypeChecking.MetaVars.Occurs |
| occursAs | Agda.TypeChecking.Positivity |
| occursCheck | |
| 1 (Function) | Agda.TypeChecking.MetaVars.Occurs |
| 2 (Function) | Agda.TypeChecking.Rules.LHS.Unify |
| OccursCtx | Agda.TypeChecking.MetaVars.Occurs |
| OccursWhere | Agda.TypeChecking.Positivity |
| octDigit | Agda.Utils.Char |
| ofExpr | Agda.Interaction.BasicOps |
| Offset | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| offsideRule | Agda.Syntax.Parser.Layout |
| ofName | Agda.Interaction.BasicOps |
| OfType | Agda.Interaction.BasicOps |
| OfType' | Agda.Interaction.BasicOps |
| OHCon | Agda.Syntax.Internal.Pattern |
| OHPats | Agda.Syntax.Internal.Pattern |
| OK | Agda.Auto.NarrowingSearch |
| OKHandle | Agda.Auto.NarrowingSearch |
| OKMeta | Agda.Auto.NarrowingSearch |
| OKVal | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract |
| OldName | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
| OldQName | Agda.Syntax.Translation.ConcreteToAbstract |
| oldToNewNotation | Agda.Syntax.Fixity |
| once | Agda.Utils.QuickCheck |
| OneHolePattern | Agda.Syntax.Internal.Pattern |
| OneHolePatterns | Agda.Syntax.Internal.Pattern |
| OneLineMode | Agda.Utils.Pretty |
| oneof | Agda.Utils.QuickCheck |
| OnlyQualified | Agda.Syntax.Common |
| OnlyQualifiedNS | Agda.Syntax.Scope.Base |
| onlyVarsUpTo | Agda.TypeChecking.Positivity |
| onSub | Agda.TypeChecking.Rules.LHS.Unify |
| Op | Agda.TypeChecking.Primitive |
| OpApp | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| OpAppP | Agda.Syntax.Concrete |
| OpAppV | Agda.Syntax.Concrete.Operators.Parser |
| opBrackets | Agda.Syntax.Fixity |
| Open | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| openBrace | Agda.Syntax.Parser.Layout |
| OpenIFS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| openModule_ | Agda.Syntax.Scope.Monad |
| OpenShortHand | Agda.Syntax.Concrete |
| OpenThing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| oplus | Agda.Utils.SemiRing |
| opP | Agda.Syntax.Concrete.Operators.Parser |
| optAllowUnsolved | Agda.Interaction.Options |
| optCompile | Agda.Interaction.Options |
| optCompileDir | Agda.Interaction.Options |
| optCompletenessCheck | Agda.Interaction.Options |
| optCopatterns | Agda.Interaction.Options |
| optCSSFile | Agda.Interaction.Options |
| optDependencyGraph | Agda.Interaction.Options |
| optDisablePositivity | Agda.Interaction.Options |
| optEpicCompile | Agda.Interaction.Options |
| optEpicFlags | Agda.Interaction.Options |
| optExperimentalIrrelevance | Agda.Interaction.Options |
| optForcing | Agda.Interaction.Options |
| optGenerateHTML | Agda.Interaction.Options |
| optGenerateLaTeX | Agda.Interaction.Options |
| optGenerateVimFile | Agda.Interaction.Options |
| optGhcFlags | Agda.Interaction.Options |
| optGHCiInteraction | Agda.Interaction.Options |
| optGuardingTypeConstructors | Agda.Interaction.Options |
| optHTMLDir | Agda.Interaction.Options |
| optIgnoreInterfaces | Agda.Interaction.Options |
| optIncludeDirs | Agda.Interaction.Options |
| optInjectiveTypeConstructors | Agda.Interaction.Options |
| optInputFile | Agda.Interaction.Options |
| optInteractive | Agda.Interaction.Options |
| option | Agda.Utils.ReadP |
| optional | Agda.Utils.ReadP |
| optionError | Agda.Main |
| Options | Agda.Interaction.Options |
| optionsOnReload | Agda.Interaction.InteractionTop |
| OptionsPragma | |
| 1 (Type/Class) | Agda.Interaction.Options |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| optIrrelevantProjections | Agda.Interaction.Options |
| optJSCompile | Agda.Interaction.Options |
| optLaTeXDir | Agda.Interaction.Options |
| optPragmaOptions | Agda.Interaction.Options |
| optProgramName | Agda.Interaction.Options |
| optProofIrrelevance | Agda.Interaction.Options |
| optRunTests | Agda.Interaction.Options |
| optSafe | Agda.Interaction.Options |
| optShowHelp | Agda.Interaction.Options |
| optShowImplicit | Agda.Interaction.Options |
| optShowIrrelevant | Agda.Interaction.Options |
| optShowVersion | Agda.Interaction.Options |
| optSizedTypes | Agda.Interaction.Options |
| optTerminationCheck | Agda.Interaction.Options |
| optTerminationDepth | Agda.Interaction.Options |
| optUniverseCheck | Agda.Interaction.Options |
| optUniversePolymorphism | Agda.Interaction.Options |
| optVerbose | Agda.Interaction.Options |
| optWithoutK | Agda.Interaction.Options |
| Or | Agda.Auto.NarrowingSearch |
| or2M | Agda.Utils.Monad |
| Order | Agda.Termination.CallGraph |
| Ordered | Agda.Utils.QuickCheck |
| OrderedList | Agda.Utils.QuickCheck |
| orderedList | Agda.Utils.QuickCheck |
| orderFields | Agda.TypeChecking.Records |
| orderMat | Agda.Termination.CallGraph |
| Ordinary | Agda.Syntax.Concrete |
| orM | Agda.Utils.Monad |
| OtherAspect | Agda.Interaction.Highlighting.Precise |
| otherAspects | Agda.Interaction.Highlighting.Precise |
| OtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| OtherV | Agda.Syntax.Concrete.Operators.Parser |
| otimes | Agda.Utils.SemiRing |
| Out | Agda.Syntax.Scope.Monad |
| outFile | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| outFile' | Agda.Compiler.MAlonzo.Compiler |
| outFile_ | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| output | Agda.Utils.QuickCheck |
| OutputConstraint | Agda.Interaction.BasicOps |
| OutputConstraint' | Agda.Interaction.BasicOps |
| OutputForm | |
| 1 (Type/Class) | Agda.Interaction.BasicOps |
| 2 (Data Constructor) | Agda.Interaction.BasicOps |
| outputFormId | Agda.Interaction.BasicOps |
| outsideScope | Agda.Syntax.Translation.ConcreteToAbstract |
| overlapping | |
| 1 (Function) | Agda.Interaction.Highlighting.Range |
| 2 (Function) | Agda.TypeChecking.Coverage.Match |
| OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |