Agda-2.6.1.3: 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
ObjectAgda.Compiler.JS.Syntax
objectAgda.Compiler.JS.Substitution
observeHidingAgda.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
occVarsAgda.TypeChecking.MetaVars.Occurs
ofExprAgda.Interaction.Base
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
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
OldName 
1 (Type/Class)Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor)Agda.Syntax.Translation.ConcreteToAbstract
OldQNameAgda.Syntax.Translation.ConcreteToAbstract
OldSizeConstraintAgda.TypeChecking.SizedTypes
OldSizeExprAgda.TypeChecking.SizedTypes
oldSizeExprAgda.TypeChecking.SizedTypes
oldSolverAgda.TypeChecking.SizedTypes
oldSolveSizeConstraintsAgda.TypeChecking.SizedTypes
omegaFlexRigAgda.TypeChecking.Free.Lazy
onceAgda.Compiler.Treeless.Subst
OneAgda.Utils.Three
oneFlexRigAgda.TypeChecking.Free.Lazy
oneFreeVariableAgda.Syntax.Common
OneHoleAgda.Utils.AffineHole
OneLineModeAgda.Utils.Pretty
oneVarOccAgda.TypeChecking.Free.Lazy
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
OpAppPAgda.Syntax.Concrete
OpAppVAgda.Syntax.Concrete.Operators.Parser
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
openBraceAgda.Syntax.Parser.Layout
OpenedAgda.Syntax.Scope.Base
OpenInstanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OpenKindAgda.Syntax.Scope.Monad
openMetasToPostulatesAgda.TypeChecking.MetaVars
openModuleAgda.Syntax.Scope.Monad
openModule_Agda.Syntax.Scope.Monad
OpenPublicAbstractAgda.Syntax.Concrete.Definitions
OpenPublicAbstract_Agda.Interaction.Options.Warnings
OpenPublicPrivateAgda.Syntax.Concrete.Definitions
OpenPublicPrivate_Agda.Interaction.Options.Warnings
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
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
optAllowIncompleteMatchAgda.Interaction.Options
optAllowUnsolvedAgda.Interaction.Options
OptArgAgda.Interaction.Options
optAutoInlineAgda.Interaction.Options
optCachingAgda.Interaction.Options
optCompareSortsAgda.Interaction.Options
optCompileDirAgda.Interaction.Options
optCompileNoMainAgda.Interaction.Options
optCompletenessCheckAgda.Interaction.Options
optConfluenceCheckAgda.Interaction.Options
optCopatternsAgda.Interaction.Options
optCountClustersAgda.Interaction.Options
optCSSFileAgda.Interaction.Options
optCubicalAgda.Interaction.Options
optCumulativityAgda.Interaction.Options
optDefaultLibsAgda.Interaction.Options
optDependencyGraphAgda.Interaction.Options
OptDescrAgda.Interaction.Options
optDisablePositivityAgda.Interaction.Options
optDoubleCheckAgda.Interaction.Options
optEtaAgda.Interaction.Options
optExactSplitAgda.Interaction.Options
optExperimentalIrrelevanceAgda.Interaction.Options
optFastReduceAgda.Interaction.Options
optFlatSplitAgda.Interaction.Options
optForcingAgda.Interaction.Options
optGenerateHTMLAgda.Interaction.Options
optGenerateLaTeXAgda.Interaction.Options
optGenerateVimFileAgda.Interaction.Options
optGhcCallGhcAgda.Compiler.MAlonzo.Compiler
optGhcCompileAgda.Compiler.MAlonzo.Compiler
optGhcFlagsAgda.Compiler.MAlonzo.Compiler
optGHCiInteractionAgda.Interaction.Options
optGuardednessAgda.Interaction.Options
optHTMLDirAgda.Interaction.Options
optHTMLHighlightAgda.Interaction.Options
optIgnoreAllInterfacesAgda.Interaction.Options
optIgnoreInterfacesAgda.Interaction.Options
optIncludePathsAgda.Interaction.Options
optInjectiveTypeConstructorsAgda.Interaction.Options
optInputFileAgda.Interaction.Options
optInstanceSearchDepthAgda.Interaction.Options
optInteractiveAgda.Interaction.Options
optInversionMaxDepthAgda.Interaction.Options
OptionAgda.Interaction.Options
optionErrorAgda.Main
OptionsAgda.Interaction.Options
optionsAgda.Compiler.Backend
optionsOnReloadAgda.Interaction.Base
OptionsPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Type/Class)Agda.Interaction.Options
optIrrelevantProjectionsAgda.Interaction.Options
optJSCompileAgda.Compiler.JS.Compiler
optJSONInteractionAgda.Interaction.Options
optKeepPatternVariablesAgda.Interaction.Options
optLaTeXDirAgda.Interaction.Options
optLibrariesAgda.Interaction.Options
optLocalInterfacesAgda.Interaction.Options
OptMAgda.Interaction.Options
optOmegaInOmegaAgda.Interaction.Options
optOnlyScopeCheckingAgda.Interaction.Options
optOptimSmashingAgda.Interaction.Options
optOverlappingInstancesAgda.Interaction.Options
optOverrideLibrariesFileAgda.Interaction.Options
optPatternMatchingAgda.Interaction.Options
optPostfixProjectionsAgda.Interaction.Options
optPragmaOptionsAgda.Interaction.Options
optPrintPatternSynonymsAgda.Interaction.Options
optProgramNameAgda.Interaction.Options
optProjectionLikeAgda.Interaction.Options
optPropAgda.Interaction.Options
optRewritingAgda.Interaction.Options
optSafeAgda.Interaction.Options
optShowHelpAgda.Interaction.Options
optShowImplicitAgda.Interaction.Options
optShowIrrelevantAgda.Interaction.Options
optShowVersionAgda.Interaction.Options
optSizedTypesAgda.Interaction.Options
optSubtypingAgda.Interaction.Options
optSyntacticEqualityAgda.Interaction.Options
optTerminationCheckAgda.Interaction.Options
optTerminationDepthAgda.Interaction.Options
optUniverseCheckAgda.Interaction.Options
optUniversePolymorphismAgda.Interaction.Options
optUseLibsAgda.Interaction.Options
optUseUnicodeAgda.Interaction.Options
optVerboseAgda.Interaction.Options
optWarningModeAgda.Interaction.Options
optWithCompilerAgda.Interaction.Options
optWithoutKAgda.Interaction.Options
OrAgda.Auto.NarrowingSearch
or2MAgda.Utils.Monad
OrderAgda.Termination.Order
orderFieldsAgda.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.Interaction.Highlighting.Precise
otherAspectsAgda.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
otimesAgda.Utils.SemiRing
OTypeAgda.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
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
OverlappableAgda.Syntax.Common
overlappingAgda.Interaction.Highlighting.Range
OverlappingProjectsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
OverlappingTokensErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarningAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
OverlappingTokensWarning_Agda.Interaction.Options.Warnings
ozeroAgda.Utils.SemiRing