Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant

Index - O

O 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class)Agda.Auto.Convert
objAgda.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
ObjectWithSingleFieldAgda.Interaction.JSON
observeHidingAgda.Syntax.Concrete
observeModifiersAgda.Syntax.Concrete
observeRelevanceAgda.Syntax.Concrete
occCxtSizeAgda.TypeChecking.MetaVars.Occurs
OccEnv 
1 (Type/Class)Agda.TypeChecking.Positivity
2 (Data Constructor)Agda.TypeChecking.Positivity
OccMAgda.TypeChecking.Positivity
occMetaAgda.TypeChecking.MetaVars.Occurs
occUnfoldAgda.TypeChecking.MetaVars.Occurs
OccurrenceAgda.TypeChecking.Positivity.Occurrence
OccurrencesAgda.TypeChecking.Positivity
occurrencesAgda.TypeChecking.Positivity
OccurrencesBuilderAgda.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
occursAgda.TypeChecking.MetaVars.Occurs
OccursAsAgda.TypeChecking.Positivity
OccursAs'Agda.TypeChecking.Positivity
OccursCheckAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
occursCheckAgda.TypeChecking.MetaVars.Occurs
OccursCtxAgda.TypeChecking.MetaVars.Occurs
OccursExtra 
1 (Type/Class)Agda.TypeChecking.MetaVars.Occurs
2 (Data Constructor)Agda.TypeChecking.MetaVars.Occurs
OccursHereAgda.TypeChecking.Positivity
OccursHere'Agda.TypeChecking.Positivity
occursInAgda.Compiler.Treeless.Subst
OccursMAgda.TypeChecking.MetaVars.Occurs
OccursWhere 
1 (Type/Class)Agda.TypeChecking.Positivity.Occurrence
2 (Data Constructor)Agda.TypeChecking.Positivity.Occurrence
occurs_Agda.TypeChecking.MetaVars.Occurs
occVarsAgda.TypeChecking.MetaVars.Occurs
ofExprAgda.Interaction.Base
Offset 
1 (Type/Class)Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
3 (Data Constructor)Agda.TypeChecking.SizedTypes.WarshallSolver
offsetAgda.TypeChecking.SizedTypes.Syntax
offsideRuleAgda.Syntax.Parser.Layout
ofNameAgda.Interaction.Base
OfTypeAgda.Interaction.Base
OfType'Agda.Interaction.Base
OKAgda.Auto.NarrowingSearch
OKHandleAgda.Auto.NarrowingSearch
OKMetaAgda.Auto.NarrowingSearch
OKVal 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
OldBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OldBuiltin_Agda.Interaction.Options.Warnings
oldCanonicalizeSizeConstraintAgda.TypeChecking.SizedTypes
oldComputeSizeConstraintAgda.TypeChecking.SizedTypes
oldComputeSizeConstraintsAgda.TypeChecking.SizedTypes
OldInteractionScopesAgda.Interaction.Base
oldInteractionScopesAgda.Interaction.Base
OldModuleNameAgda.Syntax.Translation.ConcreteToAbstract
oldOptionNameAgda.Interaction.Options
OldQNameAgda.Syntax.Translation.ConcreteToAbstract
OldSizeConstraintAgda.TypeChecking.SizedTypes
OldSizeExprAgda.TypeChecking.SizedTypes
oldSizeExprAgda.TypeChecking.SizedTypes
omegaFlexRigAgda.TypeChecking.Free.Lazy
omitFieldAgda.Interaction.JSON
omitField1Agda.Interaction.JSON
omitField2Agda.Interaction.JSON
omitNothingFieldsAgda.Interaction.JSON
omittedFieldAgda.Interaction.JSON
omittedField1Agda.Interaction.JSON
omittedField2Agda.Interaction.JSON
onBlockingMetasMAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
onceAgda.Compiler.Treeless.Subst
One 
1 (Data Constructor)Agda.Utils.Three
2 (Type/Class)Agda.Interaction.JSON
oneFlexRigAgda.TypeChecking.Free.Lazy
oneFreeVariableAgda.Syntax.Common
OneHoleAgda.Utils.AffineHole
OneLineModeAgda.Syntax.Common.Pretty
oneVarOccAgda.TypeChecking.Free.Lazy
onLetBindingTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OnlyReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyReduceProjectionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyReduceTypesAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
onlyShowIfUnsolvedAgda.TypeChecking.Warnings
OnlyVarsUpToAgda.TypeChecking.Positivity
onReduceEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ooneAgda.Utils.SemiRing
OpAgda.TypeChecking.Primitive
OpApp 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Concrete
OpAppArgsAgda.Syntax.Concrete
OpAppArgs'Agda.Syntax.Concrete
OpAppPAgda.Syntax.Concrete
OpAppVAgda.Syntax.Concrete.Operators.Parser
OpaqueAgda.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
opaqueDeclsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpaqueDefAgda.Syntax.Common
OpaqueId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
opaqueIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpaqueInMutualAgda.Syntax.Concrete.Definitions.Errors
opaqueParentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opaqueRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opaqueUnfoldingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
opBracketsAgda.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
openAgda.TypeChecking.Names
OpenedAgda.Syntax.Scope.Base
OpenInstanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpenKindAgda.Syntax.Scope.Monad
openMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openMetasToPostulatesAgda.TypeChecking.MetaVars
openModuleAgda.Syntax.Scope.Monad
openModule_Agda.Syntax.Scope.Monad
OpenPublicAbstractAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
OpenPublicAbstract_Agda.Interaction.Options.Warnings
OpenPublicPrivateAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
OpenPublicPrivate_Agda.Interaction.Options.Warnings
OpenSAgda.Syntax.Abstract
OpenShortHandAgda.Syntax.Concrete
OpenThingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingCheckpointAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingCheckpointMapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openThingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
openVerboseBracketAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OperatorInformationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OperatorsExprAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
OperatorsPatternAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
OperatorTypeAgda.Syntax.Concrete.Operators.Parser
oplusAgda.Utils.SemiRing
opPAgda.Syntax.Concrete.Operators.Parser
oppositeDAGAgda.Utils.Graph.AdjacencyMap.Unidirectional
oppPOAgda.Utils.PartialOrd
optAbsoluteIncludePathsAgda.Interaction.Options
optAllowExecAgda.Interaction.Options
optAllowIncompleteMatchAgda.Interaction.Options
optAllowUnsolvedAgda.Interaction.Options
OptArgAgda.Interaction.Options
optAutoInlineAgda.Interaction.Options
optCachingAgda.Interaction.Options
optCallByNameAgda.Interaction.Options
optCohesionAgda.Interaction.Options
optCompileDirAgda.Interaction.Options
optCompileNoMainAgda.Interaction.Options
optConfluenceCheckAgda.Interaction.Options
optCopatternsAgda.Interaction.Options
optCountClustersAgda.Interaction.Options
optCubicalAgda.Interaction.Options
optCubicalCompatibleAgda.Interaction.Options
optCumulativityAgda.Interaction.Options
optDefaultLibsAgda.Interaction.Options
OptDescrAgda.Interaction.Options
optDiagnosticsColourAgda.Interaction.Options
optDoubleCheckAgda.Interaction.Options
optErasedMatchesAgda.Interaction.Options
optEraseRecordParametersAgda.Interaction.Options
optErasureAgda.Interaction.Options
optEtaAgda.Interaction.Options
optExitOnErrorAgda.Interaction.Options
optExperimentalIrrelevanceAgda.Interaction.Options
optFastReduceAgda.Interaction.Options
optFirstOrderAgda.Interaction.Options
optFlatSplitAgda.Interaction.Options
optForcedArgumentRecursionAgda.Interaction.Options
optForcingAgda.Interaction.Options
optGenerateVimFileAgda.Interaction.Options
optGhcBinAgda.Compiler.MAlonzo.Misc
optGhcCallGhcAgda.Compiler.MAlonzo.Misc
optGhcCompileDirAgda.Compiler.MAlonzo.Misc
optGhcFlagsAgda.Compiler.MAlonzo.Misc
optGHCiInteractionAgda.Interaction.Options
optGhcStrictAgda.Compiler.MAlonzo.Misc
optGhcStrictDataAgda.Compiler.MAlonzo.Misc
optGuardedAgda.Interaction.Options
optGuardednessAgda.Interaction.Options
optHiddenArgumentPunsAgda.Interaction.Options
optIgnoreAllInterfacesAgda.Interaction.Options
optIgnoreInterfacesAgda.Interaction.Options
optImportSortsAgda.Interaction.Options
optIncludePathsAgda.Interaction.Options
optInferAbsurdClausesAgda.Interaction.Options
optInjectiveTypeConstructorsAgda.Interaction.Options
optInputFileAgda.Interaction.Options
optInstanceSearchDepthAgda.Interaction.Options
optInteractiveAgda.Interaction.Options
optInversionMaxDepthAgda.Interaction.Options
OptionAgda.Interaction.Options
OptionErrorAgda.Interaction.ExitCode
optionErrorAgda.Main
OptionRenamedAgda.Interaction.Options
OptionRenamed_Agda.Interaction.Options.Warnings
Options 
1 (Data Constructor)Agda.Interaction.Options
2 (Type/Class)Agda.Interaction.JSON
optionsAgda.Compiler.Backend
optionsOnReloadAgda.Interaction.Base
OptionsPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Type/Class)Agda.Interaction.Library.Base, Agda.Interaction.Library
4 (Data Constructor)Agda.Interaction.Library.Base, Agda.Interaction.Library
OptionWarning 
1 (Type/Class)Agda.Interaction.Options
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
optionWarningNameAgda.Interaction.Options
optIrrelevantProjectionsAgda.Interaction.Options
optJSCompileAgda.Compiler.JS.Compiler
optJSMinifyAgda.Compiler.JS.Compiler
optJSModuleStyleAgda.Compiler.JS.Compiler
optJSONInteractionAgda.Interaction.Options
optJSOptimizeAgda.Compiler.JS.Compiler
optJSVerifyAgda.Compiler.JS.Compiler
optKeepCoveringClausesAgda.Interaction.Options
optKeepPatternVariablesAgda.Interaction.Options
optLargeIndicesAgda.Interaction.Options
optLevelUniverseAgda.Interaction.Options
optLibrariesAgda.Interaction.Options
optLoadPrimitivesAgda.Interaction.Options
optLocalInterfacesAgda.Interaction.Options
OptMAgda.Interaction.Options
optOmegaInOmegaAgda.Interaction.Options
optOnlyScopeCheckingAgda.Interaction.Options
optOverlappingInstancesAgda.Interaction.Options
optOverrideLibrariesFileAgda.Interaction.Options
optPatternMatchingAgda.Interaction.Options
optPositivityCheckAgda.Interaction.Options
optPostfixProjectionsAgda.Interaction.Options
optPragmaOptionsAgda.Interaction.Options
optPrintAgdaDirAgda.Interaction.Options
optPrintHelpAgda.Interaction.Options
optPrintPatternSynonymsAgda.Interaction.Options
optPrintVersionAgda.Interaction.Options
optProfilingAgda.Interaction.Options
optProgramNameAgda.Interaction.Options
optProjectionLikeAgda.Interaction.Options
optPropAgda.Interaction.Options
optQualifiedInstancesAgda.Interaction.Options
optRewritingAgda.Interaction.Options
optSafeAgda.Interaction.Options
optSaveMetasAgda.Interaction.Options
optShowGeneralizedAgda.Interaction.Options
optShowIdentitySubstitutionsAgda.Interaction.Options
optShowImplicitAgda.Interaction.Options
optShowIrrelevantAgda.Interaction.Options
optSizedTypesAgda.Interaction.Options
optSyntacticEqualityAgda.Interaction.Options
optTerminationCheckAgda.Interaction.Options
optTerminationDepthAgda.Interaction.Options
optTraceImportsAgda.Interaction.Options
optTransliterateAgda.Interaction.Options
optTrustedExecutablesAgda.Interaction.Options
optTwoLevelAgda.Interaction.Options
optUniverseCheckAgda.Interaction.Options
optUniversePolymorphismAgda.Interaction.Options
optUseLibsAgda.Interaction.Options
optUseUnicodeAgda.Interaction.Options
optVerboseAgda.Interaction.Options
optWarningModeAgda.Interaction.Options
optWithoutKAgda.Interaction.Options
OrAgda.Auto.NarrowingSearch
or2MAgda.Utils.Monad
OrderAgda.Termination.Order
orderFieldsAgda.TypeChecking.Records
orderFieldsFailAgda.TypeChecking.Records
orderFieldsWarnAgda.TypeChecking.Records
orderMatAgda.Termination.Order
orderSemiringAgda.Termination.Order
OrdinaryAgda.Syntax.Concrete
orEitherMAgda.Utils.Monad
OrgFileTypeAgda.Syntax.Common
OriginAgda.Syntax.Common
origProjectionAgda.TypeChecking.Records
orMAgda.Utils.Monad
orPOAgda.Utils.PartialOrd
ostarAgda.Utils.SemiRing
OTermAgda.Syntax.Internal
OtherAspectAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
otherAspectsAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
OtherBackendAgda.Interaction.Base
OtherDefNameAgda.Syntax.Scope.Base
OtherFlexAgda.TypeChecking.Rules.LHS.Problem
otherPatternsAgda.TypeChecking.Rules.LHS.Problem
OtherPragmaAgda.Utils.Haskell.Syntax
OtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OtherTypeAgda.Syntax.Internal
OtherVAgda.Syntax.Concrete.Operators.Parser
otherValueAgda.Utils.Graph.AdjacencyMap.Unidirectional
otimesAgda.Utils.SemiRing
OTypeAgda.Syntax.Internal
outFileAgda.Compiler.JS.Compiler
outFile_Agda.Compiler.JS.Compiler
outgoingAgda.TypeChecking.SizedTypes.WarshallSolver
OutputConstraintAgda.Interaction.Base
OutputConstraint'Agda.Interaction.Base
OutputContextEntryAgda.Interaction.Base
OutputForm 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
outputFormIdAgda.Interaction.BasicOps
OutputTypeName 
1 (Type/Class)Agda.TypeChecking.Telescope
2 (Data Constructor)Agda.TypeChecking.Telescope
OutputTypeNameNotYetKnownAgda.TypeChecking.Telescope
OutputTypeVarAgda.TypeChecking.Telescope
OutputTypeVisiblePiAgda.TypeChecking.Telescope
outsideLocalVarsAgda.Syntax.Scope.Monad
overAgda.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
overCallSitesAgda.Utils.CallStack
OverlappableAgda.Syntax.Common
overlappingAgda.Interaction.Highlighting.Range
OverlappingProjectsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
overlappingsAgda.Interaction.Highlighting.Range
OverlappingTokensErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarningAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarning_Agda.Interaction.Options.Warnings
ozeroAgda.Utils.SemiRing