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

- 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
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