| O | Agda.Auto.Convert |
| 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 |
| occFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Occurrence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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.Auto.SearchControl |
| 2 (Function) | Agda.TypeChecking.MetaVars.Occurs |
| 3 (Function) | Agda.TypeChecking.Rules.LHS.Unify |
| OccursWhere | Agda.TypeChecking.Positivity |
| octDigit | Agda.Utils.Char |
| ofExpr | Agda.Interaction.BasicOps |
| 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 |
| OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| OldName | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| OldQName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| on | Agda.Interaction.Highlighting.Vim |
| one | Agda.Termination.Semiring |
| OneHolePattern | Agda.Syntax.Internal.Pattern |
| OneHolePatterns | Agda.Syntax.Internal.Pattern |
| OneLineMode | Agda.Utils.Pretty |
| oneof | Agda.Utils.QuickCheck |
| onSub | Agda.TypeChecking.Rules.LHS.Unify |
| onTrace | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| Op | Agda.TypeChecking.Primitive |
| OpApp | 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 |
| openModule_ | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| 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 |
| optCompileAlonzo | Agda.Interaction.Options |
| optCompileMAlonzo | Agda.Interaction.Options |
| optCompletenessCheck | Agda.Interaction.Options |
| optCSSFile | Agda.Interaction.Options |
| optDisablePositivity | Agda.Interaction.Options |
| optGenerateHTML | Agda.Interaction.Options |
| optGenerateVimFile | Agda.Interaction.Options |
| optGhcFlags | Agda.Interaction.Options |
| optHTMLDir | Agda.Interaction.Options |
| optIgnoreInterfaces | Agda.Interaction.Options |
| optIncludeDirs | 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 |
| OptionsPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| optMAlonzoDir | Agda.Interaction.Options |
| optProgramName | Agda.Interaction.Options |
| optProofIrrelevance | Agda.Interaction.Options |
| optRunTests | Agda.Interaction.Options |
| optShowHelp | Agda.Interaction.Options |
| optShowImplicit | Agda.Interaction.Options |
| optShowVersion | Agda.Interaction.Options |
| optSizedTypes | Agda.Interaction.Options |
| optTerminationCheck | Agda.Interaction.Options |
| optUniverseCheck | Agda.Interaction.Options |
| optUniversePolymorphism | Agda.Interaction.Options |
| optUnreachableCheck | Agda.Interaction.Options |
| optVerbose | Agda.Interaction.Options |
| Or | Agda.Auto.NarrowingSearch |
| Order | Agda.Termination.CallGraph |
| Ordered | Agda.Utils.QuickCheck |
| OrderedList | Agda.Utils.QuickCheck |
| orderedList | Agda.Utils.QuickCheck |
| orderFields | Agda.TypeChecking.Records |
| 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, Agda.Interaction.GhciTop |
| outFile | Agda.Compiler.MAlonzo.Compiler |
| outFile' | Agda.Compiler.MAlonzo.Compiler |
| OutputForm | Agda.Interaction.BasicOps |
| OutputForm' | Agda.Interaction.BasicOps |
| outputFormId | Agda.Interaction.BasicOps |
| outputHsModule | Agda.Compiler.Alonzo.Haskell |
| outsideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| overlapping | Agda.Interaction.Highlighting.Range |
| OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |