O | Agda.TypeChecking.SizedTypes.Syntax |
obj | Agda.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 |
ObjectWithSingleField | Agda.Interaction.JSON |
observeHiding | Agda.Syntax.Concrete |
observeModifiers | Agda.Syntax.Concrete |
observeRelevance | Agda.Syntax.Concrete |
occCxtSize | Agda.TypeChecking.MetaVars.Occurs |
OccEnv | |
1 (Type/Class) | Agda.TypeChecking.Positivity |
2 (Data Constructor) | Agda.TypeChecking.Positivity |
OccM | Agda.TypeChecking.Positivity |
occMeta | Agda.TypeChecking.MetaVars.Occurs |
occUnfold | Agda.TypeChecking.MetaVars.Occurs |
Occurrence | Agda.TypeChecking.Positivity.Occurrence |
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 |
OccursExtra | |
1 (Type/Class) | Agda.TypeChecking.MetaVars.Occurs |
2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
OccursHere | Agda.TypeChecking.Positivity |
OccursHere' | Agda.TypeChecking.Positivity |
occursIn | Agda.Compiler.Treeless.Subst |
OccursM | Agda.TypeChecking.MetaVars.Occurs |
OccursWhere | |
1 (Type/Class) | Agda.TypeChecking.Positivity.Occurrence |
2 (Data Constructor) | Agda.TypeChecking.Positivity.Occurrence |
occurs_ | Agda.TypeChecking.MetaVars.Occurs |
occVars | Agda.TypeChecking.MetaVars.Occurs |
ofExpr | Agda.Interaction.Base |
Offset | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
3 (Data Constructor) | Agda.TypeChecking.SizedTypes.WarshallSolver |
offset | Agda.TypeChecking.SizedTypes.Syntax |
offsideRule | Agda.Syntax.Parser.Layout |
ofName | Agda.Interaction.Base |
OfType | Agda.Interaction.Base |
OfType' | Agda.Interaction.Base |
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.Base |
oldInteractionScopes | Agda.Interaction.Base |
OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract |
oldOptionName | Agda.Interaction.Options |
OldQName | Agda.Syntax.Translation.ConcreteToAbstract |
OldSizeConstraint | Agda.TypeChecking.SizedTypes |
OldSizeExpr | Agda.TypeChecking.SizedTypes |
oldSizeExpr | Agda.TypeChecking.SizedTypes |
omegaFlexRig | Agda.TypeChecking.Free.Lazy |
omitField | Agda.Interaction.JSON |
omitField1 | Agda.Interaction.JSON |
omitField2 | Agda.Interaction.JSON |
omitNothingFields | Agda.Interaction.JSON |
omittedField | Agda.Interaction.JSON |
omittedField1 | Agda.Interaction.JSON |
omittedField2 | Agda.Interaction.JSON |
on | Agda.Utils.Function |
onBlockingMetasM | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
once | Agda.Compiler.Treeless.Subst |
One | |
1 (Data Constructor) | Agda.Utils.Three |
2 (Type/Class) | Agda.Interaction.JSON |
oneFlexRig | Agda.TypeChecking.Free.Lazy |
oneFreeVariable | Agda.Syntax.Common |
OneHole | Agda.Utils.AffineHole |
OneLineMode | Agda.Syntax.Common.Pretty |
oneVarOcc | Agda.TypeChecking.Free.Lazy |
onLetBindingType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
onlyErased | Agda.Syntax.Parser.Helpers |
OnlyLazy | |
1 (Type/Class) | Agda.TypeChecking.Patterns.Match |
2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
OnlyReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
onlyReduceProjections | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
onlyReduceTypes | 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 |
OpAppArgs | Agda.Syntax.Concrete |
OpAppArgs' | Agda.Syntax.Concrete |
OpAppP | Agda.Syntax.Concrete |
OpAppV | Agda.Syntax.Concrete.Operators.Parser |
Opaque | Agda.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 |
opaqueDecls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
OpaqueDef | Agda.Syntax.Common |
OpaqueId | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
opaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
OpaqueInMutual | Agda.Syntax.Concrete.Definitions.Errors |
opaqueParent | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
opaqueRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
opaqueUnfolding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
opBrackets | Agda.Syntax.Fixity |
opBrackets' | Agda.Syntax.Fixity |
Open | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
open | Agda.TypeChecking.Names |
Opened | Agda.Syntax.Scope.Base |
OpenKind | Agda.Syntax.Scope.Monad |
OpenMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
openMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
openMetasToPostulates | Agda.TypeChecking.MetaVars |
openModule | Agda.Syntax.Scope.Monad |
openModule_ | Agda.Syntax.Scope.Monad |
OpenPublicAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
OpenPublicAbstract_ | Agda.Interaction.Options.Warnings |
OpenPublicPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
OpenPublicPrivate_ | Agda.Interaction.Options.Warnings |
OpenS | Agda.Syntax.Abstract |
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 |
openThingCheckpointMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
openThingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
openVerboseBracket | Agda.TypeChecking.Monad.Debug, 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 |
optAllowExec | Agda.Interaction.Options |
optAllowIncompleteMatch | Agda.Interaction.Options |
optAllowUnsolved | Agda.Interaction.Options |
OptArg | Agda.Interaction.Options |
optAutoInline | Agda.Interaction.Options |
optBacktrackingInstances | Agda.Interaction.Options |
optCaching | Agda.Interaction.Options |
optCallByName | Agda.Interaction.Options |
optCohesion | Agda.Interaction.Options |
optCompileDir | Agda.Interaction.Options |
optCompileNoMain | Agda.Interaction.Options |
optConfluenceCheck | Agda.Interaction.Options |
optCopatterns | Agda.Interaction.Options |
optCountClusters | Agda.Interaction.Options |
optCubical | Agda.Interaction.Options |
optCubicalCompatible | Agda.Interaction.Options |
optCumulativity | Agda.Interaction.Options |
optDefaultLibs | Agda.Interaction.Options |
OptDescr | Agda.Interaction.Options |
optDiagnosticsColour | Agda.Interaction.Options |
optDoubleCheck | Agda.Interaction.Options |
optErasedMatches | Agda.Interaction.Options |
optEraseRecordParameters | Agda.Interaction.Options |
optErasure | Agda.Interaction.Options |
optEta | Agda.Interaction.Options |
optExitOnError | Agda.Interaction.Options |
optExperimentalIrrelevance | Agda.Interaction.Options |
optExplicitHints | Agda.Mimer.Options |
optFastReduce | Agda.Interaction.Options |
optFirstOrder | Agda.Interaction.Options |
optFlatSplit | Agda.Interaction.Options |
optForcedArgumentRecursion | Agda.Interaction.Options |
optForcing | Agda.Interaction.Options |
optGenerateVimFile | Agda.Interaction.Options |
optGhcBin | Agda.Compiler.MAlonzo.Misc |
optGhcCallGhc | Agda.Compiler.MAlonzo.Misc |
optGhcCompileDir | Agda.Compiler.MAlonzo.Misc |
optGhcFlags | Agda.Compiler.MAlonzo.Misc |
optGHCiInteraction | Agda.Interaction.Options |
optGhcStrict | Agda.Compiler.MAlonzo.Misc |
optGhcStrictData | Agda.Compiler.MAlonzo.Misc |
optGuarded | Agda.Interaction.Options |
optGuardedness | Agda.Interaction.Options |
optHiddenArgumentPuns | Agda.Interaction.Options |
optHintMode | Agda.Mimer.Options |
optIgnoreAllInterfaces | Agda.Interaction.Options |
optIgnoreInterfaces | Agda.Interaction.Options |
optImportSorts | Agda.Interaction.Options |
optIncludePaths | Agda.Interaction.Options |
optInferAbsurdClauses | 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 |
OptionError | Agda.Interaction.ExitCode |
optionError | Agda.Main |
OptionRenamed | Agda.Interaction.Options |
OptionRenamed_ | Agda.Interaction.Options.Warnings |
Options | |
1 (Data Constructor) | Agda.Interaction.Options |
2 (Type/Class) | Agda.Interaction.JSON |
3 (Type/Class) | Agda.Mimer.Options |
4 (Data Constructor) | Agda.Mimer.Options |
options | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
optionsOnReload | Agda.Interaction.Base |
OptionsPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
3 (Data Constructor) | Agda.Interaction.Library.Base, Agda.Interaction.Library |
4 (Data Constructor) | Agda.Syntax.Abstract |
OptionWarning | |
1 (Type/Class) | Agda.Interaction.Options |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
optionWarningName | Agda.Interaction.Options |
optIrrelevantProjections | Agda.Interaction.Options |
optJSCompile | Agda.Compiler.JS.Compiler |
optJSMinify | Agda.Compiler.JS.Compiler |
optJSModuleStyle | Agda.Compiler.JS.Compiler |
optJSONInteraction | Agda.Interaction.Options |
optJSOptimize | Agda.Compiler.JS.Compiler |
optJSVerify | Agda.Compiler.JS.Compiler |
optKeepCoveringClauses | Agda.Interaction.Options |
optKeepPatternVariables | Agda.Interaction.Options |
optLargeIndices | Agda.Interaction.Options |
optLevelUniverse | Agda.Interaction.Options |
optLibraries | Agda.Interaction.Options |
optList | Agda.Mimer.Options |
optLoadPrimitives | Agda.Interaction.Options |
optLocalInterfaces | Agda.Interaction.Options |
OptM | Agda.Interaction.Options |
optOmegaInOmega | Agda.Interaction.Options |
optOnlyScopeChecking | Agda.Interaction.Options |
optOverrideLibrariesFile | Agda.Interaction.Options |
optPatternMatching | Agda.Interaction.Options |
optPositivityCheck | Agda.Interaction.Options |
optPostfixProjections | Agda.Interaction.Options |
optPragmaOptions | Agda.Interaction.Options |
optPrintAgdaAppDir | Agda.Interaction.Options |
optPrintAgdaDataDir | Agda.Interaction.Options |
optPrintHelp | Agda.Interaction.Options |
optPrintPatternSynonyms | Agda.Interaction.Options |
optPrintVersion | Agda.Interaction.Options |
optProfiling | Agda.Interaction.Options |
optProgramName | Agda.Interaction.Options |
optProjectionLike | Agda.Interaction.Options |
optProp | Agda.Interaction.Options |
optQualifiedInstances | Agda.Interaction.Options |
optRequireUniqueMetaSolutions | Agda.Interaction.Options |
optRewriting | Agda.Interaction.Options |
optSafe | Agda.Interaction.Options |
optSaveMetas | Agda.Interaction.Options |
optShowGeneralized | Agda.Interaction.Options |
optShowIdentitySubstitutions | Agda.Interaction.Options |
optShowImplicit | Agda.Interaction.Options |
optShowIrrelevant | Agda.Interaction.Options |
optSizedTypes | Agda.Interaction.Options |
optSkip | Agda.Mimer.Options |
optSyntacticEquality | Agda.Interaction.Options |
optTerminationCheck | Agda.Interaction.Options |
optTerminationDepth | Agda.Interaction.Options |
optTimeout | Agda.Mimer.Options |
optTraceImports | Agda.Interaction.Options |
optTransliterate | Agda.Interaction.Options |
optTrustedExecutables | Agda.Interaction.Options |
optTwoLevel | 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 |
or2M | Agda.Utils.Monad |
Order | Agda.Termination.Order |
OrderCandidates | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
orderFields | Agda.TypeChecking.Records |
orderFieldsFail | Agda.TypeChecking.Records |
orderFieldsWarn | 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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
otherAspects | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
OtherBackend | Agda.Interaction.Base |
OtherDefName | Agda.Syntax.Scope.Base |
OtherFlex | Agda.TypeChecking.Rules.LHS.Problem |
otherPatterns | 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 |
otherValue | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
otimes | Agda.Utils.SemiRing |
OType | Agda.Syntax.Internal |
outFile | Agda.Compiler.JS.Compiler |
outFile_ | Agda.Compiler.JS.Compiler |
outgoing | Agda.TypeChecking.SizedTypes.WarshallSolver |
OutputConstraint | Agda.Interaction.Output |
OutputConstraint' | Agda.Interaction.Base |
OutputConstraint_boot | Agda.Interaction.Base |
OutputContextEntry | Agda.Interaction.Base |
OutputForm | |
1 (Data Constructor) | Agda.Interaction.Base |
2 (Type/Class) | Agda.Interaction.Output |
outputFormId | Agda.Interaction.BasicOps |
OutputForm_boot | Agda.Interaction.Base |
OutputTypeName | |
1 (Type/Class) | Agda.TypeChecking.InstanceArguments |
2 (Data Constructor) | Agda.TypeChecking.InstanceArguments |
OutputTypeNameNotYetKnown | Agda.TypeChecking.InstanceArguments |
OutputTypeVar | Agda.TypeChecking.InstanceArguments |
OutputTypeVisiblePi | Agda.TypeChecking.InstanceArguments |
outsideLocalVars | Agda.Syntax.Scope.Monad |
over | Agda.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 |
overCallSites | Agda.Utils.CallStack |
OverlapMode | Agda.Syntax.Common |
Overlappable | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Common |
Overlapping | Agda.Syntax.Common |
overlapping | Agda.Interaction.Highlighting.Range |
OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
overlappings | Agda.Interaction.Highlighting.Range |
OverlappingTokensError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
OverlappingTokensWarning | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
OverlappingTokensWarning_ | Agda.Interaction.Options.Warnings |
OverlapPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Overlaps | Agda.Syntax.Common |
ozero | Agda.Utils.SemiRing |