| D | Agda.Auto.Options |
| DAG | |
| 1 (Type/Class) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Data Constructor) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| dagComponentMap | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| dagGraph | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| dagInvariant | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| dagNodeMap | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| Data | Agda.Syntax.Concrete |
| dataAbstr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataBlock | Agda.Syntax.Concrete.Definitions.Types |
| dataClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataCon | Agda.TypeChecking.Datatypes |
| dataCons | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataConstructor | Agda.Syntax.Reflected |
| DataDecl | Agda.Utils.Haskell.Syntax |
| DataDef | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| dataDefGeneralizedParams | Agda.Syntax.Abstract |
| DataDefParams | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| dataDefParams | Agda.Syntax.Abstract |
| dataIxs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dataMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataName | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base |
| DataOrNew | Agda.Utils.Haskell.Syntax |
| DataOrRecord | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.TypeChecking.Rules.LHS |
| DataOrRecordModule | Agda.Syntax.Scope.Base |
| DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dataPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dataPathCons | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataRecOrFun | Agda.Syntax.Concrete.Definitions.Types |
| datarecPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataSig | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| dataSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DataType | Agda.Utils.Haskell.Syntax |
| Datatype | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dbPatPerm | Agda.Syntax.Internal.Pattern |
| dbPatPerm' | Agda.Syntax.Internal.Pattern |
| DBPatVar | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| dbPatVarIndex | Agda.Syntax.Internal |
| dbPatVarName | Agda.Syntax.Internal |
| dbraces | |
| 1 (Function) | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| DBSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
| DCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DDot | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| Deadcode | Agda.Interaction.Highlighting.Precise |
| deadStandardOptions | Agda.Interaction.Options |
| DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
| DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| debruijnNamedVar | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
| DeBruijnPattern | Agda.Syntax.Internal |
| deBruijnVar | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
| deBruijnView | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
| debug | Agda.TypeChecking.SizedTypes.Utils |
| debugConstraints | Agda.TypeChecking.Constraints |
| debugPrintDecl | Agda.TypeChecking.Rules.Decl |
| Decl | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Declaration | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| DeclarationException | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| declarationException | Agda.Syntax.Concrete.Definitions.Monad |
| DeclarationException' | Agda.Syntax.Concrete.Definitions.Errors |
| DeclarationPanic | Agda.Syntax.Concrete.Definitions.Errors |
| DeclarationWarning | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| declarationWarning | Agda.Syntax.Concrete.Definitions.Monad |
| DeclarationWarning' | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| declarationWarning' | Agda.Syntax.Concrete.Definitions.Monad |
| declarationWarningName | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| declarationWarningName' | Agda.Syntax.Concrete.Definitions.Errors |
| DeclaredNames | Agda.Syntax.Abstract.Views |
| declaredNames | Agda.Syntax.Abstract.Views |
| DeclCont | Agda.Auto.Syntax |
| DeclInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| declName | |
| 1 (Function) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Function) | Agda.Syntax.Info |
| DeclNum | Agda.Syntax.Concrete.Definitions.Types |
| declRange | Agda.Syntax.Info |
| decode | |
| 1 (Function) | Agda.Interaction.JSON |
| 2 (Function) | Agda.TypeChecking.Serialise |
| decode' | Agda.Interaction.JSON |
| DecodedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| decodeFile | Agda.TypeChecking.Serialise |
| decodeFileStrict | Agda.Interaction.JSON |
| decodeFileStrict' | Agda.Interaction.JSON |
| decodeHashes | Agda.TypeChecking.Serialise |
| decodeInterface | Agda.TypeChecking.Serialise |
| decodeStrict | Agda.Interaction.JSON |
| decodeStrict' | Agda.Interaction.JSON |
| decomposeInterval | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| decomposeInterval' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Decoration | Agda.Utils.Functor |
| Decr | Agda.Termination.Order |
| decr | Agda.Termination.Order |
| decrease | Agda.Termination.Order |
| decreasing | Agda.Termination.Order |
| deepEtaExpand | Agda.TypeChecking.EtaExpand |
| DeepSizeView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| deepSizeView | Agda.TypeChecking.SizedTypes |
| deepUnscope | Agda.Syntax.Abstract.Views |
| deepUnscopeDecl | Agda.Syntax.Abstract.Views |
| deepUnscopeDecls | Agda.Syntax.Abstract.Views |
| deException | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| Def | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| Def' | Agda.Syntax.Abstract |
| defAbstract | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defAccess | Agda.Syntax.Info |
| defApp | Agda.TypeChecking.Substitute |
| DefArg | Agda.TypeChecking.Positivity.Occurrence |
| defArgGeneralizable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defArgInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defArgs | Agda.TypeChecking.MetaVars.Occurs |
| Default | Agda.Utils.WithDefault |
| defaultAction | Agda.TypeChecking.CheckInternal |
| defaultAddCtx | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| defaultAddLetBinding' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| defaultAnnotation | Agda.Syntax.Common |
| defaultAppInfo | Agda.Syntax.Info |
| defaultAppInfo_ | Agda.Syntax.Info |
| defaultArg | Agda.Syntax.Common |
| defaultArgDom | Agda.Syntax.Internal |
| defaultArgInfo | Agda.Syntax.Common |
| defaultAxiom | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultCohesion | Agda.Syntax.Common |
| DefaultCompute | Agda.Interaction.Base |
| defaultCutOff | Agda.Termination.CutOff, Agda.Interaction.Options |
| defaultDefn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultDom | Agda.Syntax.Internal |
| defaultErased | Agda.Syntax.Common |
| defaultFixity | Agda.Syntax.Common |
| defaultGetConstInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| defaultGetRewriteRulesFor | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| defaultGetVerbosity | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultGHCFlags | Agda.Compiler.MAlonzo.Compiler |
| defaultImportDir | Agda.Syntax.Common |
| defaultInteractionOptions | Agda.Interaction.Options |
| defaultInteractionOutputCallback | Agda.Interaction.Response |
| defaultInteractor | Agda.Main |
| defaultIsDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultJSONKeyOptions | Agda.Interaction.JSON |
| defaultJSOptions | Agda.Compiler.JS.Compiler |
| defaultLevelsToZero | Agda.TypeChecking.Level.Solve |
| defaultLock | Agda.Syntax.Common |
| defaultModality | Agda.Syntax.Common |
| defaultNamedArg | Agda.Syntax.Common |
| defaultNamedArgDom | Agda.Syntax.Internal |
| defaultNowDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultOpenLevelsToZero | Agda.TypeChecking.Level.Solve |
| defaultOptions | |
| 1 (Function) | Agda.Interaction.Options |
| 2 (Function) | Agda.Interaction.JSON |
| defaultParseFlags | Agda.Syntax.Parser.Monad |
| defaultPatternInfo | Agda.Syntax.Internal |
| defaultPragmaOptions | Agda.Interaction.Options |
| DefaultProjectConfig | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| defaultQuantity | Agda.Syntax.Common |
| defaultRelevance | Agda.Syntax.Common |
| defaultTaggedObject | Agda.Interaction.JSON |
| defaultTerEnv | Agda.Termination.Monad |
| DefaultToInfty | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| 2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve |
| defaultUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defaultVerbosity | Agda.Interaction.Options |
| defaultWarningMode | Agda.Interaction.Options.Warnings |
| defaultWarningSet | Agda.Interaction.Options.Warnings |
| defBlocked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defClauses | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defCompiled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defCompilerPragmas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defConstructors | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defCopy | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defDelayed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defDisplay | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defFixity | Agda.Syntax.Info |
| defForced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defGeneralizedParams | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defineCompData | Agda.TypeChecking.Rules.Data |
| defineCompKitR | Agda.TypeChecking.Rules.Record |
| Defined | Agda.Syntax.Scope.Base |
| DefinedName | Agda.Syntax.Scope.Base |
| defineHCompForFields | Agda.TypeChecking.Rules.Data |
| defineProjections | Agda.TypeChecking.Rules.Data |
| defineTranspForFields | Agda.TypeChecking.Rules.Data |
| defineTranspOrHCompForFields | Agda.TypeChecking.Rules.Data |
| defineTranspOrHCompR | Agda.TypeChecking.Rules.Record |
| DefInfo | |
| 1 (Data Constructor) | Agda.Syntax.Info |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| defInfo | Agda.Syntax.Info |
| DefInfo' | Agda.Syntax.Info |
| definitelyNonRecursive_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| Definition | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Type/Class) | Agda.Syntax.Reflected |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| definition | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| definition' | Agda.Compiler.JS.Compiler |
| definitionCheck | Agda.TypeChecking.MetaVars.Occurs |
| DefinitionIsErased | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Definitions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DefinitionSite | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| definitionSite | Agda.Interaction.Highlighting.Precise |
| defInjective | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defInstance | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defInverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defIsRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defJSDef | Agda.Compiler.JS.Compiler |
| defLanguage | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defMacro | Agda.Syntax.Info |
| defMatchable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Defn | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defn | Agda.Compiler.JS.Syntax |
| defName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs |
| defNoCompilation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DefNode | Agda.TypeChecking.Positivity |
| defNonterminating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defOrVar | Agda.TypeChecking.Rules.Term |
| DefP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| defParameters | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defPolarity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DefS | Agda.Syntax.Internal |
| defSiteAnchor | Agda.Interaction.Highlighting.Precise |
| defSiteHere | Agda.Interaction.Highlighting.Precise |
| defSiteModule | Agda.Interaction.Highlighting.Precise |
| defSitePos | Agda.Interaction.Highlighting.Precise |
| defTactic | Agda.Syntax.Info |
| defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| defType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Delayed | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| DelayedMerge | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| delayedMergeInvariant | Agda.Interaction.Highlighting.Precise |
| delete | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.SmallSet |
| 3 (Function) | Agda.Utils.Trie |
| 4 (Function) | Agda.Utils.AssocList |
| delimiter | Agda.Utils.String |
| deLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| dependencySortMetas | Agda.TypeChecking.MetaVars |
| DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DeprecationWarning_ | Agda.Interaction.Options.Warnings |
| depthofvar | Agda.Auto.CaseSplit |
| derefPtr | Agda.Utils.Pointer |
| Deriving | Agda.Utils.Haskell.Syntax |
| Deserialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| dest | Agda.TypeChecking.SizedTypes.WarshallSolver |
| desugarDoNotation | Agda.Syntax.DoNotation |
| detecteliminand | Agda.Auto.Syntax |
| detectIdentityFunctions | Agda.Compiler.Treeless.Identity |
| detectsemiflex | Agda.Auto.Syntax |
| dfPats | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dfPatternVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dfRHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dget | Agda.Utils.Functor |
| Diagonal | Agda.Termination.SparseMatrix |
| diagonal | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.Termination.SparseMatrix |
| Dict | |
| 1 (Type/Class) | Agda.TypeChecking.Serialise.Base |
| 2 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
| didYouMean | Agda.TypeChecking.Pretty.Warning |
| difference | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.IntSet.Infinite |
| 3 (Function) | Agda.Utils.SmallSet |
| Dioid | Agda.TypeChecking.SizedTypes.Utils |
| Direct | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DirEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DirGeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DirLeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dirToCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Dirty | |
| 1 (Type/Class) | Agda.TypeChecking.Unquote |
| 2 (Data Constructor) | Agda.TypeChecking.Unquote |
| dirty | Agda.Utils.Update |
| disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DisallowedGeneralizeName | Agda.Syntax.Scope.Base |
| disallowGeneralizedVars | Agda.Syntax.Scope.Base |
| DisambiguatedName | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| disambiguateRecordFields | Agda.Interaction.Highlighting.Generate |
| discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| Display | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| displayDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DisplayForm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| displayForm | Agda.TypeChecking.DisplayForm |
| DisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DisplayInfo | Agda.Interaction.Response |
| DisplayPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| displayRunningInfo | Agda.Interaction.EmacsCommand |
| displayStatus | Agda.Interaction.InteractionTop |
| DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| display_info | Agda.Interaction.InteractionTop |
| display_info' | Agda.Interaction.EmacsCommand |
| distinct | Agda.Utils.List |
| distributeF | Agda.Utils.Functor |
| dmap | Agda.Utils.Functor |
| dname | Agda.Compiler.MAlonzo.Misc |
| DoBind | Agda.Syntax.Concrete |
| DoBlock | Agda.Syntax.Concrete |
| Doc | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.Compiler.JS.Pretty |
| 3 (Data Constructor) | Agda.Compiler.JS.Pretty |
| 4 (Type/Class) | Agda.TypeChecking.Pretty |
| doc | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| doclos | Agda.Auto.Syntax |
| doCompile | Agda.Compiler.Common |
| doCompile' | Agda.Compiler.Common |
| DocP | Agda.Utils.Parser.MemoisedCPS |
| doDef | Agda.Syntax.Internal.Defs |
| DoDrop | Agda.Utils.Permutation |
| doDrop | Agda.Utils.Permutation |
| doesFileExistCaseSensitive | Agda.Utils.FileName |
| DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| doExpandLast | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| DoGeneralize | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DoHComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| DoHighlightModuleContents | Agda.TypeChecking.Rules.Decl |
| DoLet | Agda.Syntax.Concrete |
| Dom | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| Dom' | Agda.Syntax.Internal |
| DomainFree | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| domainFree | Agda.TypeChecking.Rules.Term |
| DomainFull | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Domains | Agda.Utils.TypeLevel |
| Domains' | Agda.Utils.TypeLevel |
| doMeta | Agda.Syntax.Internal.Defs |
| domFinite | Agda.Syntax.Internal |
| domFromArg | Agda.Syntax.Internal |
| domFromNamedArg | Agda.Syntax.Internal |
| domFromNamedArgName | Agda.TypeChecking.Substitute |
| domH | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| dominated | Agda.Utils.Favorites |
| Dominates | Agda.Utils.Favorites |
| dominator | Agda.Utils.Favorites |
| domInfo | Agda.Syntax.Internal |
| domN | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| domName | Agda.Syntax.Internal |
| domOfBV | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| domTactic | Agda.Syntax.Internal |
| Done | |
| 1 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Agda.Interaction.Base |
| DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser |
| dontAssignMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| DontCare | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| dontCare | |
| 1 (Function) | Agda.Auto.Syntax |
| 2 (Function) | Agda.Syntax.Internal |
| DontCutOff | Agda.Termination.CutOff |
| DontDefaultToInfty | Agda.TypeChecking.SizedTypes.Solve |
| DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dontExpandLast | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl |
| DontKnow | Agda.TypeChecking.Patterns.Match |
| DontOpen | Agda.Syntax.Concrete |
| DontReduceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile |
| DontWakeUp | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| DoOpen | Agda.Syntax.Concrete |
| DoQuoteTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| doQuoteTerm | Agda.TypeChecking.Rules.Term |
| DoStmt | Agda.Syntax.Concrete |
| Dot | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| dotBackend | Agda.Interaction.Highlighting.Dot |
| DotFlex | Agda.TypeChecking.Rules.LHS.Problem |
| DoThen | Agda.Syntax.Concrete |
| DOtherSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| DotNetTime | |
| 1 (Type/Class) | Agda.Interaction.JSON |
| 2 (Data Constructor) | Agda.Interaction.JSON |
| DotP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| dotP | Agda.Syntax.Internal |
| DotPattern | Agda.TypeChecking.Rules.LHS.Problem |
| DotPatternCtx | Agda.Syntax.Fixity |
| dotPatterns | Agda.TypeChecking.Rules.LHS.Problem |
| dotPatternsToPatterns | Agda.TypeChecking.Patterns.Internal |
| DoTransp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| DottedPattern | Agda.Interaction.Highlighting.Precise |
| Double | Agda.Compiler.JS.Syntax |
| double | Agda.Utils.Pretty |
| doubleACos | Agda.Utils.Float |
| doubleACosh | Agda.Utils.Float |
| doubleASin | Agda.Utils.Float |
| doubleASinh | Agda.Utils.Float |
| doubleATan | Agda.Utils.Float |
| doubleATan2 | Agda.Utils.Float |
| doubleATanh | Agda.Utils.Float |
| doubleblock | Agda.Auto.NarrowingSearch |
| doubleC | Agda.TypeChecking.Serialise.Base |
| doubleCeiling | Agda.Utils.Float |
| doubleCos | Agda.Utils.Float |
| doubleCosh | Agda.Utils.Float |
| doubleD | Agda.TypeChecking.Serialise.Base |
| doubleDecode | Agda.Utils.Float |
| doubleDenotEq | Agda.Utils.Float |
| doubleDenotOrd | Agda.Utils.Float |
| doubleDiv | Agda.Utils.Float |
| DoubleDot | Agda.Syntax.Concrete |
| doubleE | Agda.TypeChecking.Serialise.Base |
| doubleEncode | Agda.Utils.Float |
| doubleEq | Agda.Utils.Float |
| doubleExp | Agda.Utils.Float |
| doubleFloor | Agda.Utils.Float |
| doubleLe | Agda.Utils.Float |
| doubleLog | Agda.Utils.Float |
| doubleLt | Agda.Utils.Float |
| doubleMinus | Agda.Utils.Float |
| doubleNegate | Agda.Utils.Float |
| doublePlus | Agda.Utils.Float |
| doublePow | Agda.Utils.Float |
| doubleQuotes | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| doubleRound | Agda.Utils.Float |
| doubleSin | Agda.Utils.Float |
| doubleSinh | Agda.Utils.Float |
| doubleSqrt | Agda.Utils.Float |
| doubleTan | Agda.Utils.Float |
| doubleTanh | Agda.Utils.Float |
| doubleTimes | Agda.Utils.Float |
| doubleToRatio | Agda.Utils.Float |
| doubleToWord64 | Agda.Utils.Float |
| DoWarn | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Fixity |
| downFrom | Agda.Utils.List |
| Drop | |
| 1 (Type/Class) | Agda.Utils.Permutation |
| 2 (Data Constructor) | Agda.Utils.Permutation |
| drop | Agda.Utils.List1 |
| DropArgs | Agda.TypeChecking.DropArgs |
| dropArgs | Agda.TypeChecking.DropArgs |
| dropCommon | Agda.Utils.List |
| dropConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| dropDecodedModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| dropEnd | Agda.Utils.List |
| dropFrom | Agda.Utils.Permutation |
| drophid | Agda.Auto.CaseSplit |
| dropMore | Agda.Utils.Permutation |
| dropN | Agda.Utils.Permutation |
| dropParameters | Agda.TypeChecking.ReconstructParameters |
| droppedP | Agda.Utils.Permutation |
| droppedPars | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| dropS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| dropTopLevelModule | Agda.TypeChecking.Errors |
| dropTypeAndModality | Agda.Syntax.Concrete |
| dropWhile | Agda.Utils.List1 |
| dropWhileEndM | Agda.Utils.Monad |
| dropWhileM | Agda.Utils.Monad |
| dryInstantiate | Agda.Auto.NarrowingSearch |
| DSizeInf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| DSizeMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| DSizeVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| DTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Dummy | Agda.Syntax.Internal |
| dummyDom | Agda.Syntax.Internal |
| dummyLevel | Agda.Syntax.Internal |
| dummyLocName | Agda.Syntax.Internal |
| DummyS | Agda.Syntax.Internal |
| dummySort | Agda.Syntax.Internal |
| dummyTerm | Agda.Syntax.Internal |
| DummyTermKind | Agda.Syntax.Internal |
| dummyTermWith | Agda.Syntax.Internal |
| dummyType | Agda.Syntax.Internal |
| duname | Agda.Compiler.MAlonzo.Misc |
| DuplicateAnonDeclaration | Agda.Syntax.Concrete.Definitions.Errors |
| DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicateDefinition | Agda.Syntax.Concrete.Definitions.Errors |
| DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicateFieldsWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicateFieldsWarning_ | Agda.Interaction.Options.Warnings |
| DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicatePrimitiveBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| duplicates | Agda.Utils.List |
| DuplicateUsing | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| DuplicateUsing_ | Agda.Interaction.Options.Warnings |
| DWithApp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| dwLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| dwWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |