Index - D
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataCon | Agda.TypeChecking.Datatypes |
| dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataConstructor | Agda.Syntax.Reflected |
| DataDecl | Agda.Utils.Haskell.Syntax |
| DataDef | |
| 1 (Data Constructor) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| dataFormat | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataNonLinPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataOrNew | Agda.Utils.Haskell.Syntax |
| DataOrRecord | Agda.Syntax.Common |
| dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataSig | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| dataSmallPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| DBSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
| DCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DDot | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| deal | Agda.Utils.List |
| DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
| DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| decDigit | Agda.Utils.Char |
| Decl | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Declaration | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| DeclarationException | Agda.Syntax.Concrete.Definitions |
| DeclarationPanic | Agda.Syntax.Concrete.Definitions |
| DeclarationWarning | Agda.Syntax.Concrete.Definitions |
| DeclCont | Agda.Auto.Syntax |
| DeclInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| declName | Agda.Syntax.Info |
| declRange | Agda.Syntax.Info |
| decode | Agda.TypeChecking.Serialise |
| DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| decodeFile | Agda.TypeChecking.Serialise |
| decodeHashes | Agda.TypeChecking.Serialise |
| decodeInterface | Agda.TypeChecking.Serialise |
| decompress | Agda.Interaction.Highlighting.Precise |
| Decoration | Agda.Utils.Functor |
| Decr | Agda.Termination.Order |
| decr | Agda.Termination.Order |
| decrease | Agda.Termination.Order |
| decreasing | Agda.Termination.Order |
| DeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| deepSizeView | Agda.TypeChecking.SizedTypes |
| deepUnscope | Agda.Syntax.Abstract.Views |
| deepUnscopeDecl | Agda.Syntax.Abstract.Views |
| deepUnscopeDecls | Agda.Syntax.Abstract.Views |
| Def | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| defAbstract | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defAccess | Agda.Syntax.Info |
| defApp | Agda.TypeChecking.Substitute |
| DefArg | Agda.TypeChecking.Positivity.Occurrence |
| defArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defArgs | Agda.TypeChecking.MetaVars.Occurs |
| defaultAction | Agda.TypeChecking.CheckInternal |
| defaultArg | Agda.Syntax.Common |
| defaultArgInfo | Agda.Syntax.Common |
| DefaultCompute | Agda.Interaction.BasicOps |
| defaultCSSFile | Agda.Interaction.Highlighting.HTML |
| defaultCutOff | Agda.Interaction.Options |
| defaultDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultDom | Agda.Syntax.Common |
| defaultFixity | Agda.Syntax.Fixity |
| defaultGetConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultGetRewriteRulesFor | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultGHCOptions | Agda.Compiler.MAlonzo.Compiler |
| defaultImportDir | Agda.Syntax.Common |
| defaultInteraction | Agda.Main |
| defaultInteractionOptions | Agda.Interaction.Options |
| defaultInteractionOutputCallback | Agda.Interaction.Response |
| defaultJSOptions | Agda.Compiler.JS.Compiler |
| defaultLamInfo | Agda.Syntax.Info |
| defaultLamInfo_ | Agda.Syntax.Info |
| defaultLibDir | Agda.Interaction.Options |
| defaultModuleParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultNamedArg | Agda.Syntax.Common |
| defaultOptions | Agda.Interaction.Options |
| defaultParseFlags | Agda.Syntax.Parser.Monad |
| defaultPragmaOptions | Agda.Interaction.Options |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultVerbosity | Agda.Interaction.Options |
| defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defCompilerPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defCopy | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defFixity | Agda.Syntax.Info |
| Defined | Agda.Syntax.Scope.Base |
| DefinedName | Agda.Syntax.Scope.Monad |
| DefInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| defInfo | Agda.Syntax.Info |
| definitelyNonRecursive_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Definition | |
| 1 (Type/Class) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| definition | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| definition' | Agda.Compiler.JS.Compiler |
| DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| defInstance | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defJSDef | Agda.Compiler.JS.Compiler |
| defMacro | Agda.Syntax.Info |
| defMatchable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Defn | |
| 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 |
| defn | Agda.Compiler.JS.Syntax |
| DefName | Agda.Syntax.Scope.Base |
| defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs |
| DefNode | Agda.TypeChecking.Positivity |
| defNonterminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defOrVar | Agda.TypeChecking.Rules.Term |
| DefP | Agda.Syntax.Abstract |
| defParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defSiteAnchor | Agda.Interaction.Highlighting.Precise |
| defSiteHere | Agda.Interaction.Highlighting.Precise |
| defSiteModule | Agda.Interaction.Highlighting.Precise |
| defSitePos | Agda.Interaction.Highlighting.Precise |
| defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Delayed | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| delete | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.HashMap |
| 3 (Function) | Agda.Utils.Trie |
| delimiter | Agda.Utils.String |
| dependentPolarity | Agda.TypeChecking.Polarity |
| DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| depthofvar | Agda.Auto.CaseSplit |
| derefPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
| Deriving | Agda.Utils.Haskell.Syntax |
| Deserialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| dest | Agda.TypeChecking.SizedTypes.WarshallSolver |
| detecteliminand | Agda.Auto.Syntax |
| detectIdentityFunctions | Agda.Compiler.Treeless.Identity |
| detectsemiflex | Agda.Auto.Syntax |
| dfFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dfPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dfRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| difference | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.HashMap |
| differenceWith | Agda.Utils.HashMap |
| DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Dioid | Agda.TypeChecking.SizedTypes.Utils |
| Direct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DirEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DirGeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DirLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dirToCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Dirty | |
| 1 (Type/Class) | Agda.TypeChecking.Unquote |
| 2 (Data Constructor) | Agda.TypeChecking.Unquote |
| dirty | Agda.Utils.Update |
| disableDestructiveUpdate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| displayDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| displayForm | Agda.TypeChecking.DisplayForm |
| displayFormArities | Agda.TypeChecking.DisplayForm |
| DisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| display_info | Agda.Interaction.InteractionTop |
| display_info' | Agda.Interaction.EmacsCommand |
| display_warning | Agda.Interaction.EmacsCommand |
| distinct | Agda.Utils.List |
| distributeF | Agda.Utils.Functor |
| DLub | Agda.Syntax.Internal |
| dLub | Agda.TypeChecking.Substitute |
| dmap | Agda.Utils.Functor |
| dname | Agda.Compiler.MAlonzo.Misc |
| Doc | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (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 |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| doExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Dom | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| 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 |
| domFromArg | Agda.Syntax.Common |
| domH | Agda.TypeChecking.Primitive |
| dominated | Agda.Utils.Favorites |
| Dominates | Agda.Utils.Favorites |
| dominator | Agda.Utils.Favorites |
| domInfo | Agda.Syntax.Common |
| domN | Agda.TypeChecking.Primitive |
| Done | |
| 1 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| 2 (Data Constructor) | Agda.Interaction.InteractionTop |
| DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser |
| dontAssignMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| dontDescendInto | Agda.Utils.Geniplate |
| DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DontKnow | |
| 1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify |
| DontOpen | Agda.Syntax.Concrete |
| DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete |
| DoOpen | Agda.Syntax.Concrete |
| Dot | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| DotFlex | Agda.TypeChecking.Rules.LHS.Problem |
| DOtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DotM | Agda.Interaction.Highlighting.Dot |
| DotP | |
| 1 (Data Constructor) | Agda.Syntax.Reflected |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| DotPatternCtx | Agda.Syntax.Fixity |
| DotPatternInst | Agda.TypeChecking.Rules.LHS.Problem |
| dotPatternInst | Agda.TypeChecking.Rules.LHS.Problem |
| dotPatternName | Agda.TypeChecking.Rules.LHS.Problem |
| dotPatternType | Agda.TypeChecking.Rules.LHS.Problem |
| dotPatternUserExpr | Agda.TypeChecking.Rules.LHS.Problem |
| DotState | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Dot |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Dot |
| DottedPattern | Agda.Interaction.Highlighting.Precise |
| dottify | Agda.Interaction.Highlighting.Dot |
| Double | Agda.Compiler.JS.Syntax |
| double | Agda.Utils.Pretty |
| doubleblock | Agda.Auto.NarrowingSearch |
| doubleC | Agda.TypeChecking.Serialise.Base |
| doubleD | Agda.TypeChecking.Serialise.Base |
| doubleE | Agda.TypeChecking.Serialise.Base |
| doubleQuotes | Agda.Utils.Pretty |
| downFrom | Agda.Utils.List |
| DPI | Agda.TypeChecking.Rules.LHS.Problem |
| Drop | |
| 1 (Type/Class) | Agda.Utils.Permutation |
| 2 (Data Constructor) | Agda.Utils.Permutation |
| DropArgs | Agda.TypeChecking.DropArgs |
| dropArgs | Agda.TypeChecking.DropArgs |
| dropCommon | Agda.Utils.List |
| dropConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dropFrom | Agda.Utils.Permutation |
| drophid | Agda.Auto.CaseSplit |
| dropI | Agda.Syntax.Position |
| dropMore | Agda.Utils.Permutation |
| dropN | Agda.Utils.Permutation |
| dropParameters | Agda.TypeChecking.ReconstructParameters |
| droppedP | Agda.Utils.Permutation |
| droppedPars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dropProjElims | Agda.Syntax.Internal |
| dropS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| dropSameCandidates | Agda.TypeChecking.InstanceArguments |
| dropTopLevelModule | Agda.TypeChecking.Errors |
| dropWhileM | Agda.Utils.Monad |
| dryInstantiate | Agda.Auto.NarrowingSearch |
| dsConnection | Agda.Interaction.Highlighting.Dot |
| DSizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DSizeMeta | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DSizeVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dsModules | Agda.Interaction.Highlighting.Dot |
| dsNameSupply | Agda.Interaction.Highlighting.Dot |
| DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dtermToTerm | Agda.TypeChecking.DisplayForm |
| dummyDom | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| duname | Agda.Compiler.MAlonzo.Misc |
| DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DuplicateDefinition | Agda.Syntax.Concrete.Definitions |
| DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| duplicates | Agda.Utils.List |
| DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |