| O | |
| 1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Type/Class) | Agda.Auto.Convert |
| Object | Agda.Compiler.JS.Syntax |
| object | Agda.Compiler.JS.Substitution |
| OccEnv | |
| 1 (Type/Class) | Agda.TypeChecking.Positivity |
| 2 (Data Constructor) | Agda.TypeChecking.Positivity |
| OccM | Agda.TypeChecking.Positivity |
| Occurrence | |
| 1 (Type/Class) | Agda.TypeChecking.Positivity.Occurrence |
| 2 (Type/Class) | Agda.TypeChecking.Free |
| 3 (Type/Class) | Agda.TypeChecking.Free.Old |
| occurrence | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.TypeChecking.Free.Old |
| 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 |
| OccursHere | Agda.TypeChecking.Positivity |
| OccursHere' | Agda.TypeChecking.Positivity |
| occursIn | Agda.Compiler.Treeless.Subst |
| OccursWhere | |
| 1 (Type/Class) | Agda.TypeChecking.Positivity.Occurrence |
| 2 (Data Constructor) | Agda.TypeChecking.Positivity.Occurrence |
| octDigit | Agda.Utils.Char |
| ofExpr | Agda.Interaction.BasicOps |
| Offset | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| 3 (Type/Class) | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| offset | Agda.TypeChecking.SizedTypes.Syntax |
| offsideRule | Agda.Syntax.Parser.Layout |
| ofName | Agda.Interaction.BasicOps |
| OfType | Agda.Interaction.BasicOps |
| OfType' | Agda.Interaction.BasicOps |
| 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 |
| 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.InteractionTop |
| oldInteractionScopes | Agda.Interaction.InteractionTop |
| 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 |
| OldSizeConstraint | Agda.TypeChecking.SizedTypes |
| OldSizeExpr | Agda.TypeChecking.SizedTypes |
| oldSizeExpr | Agda.TypeChecking.SizedTypes |
| oldSolver | Agda.TypeChecking.SizedTypes |
| oldSolveSizeConstraints | Agda.TypeChecking.SizedTypes |
| once | Agda.Compiler.Treeless.Subst |
| One | Agda.Utils.Three |
| oneFreeVariable | Agda.Syntax.Common |
| OneHole | Agda.Utils.AffineHole |
| OneLineMode | Agda.Utils.Pretty |
| onlyOnce | Agda.TypeChecking.Warnings |
| OnlyQualified | Agda.Syntax.Common |
| OnlyQualifiedNS | Agda.Syntax.Scope.Base |
| onlyReduceProjections | 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 |
| OpAppP | Agda.Syntax.Concrete |
| OpAppV | Agda.Syntax.Concrete.Operators.Parser |
| opBrackets | Agda.Syntax.Fixity |
| 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, Agda.Compiler.Backend |
| 4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| open | Agda.TypeChecking.Names |
| openBrace | Agda.Syntax.Parser.Layout |
| Opened | Agda.Syntax.Scope.Base |
| OpenInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| OpenKind | Agda.Syntax.Scope.Monad |
| openMetasToPostulates | Agda.TypeChecking.MetaVars |
| openModule_ | Agda.Syntax.Scope.Monad |
| 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 |
| 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 |
| optAllowUnsolved | Agda.Interaction.Options |
| OptArg | Agda.Interaction.Options |
| optAutoInline | Agda.Interaction.Options |
| optCaching | Agda.Interaction.Options |
| optCompileDir | Agda.Interaction.Options |
| optCompileNoMain | Agda.Interaction.Options |
| optCompletenessCheck | Agda.Interaction.Options |
| optCopatterns | Agda.Interaction.Options |
| optCountClusters | Agda.Interaction.Options |
| optCSSFile | Agda.Interaction.Options |
| optCubical | Agda.Interaction.Options |
| optDefaultLibs | Agda.Interaction.Options |
| optDependencyGraph | Agda.Interaction.Options |
| OptDescr | Agda.Interaction.Options |
| optDisablePositivity | Agda.Interaction.Options |
| optDoubleCheck | Agda.Interaction.Options |
| optEta | Agda.Interaction.Options |
| optExactSplit | Agda.Interaction.Options |
| optExperimentalIrrelevance | Agda.Interaction.Options |
| optFastReduce | Agda.Interaction.Options |
| optForcing | Agda.Interaction.Options |
| optGenerateHTML | Agda.Interaction.Options |
| optGenerateLaTeX | Agda.Interaction.Options |
| optGenerateVimFile | Agda.Interaction.Options |
| optGhcCallGhc | Agda.Compiler.MAlonzo.Compiler |
| optGhcCompile | Agda.Compiler.MAlonzo.Compiler |
| optGhcFlags | Agda.Compiler.MAlonzo.Compiler |
| optGHCiInteraction | Agda.Interaction.Options |
| optGuardedness | Agda.Interaction.Options |
| optHTMLDir | Agda.Interaction.Options |
| optHTMLHighlight | Agda.Interaction.Options |
| optIgnoreAllInterfaces | Agda.Interaction.Options |
| optIgnoreInterfaces | Agda.Interaction.Options |
| optIncludePaths | 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 |
| option | Agda.Utils.Parser.ReadP |
| optional | Agda.Utils.Parser.ReadP |
| optionError | Agda.Main |
| Options | Agda.Interaction.Options |
| options | Agda.Compiler.Backend |
| optionsOnReload | Agda.Interaction.InteractionTop |
| OptionsPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.Interaction.Options |
| optIrrelevantProjections | Agda.Interaction.Options |
| optJSCompile | Agda.Compiler.JS.Compiler |
| optJSONInteraction | Agda.Interaction.Options |
| optLaTeXDir | Agda.Interaction.Options |
| optLibraries | Agda.Interaction.Options |
| OptM | Agda.Interaction.Options |
| optOmegaInOmega | Agda.Interaction.Options |
| optOnlyScopeChecking | Agda.Interaction.Options |
| optOptimSmashing | Agda.Interaction.Options |
| optOverlappingInstances | Agda.Interaction.Options |
| optOverrideLibrariesFile | Agda.Interaction.Options |
| optPatternMatching | Agda.Interaction.Options |
| optPostfixProjections | Agda.Interaction.Options |
| optPragmaOptions | Agda.Interaction.Options |
| optPrintPatternSynonyms | Agda.Interaction.Options |
| optProgramName | Agda.Interaction.Options |
| optProp | Agda.Interaction.Options |
| optRewriting | 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 |
| optSyntacticEquality | Agda.Interaction.Options |
| optTerminationCheck | Agda.Interaction.Options |
| optTerminationDepth | 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 |
| Or | Agda.Auto.NarrowingSearch |
| or2M | Agda.Utils.Monad |
| Order | Agda.Termination.Order |
| orderFields | 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.Interaction.Highlighting.Precise |
| otherAspects | Agda.Interaction.Highlighting.Precise |
| OtherBackend | Agda.Interaction.InteractionTop |
| OtherFlex | 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 |
| otimes | Agda.Utils.SemiRing |
| OType | Agda.Syntax.Internal |
| 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 |
| outgoing | Agda.TypeChecking.SizedTypes.WarshallSolver |
| 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 |
| OutputTypeName | |
| 1 (Type/Class) | Agda.TypeChecking.Telescope |
| 2 (Data Constructor) | Agda.TypeChecking.Telescope |
| OutputTypeNameNotYetKnown | Agda.TypeChecking.Telescope |
| OutputTypeVar | Agda.TypeChecking.Telescope |
| OutputTypeVisiblePi | Agda.TypeChecking.Telescope |
| over | Agda.Utils.Lens |
| Overlappable | Agda.Syntax.Common |
| overlapping | Agda.Interaction.Highlighting.Range |
| OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| OverlappingTokensError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| OverlappingTokensWarning | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| OverlappingTokensWarning_ | Agda.Interaction.Options.Warnings |
| ozero | Agda.Utils.SemiRing |