| Data | Agda.Syntax.Concrete |
| dataAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataDecls | Agda.Compiler.Epic.CompileState |
| DataDef | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| dataHsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DataInfo | Agda.TypeChecking.Datatypes |
| dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify |
| dataParameters | Agda.Compiler.Epic.Forcing |
| dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Datatype | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DatatypeInfo | Agda.TypeChecking.Datatypes |
| datatypeIxs | Agda.TypeChecking.Datatypes |
| datatypeIxTel | Agda.TypeChecking.Datatypes |
| datatypeName | Agda.TypeChecking.Datatypes |
| datatypePars | Agda.TypeChecking.Datatypes |
| datatypeParTel | Agda.TypeChecking.Datatypes |
| deBruijnIndex | Agda.Interaction.MakeCase |
| DeBruijnPat | Agda.Termination.TermCheck |
| debug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad |
| decDigit | Agda.Utils.Char |
| Declaration | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| DeclarationException | Agda.Syntax.Concrete.Definitions |
| DeclarationPanic | 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 |
| declsForPrim | Agda.Compiler.MAlonzo.Primitives |
| decode | Agda.TypeChecking.Serialise |
| DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| decodeFile | Agda.TypeChecking.Serialise |
| decompress | Agda.Interaction.Highlighting.Precise |
| decr | Agda.Termination.CallGraph |
| decrConf | Agda.TypeChecking.Test.Generators |
| decreasing | Agda.Termination.CallGraph |
| Def | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| defAbstract | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defAccess | Agda.Syntax.Info |
| DefArg | Agda.TypeChecking.Positivity |
| Default | Agda.Compiler.Epic.AuxAST |
| defaultArg | Agda.Syntax.Common |
| defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defaultFixity | Agda.Syntax.Fixity |
| defaultFixity' | Agda.Syntax.Fixity |
| defaultFrequencies | Agda.TypeChecking.Test.Generators |
| defaultImportDir | Agda.Syntax.Concrete |
| defaultNotation | Agda.Syntax.Notation |
| defaultOptions | Agda.Interaction.Options |
| defaultParseFlags | Agda.Syntax.Parser.Monad |
| defaultVerbosity | Agda.Interaction.Options |
| defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defDelayed | |
| 1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Compiler.Epic.CompileState |
| defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defFixity | Agda.Syntax.Info |
| defFreq | Agda.TypeChecking.Test.Generators |
| DefinedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| DefInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| defInfo | Agda.Syntax.Info |
| Definition | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| definition | Agda.Compiler.MAlonzo.Compiler |
| DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| definitions | |
| 1 (Function) | Agda.Compiler.Epic.CompileState |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| definitionSite | Agda.Interaction.Highlighting.Precise |
| defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Defn | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DefName | |
| 1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DefNode | Agda.TypeChecking.Positivity |
| DefP | Agda.Syntax.Abstract |
| defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Delayed | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Dependent | Agda.Interaction.GhciTop |
| depthofvar | Agda.Auto.CaseSplit |
| deref | Agda.Utils.Pointer |
| detecteliminand | Agda.Auto.Syntax |
| detectsemiflex | Agda.Auto.Syntax |
| diagonal | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| disjoin | Agda.Utils.QuickCheck |
| Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| displayErrorAndExit | Agda.Interaction.GhciTop |
| DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| displayForm | Agda.TypeChecking.DisplayForm |
| displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| displayStatus | Agda.Interaction.GhciTop |
| DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| display_info | Agda.Interaction.GhciTop |
| display_info' | Agda.Interaction.GhciTop |
| display_infoD | Agda.Interaction.GhciTop |
| Dist | Agda.Utils.Warshall |
| Distance | Agda.Utils.Warshall |
| distinct | Agda.Utils.List |
| divConf | Agda.TypeChecking.Test.Generators |
| DLub | Agda.Syntax.Internal |
| dLub | Agda.TypeChecking.Substitute |
| Doc | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.TypeChecking.Pretty |
| doclos | Agda.Auto.Syntax |
| DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| doEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DomainFree | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| DomainFull | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Done | Agda.TypeChecking.CompiledClause |
| DontCare | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| dontCare | Agda.Auto.Syntax |
| dontEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DontExpandLast | Agda.TypeChecking.Rules.Term |
| DontKnow | |
| 1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 2 (Data Constructor) | Agda.Compiler.Epic.Erasure |
| 3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify |
| DontOpen | Agda.Syntax.Concrete |
| dontReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| DoOpen | Agda.Syntax.Concrete |
| Dot | Agda.Syntax.Concrete |
| DotP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| DotPatternCtx | Agda.Syntax.Fixity |
| DotPatternInst | Agda.TypeChecking.Rules.LHS |
| dotPatternInsts | Agda.TypeChecking.Rules.LHS |
| DottedPattern | Agda.Interaction.Highlighting.Precise |
| DotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| dotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| double | Agda.Utils.Pretty |
| doubleblock | Agda.Auto.NarrowingSearch |
| doubleQuotes | Agda.Utils.Pretty |
| DPI | Agda.TypeChecking.Rules.LHS |
| dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| drophid | Agda.Auto.CaseSplit |
| dropI | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| dryInstantiate | Agda.Auto.NarrowingSearch |
| dsubname | Agda.Compiler.MAlonzo.Misc |
| DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dummy | Agda.Compiler.MAlonzo.Misc |
| DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |