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
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.Old
3 (Type/Class)	Agda.TypeChecking.Free
occurrence
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
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
4 (Data Constructor)	Agda.TypeChecking.Positivity
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	Agda.TypeChecking.Positivity.Occurrence
OccursWheres	Agda.TypeChecking.Positivity
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
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
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
OneLineMode	Agda.Utils.Pretty
OnlyQualified	Agda.Syntax.Common
OnlyQualifiedNS	Agda.Syntax.Scope.Base
onlyReduceProjections	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
OnlyVarsUpTo	Agda.TypeChecking.Positivity
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
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
Opened	Agda.Syntax.Scope.Base
OpenIFS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openMetasToPostulates	Agda.TypeChecking.MetaVars
openModule_	Agda.Syntax.Scope.Monad
OpenShortHand	Agda.Syntax.Concrete
OpenThing	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openThing	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
openThingCtxIds	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OperatorChangeMessage	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OperatorInformation	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Operators	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
optCaching	Agda.Interaction.Options
optCompileDir	Agda.Interaction.Options
optCompileNoMain	Agda.Interaction.Options
optCompletenessCheck	Agda.Interaction.Options
optCopatterns	Agda.Interaction.Options
optCSSFile	Agda.Interaction.Options
optDefaultLibs	Agda.Interaction.Options
optDependencyGraph	Agda.Interaction.Options
optDisablePositivity	Agda.Interaction.Options
optEpicCompile	Agda.Interaction.Options
optEpicFlags	Agda.Interaction.Options
optEta	Agda.Interaction.Options
optExactSplit	Agda.Interaction.Options
optExperimentalIrrelevance	Agda.Interaction.Options
optForcing	Agda.Interaction.Options
optGenerateHTML	Agda.Interaction.Options
optGenerateLaTeX	Agda.Interaction.Options
optGenerateVimFile	Agda.Interaction.Options
optGhcCallGhc	Agda.Interaction.Options
optGhcCompile	Agda.Interaction.Options
optGhcFlags	Agda.Interaction.Options
optGHCiInteraction	Agda.Interaction.Options
optGuardingTypeConstructors	Agda.Interaction.Options
optHTMLDir	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
option	Agda.Utils.Parser.ReadP
optional	Agda.Utils.Parser.ReadP
optionError	Agda.Main
Options	Agda.Interaction.Options
optionsOnReload	Agda.Interaction.InteractionTop
OptionsPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Interaction.Options
3 (Data Constructor)	Agda.Syntax.Abstract
optIrrelevantProjections	Agda.Interaction.Options
optJSCompile	Agda.Interaction.Options
optLaTeXDir	Agda.Interaction.Options
optLibraries	Agda.Interaction.Options
OptM	Agda.Interaction.Options
optOptimSmashing	Agda.Interaction.Options
optOverrideLibrariesFile	Agda.Interaction.Options
optPatternMatching	Agda.Interaction.Options
optPostfixProjections	Agda.Interaction.Options
optPragmaOptions	Agda.Interaction.Options
optProgramName	Agda.Interaction.Options
optProofIrrelevance	Agda.Interaction.Options
optRewriting	Agda.Interaction.Options
opts	Agda.Compiler.UHC.FromAgda
optSafe	Agda.Interaction.Options
optSharing	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
optUHCBin	Agda.Interaction.Options
optUHCCallUHC	Agda.Interaction.Options
optUHCCompile	Agda.Interaction.Options
optUHCFlags	Agda.Interaction.Options
optUHCTextualCore	Agda.Interaction.Options
optUHCTraceLevel	Agda.Interaction.Options
optUniverseCheck	Agda.Interaction.Options
optUniversePolymorphism	Agda.Interaction.Options
optUseLibs	Agda.Interaction.Options
optVerbose	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
Origin	Agda.Syntax.Common
origProjection	Agda.TypeChecking.Records
orM	Agda.Utils.Monad
orPO	Agda.Utils.PartialOrd
ostar	Agda.Utils.SemiRing
OtherAspect	Agda.Interaction.Highlighting.Precise
otherAspects	Agda.Interaction.Highlighting.Precise
OtherSize	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
OtherType	Agda.Syntax.Internal
OtherV	Agda.Syntax.Concrete.Operators.Parser
otimes	Agda.Utils.SemiRing
outFile
1 (Function)	Agda.Compiler.JS.Compiler
2 (Function)	Agda.Compiler.MAlonzo.Compiler
outFile'	Agda.Compiler.MAlonzo.Compiler
outFile_
1 (Function)	Agda.Compiler.JS.Compiler
2 (Function)	Agda.Compiler.MAlonzo.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
outputIsInf	Agda.Compiler.Treeless.DelayCoinduction
OutputTypeName
1 (Type/Class)	Agda.TypeChecking.Telescope
2 (Data Constructor)	Agda.TypeChecking.Telescope
OutputTypeNameNotYetKnown	Agda.TypeChecking.Telescope
OutputTypeVar	Agda.TypeChecking.Telescope
over	Agda.Utils.Lens
overlapping
1 (Function)	Agda.Interaction.Highlighting.Range
2 (Function)	Agda.TypeChecking.Coverage.Match
OverlappingProjects	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
OverlappingTokensError	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarning	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
ozero	Agda.Utils.SemiRing