| 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.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.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 |
| DataName | Agda.Syntax.Scope.Base |
| DataOrNew | Agda.Utils.Haskell.Syntax |
| DataOrRecord | Agda.Syntax.Common |
| DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dataPathCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| datarecPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DataSig | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 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 |
| Deadcode | Agda.Interaction.Highlighting.Precise |
| deadStandardOptions | Agda.Interaction.Options |
| 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 |
| 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 |
| declarationWarningName | 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 |
| decomposeInterval | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| decomposeInterval' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| 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 |
| deepEtaExpand | Agda.TypeChecking.EtaExpand |
| 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.Internal |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 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 |
| defArgGeneralizable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| Default | Agda.Utils.WithDefault |
| defaultAction | Agda.TypeChecking.CheckInternal |
| defaultAddCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultAddLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defaultAppInfo | Agda.Syntax.Info |
| defaultAppInfo_ | Agda.Syntax.Info |
| defaultArg | Agda.Syntax.Common |
| defaultArgDom | Agda.Syntax.Internal |
| defaultArgInfo | Agda.Syntax.Common |
| defaultCohesion | Agda.Syntax.Common |
| DefaultCompute | Agda.Interaction.Base |
| 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.Internal |
| defaultFixity | Agda.Syntax.Common |
| 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 |
| defaultLevelsToZero | Agda.TypeChecking.Level.Solve |
| defaultLibDir | Agda.Interaction.Options |
| defaultModality | Agda.Syntax.Common |
| defaultNamedArg | Agda.Syntax.Common |
| defaultNamedArgDom | Agda.Syntax.Internal |
| defaultOpenLevelsToZero | Agda.TypeChecking.Level.Solve |
| defaultOptions | Agda.Interaction.Options |
| defaultParseFlags | Agda.Syntax.Parser.Monad |
| defaultPatternInfo | Agda.Syntax.Internal |
| defaultPragmaOptions | Agda.Interaction.Options |
| defaultQuantity | Agda.Syntax.Common |
| defaultRelevance | Agda.Syntax.Common |
| 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 |
| defaultWarningMode | Agda.Interaction.Options.Warnings |
| defaultWarningSet | Agda.Interaction.Options.Warnings |
| defBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| defCopatternLHS | 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 |
| defForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defGeneralizedParams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Definition | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Type/Class) | Agda.Syntax.Reflected |
| 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 |
| definitionCheck | Agda.TypeChecking.MetaVars.Occurs |
| DefinitionIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| defInverse | 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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs |
| defNoCompilation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DefNode | Agda.TypeChecking.Positivity |
| defNonterminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| defOrVar | Agda.TypeChecking.Rules.Term |
| DefP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | 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 |
| 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.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.SmallSet |
| 3 (Function) | Agda.Utils.Trie |
| 4 (Function) | Agda.Utils.AssocList |
| delimiter | Agda.Utils.String |
| dependencySortMetas | Agda.TypeChecking.MetaVars |
| dependentPolarity | Agda.TypeChecking.Polarity |
| DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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.IntSet.Infinite |
| 3 (Function) | Agda.Utils.SmallSet |
| 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 |
| disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DisallowedGeneralizeName | Agda.Syntax.Scope.Base |
| disallowGeneralizedVars | Agda.Syntax.Scope.Base |
| DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| disambiguateRecordFields | Agda.Interaction.Highlighting.Generate |
| 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 |
| 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.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 |
| DoGeneralize | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DoHComp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| 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.Base, Agda.TypeChecking.Primitive |
| dominated | Agda.Utils.Favorites |
| Dominates | Agda.Utils.Favorites |
| dominator | Agda.Utils.Favorites |
| domInfo | Agda.Syntax.Internal |
| domN | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| domName | Agda.Syntax.Internal |
| domOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.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 |
| DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl |
| 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 |
| DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile |
| DoOpen | Agda.Syntax.Concrete |
| DoQuoteTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| DotFlex | Agda.TypeChecking.Rules.LHS.Problem |
| DoThen | Agda.Syntax.Concrete |
| DOtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| DotM | Agda.Interaction.Highlighting.Dot |
| 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.Cubical, Agda.TypeChecking.Primitive |
| 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 |
| DoubleDot | Agda.Syntax.Concrete |
| doubleE | Agda.TypeChecking.Serialise.Base |
| doubleQuotes | Agda.Utils.Pretty |
| 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 |
| 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 |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| dropS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| dropTopLevelModule | Agda.TypeChecking.Errors |
| dropWhileEndM | Agda.Utils.Monad |
| 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 |
| Dummy | Agda.Syntax.Internal |
| dummyDom | Agda.Syntax.Internal |
| dummyLevel | Agda.Syntax.Internal |
| dummyLevel' | Agda.Syntax.Internal |
| DummyS | Agda.Syntax.Internal |
| dummySort | Agda.Syntax.Internal |
| dummyTerm | Agda.Syntax.Internal |
| dummyTerm' | Agda.Syntax.Internal |
| dummyType | Agda.Syntax.Internal |
| 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 |
| DuplicatePrimitiveBinding | 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 |