Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant

Index - D

DAgda.Auto.Options
DAG 
1 (Type/Class)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Data Constructor)Agda.Utils.Graph.AdjacencyMap.Unidirectional
dagComponentMapAgda.Utils.Graph.AdjacencyMap.Unidirectional
dagGraphAgda.Utils.Graph.AdjacencyMap.Unidirectional
dagInvariantAgda.Utils.Graph.AdjacencyMap.Unidirectional
dagNodeMapAgda.Utils.Graph.AdjacencyMap.Unidirectional
DataAgda.Syntax.Concrete
dataAbstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataBlockAgda.Syntax.Concrete.Definitions.Types
dataClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataConAgda.TypeChecking.Datatypes
dataConsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataConstructorAgda.Syntax.Reflected
DataDeclAgda.Utils.Haskell.Syntax
DataDef 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
dataDefGeneralizedParamsAgda.Syntax.Abstract
DataDefParams 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
dataDefParamsAgda.Syntax.Abstract
DataDefSAgda.Syntax.Abstract
dataIxsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataMustEndInSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataMutualAgda.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
DataOrNewAgda.Utils.Haskell.Syntax
DataOrRecord 
1 (Type/Class)Agda.Syntax.Internal
2 (Type/Class)Agda.TypeChecking.Rules.LHS
DataOrRecordModuleAgda.Syntax.Scope.Base
DataOrRecSigAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataOrRecSigData 
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
DataOrRecSigDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataParsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataPathConsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataRecOrFunAgda.Syntax.Concrete.Definitions.Types
datarecParsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataSig 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
DataSigSAgda.Syntax.Abstract
DataSortAgda.Interaction.Base
dataSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataTranspAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataTranspIxAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataTypeAgda.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
DatatypeData 
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
DatatypeDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dbPatPermAgda.Syntax.Internal.Pattern
dbPatPerm'Agda.Syntax.Internal.Pattern
DBPatVar 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
dbPatVarIndexAgda.Syntax.Internal
dbPatVarNameAgda.Syntax.Internal
dbraces 
1 (Function)Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
2 (Function)Agda.TypeChecking.Pretty
DBSizeExprAgda.TypeChecking.SizedTypes.Solve
DConAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DDotAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DeadCodeAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
DeadcodeAgda.Interaction.Highlighting.Precise
deadStandardOptionsAgda.Interaction.Options
DeBruijnAgda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnIndexOutOfScopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
debruijnNamedVarAgda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnPatternAgda.Syntax.Internal
deBruijnVarAgda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
deBruijnViewAgda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
debugAgda.TypeChecking.SizedTypes.Utils
debugClauseAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
debugConstraintsAgda.TypeChecking.Constraints
debugPrintDeclAgda.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
declarationExceptionAgda.Syntax.Concrete.Definitions.Monad
DeclarationException'Agda.Syntax.Concrete.Definitions.Errors
DeclarationPanicAgda.Syntax.Concrete.Definitions.Errors
DeclarationSpineAgda.Syntax.Abstract
declarationSpineAgda.Syntax.Abstract
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
declarationWarningAgda.Syntax.Concrete.Definitions.Monad
DeclarationWarning'Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationWarning'Agda.Syntax.Concrete.Definitions.Monad
declarationWarningNameAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationWarningName'Agda.Syntax.Concrete.Definitions.Errors
DeclaredNamesAgda.Syntax.Abstract.Views
declaredNamesAgda.Syntax.Abstract.Views
DeclContAgda.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
DeclNumAgda.Syntax.Concrete.Definitions.Types
declRangeAgda.Syntax.Info
decode 
1 (Function)Agda.TypeChecking.Serialise
2 (Function)Agda.Interaction.JSON
decode'Agda.Interaction.JSON
DecodedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
decodeFileAgda.TypeChecking.Serialise
decodeFileStrictAgda.Interaction.JSON
decodeFileStrict'Agda.Interaction.JSON
decodeHashesAgda.TypeChecking.Serialise
decodeInterfaceAgda.TypeChecking.Serialise
decodeStrictAgda.Interaction.JSON
decodeStrict'Agda.Interaction.JSON
decomposeIntervalAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
decomposeInterval'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
DecorationAgda.Utils.Functor
DecrAgda.Termination.Order
decrAgda.Termination.Order
decreaseAgda.Termination.Order
decreasingAgda.Termination.Order
deepEtaExpandAgda.TypeChecking.EtaExpand
DeepSizeViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
deepSizeViewAgda.TypeChecking.SizedTypes
deepUnscopeAgda.Syntax.Abstract.Views
deepUnscopeDeclAgda.Syntax.Abstract.Views
deepUnscopeDeclsAgda.Syntax.Abstract.Views
deExceptionAgda.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
defAccessAgda.Syntax.Info
defAppAgda.TypeChecking.Substitute
DefArgAgda.TypeChecking.Positivity.Occurrence
defArgGeneralizableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgInfoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgsAgda.TypeChecking.MetaVars.Occurs
DefaultAgda.Utils.WithDefault
defaultActionAgda.TypeChecking.CheckInternal
defaultAddCtxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
defaultAddLetBinding'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
defaultAnnotationAgda.Syntax.Common
defaultAppInfoAgda.Syntax.Info
defaultAppInfo_Agda.Syntax.Info
defaultArgAgda.Syntax.Common
defaultArgDomAgda.Syntax.Internal
defaultArgInfoAgda.Syntax.Common
defaultAxiomAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultCohesionAgda.Syntax.Common
DefaultComputeAgda.Interaction.Base
defaultCutOffAgda.Termination.CutOff, Agda.Interaction.Options
defaultDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultDisplayFormAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultDomAgda.Syntax.Internal
defaultErasedAgda.Syntax.Common
defaultFixityAgda.Syntax.Common
defaultGetConstInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
defaultGetProfileOptionsAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultGetRewriteRulesForAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
defaultGetVerbosityAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultGHCFlagsAgda.Compiler.MAlonzo.Compiler
defaultImportDirAgda.Syntax.Common
defaultInteractionOptionsAgda.Interaction.Options
defaultInteractionOutputCallbackAgda.Interaction.Response
defaultInteractorAgda.Main
defaultIsDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultJSONKeyOptionsAgda.Interaction.JSON
defaultJSOptionsAgda.Compiler.JS.Compiler
defaultLevelsToZeroAgda.TypeChecking.Level.Solve
defaultLockAgda.Syntax.Common
defaultModalityAgda.Syntax.Common
defaultNamedArgAgda.Syntax.Common
defaultNamedArgDomAgda.Syntax.Internal
defaultNowDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultOpenLevelsToZeroAgda.TypeChecking.Level.Solve
defaultOptions 
1 (Function)Agda.Interaction.Options
2 (Function)Agda.Interaction.JSON
defaultParseFlagsAgda.Syntax.Parser.Monad
defaultPatternInfoAgda.Syntax.Internal
defaultPragmaOptionsAgda.Interaction.Options
DefaultProjectConfigAgda.Interaction.Library.Base, Agda.Interaction.Library
defaultQuantityAgda.Syntax.Common
defaultRelevanceAgda.Syntax.Common
defaultTaggedObjectAgda.Interaction.JSON
defaultTbInfoAgda.Syntax.Abstract
defaultTerEnvAgda.Termination.Monad
DefaultToInfty 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Solve
defaultUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultWarningModeAgda.Interaction.Options.Warnings
defaultWarningSetAgda.Interaction.Options.Warnings
defBlockedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defClausesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompiledAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompiledRepAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompilerPragmasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defConstructorsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCopatternLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCopyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defDelayedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defDisplayAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defFixityAgda.Syntax.Info
defForcedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defGeneralizedParamsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defineCompDataAgda.TypeChecking.Rules.Data
defineCompKitRAgda.TypeChecking.Rules.Record
defineConClauseAgda.TypeChecking.Rules.Data
DefinedAgda.Syntax.Scope.Base
DefinedNameAgda.Syntax.Scope.Base
defineHCompForFieldsAgda.TypeChecking.Rules.Data
defineKanOperationForFieldsAgda.TypeChecking.Rules.Data
defineKanOperationRAgda.TypeChecking.Rules.Record
defineProjectionsAgda.TypeChecking.Rules.Data
defineTranspForFieldsAgda.TypeChecking.Rules.Data
defineTranspFunAgda.TypeChecking.Rules.Data
defineTranspIxAgda.TypeChecking.Rules.Data
DefInfo 
1 (Data Constructor)Agda.Syntax.Info
2 (Type/Class)Agda.Syntax.Abstract
defInfoAgda.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
definitionCheckAgda.TypeChecking.MetaVars.Occurs
DefinitionIsErasedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefinitionIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Definitions 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Type/Class)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
definitionSiteAgda.Interaction.Highlighting.Precise
defInjectiveAgda.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
DefInsteadOfConAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defInverseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defIsDataOrRecordAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defIsRecordAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defJSDefAgda.Compiler.JS.Compiler
defLanguageAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defMacroAgda.Syntax.Info
defMatchableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defMutualAgda.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
defnAgda.Compiler.JS.Syntax
defNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defNeedsCheckingAgda.TypeChecking.MetaVars.Occurs
defNoCompilationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefNodeAgda.TypeChecking.Positivity
defNonterminatingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defOrVarAgda.TypeChecking.Rules.Term
DefP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
defParametersAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defPolarityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefSAgda.Syntax.Internal
defSiteAnchorAgda.Interaction.Highlighting.Precise
defSiteHereAgda.Interaction.Highlighting.Precise
defSiteModuleAgda.Interaction.Highlighting.Precise
defSitePosAgda.Interaction.Highlighting.Precise
defTacticAgda.Syntax.Info
defTerminationUnconfirmedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defTypeAgda.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
delayedMergeInvariantAgda.Interaction.Highlighting.Precise
delete 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BoolSet
3 (Function)Agda.Utils.SmallSet
4 (Function)Agda.Utils.Trie
5 (Function)Agda.Utils.AssocList
deleteAtAgda.TypeChecking.Rules.LHS.Unify.Types
deleteLeftAgda.TypeChecking.Rules.LHS.Unify.Types
deleteRightAgda.TypeChecking.Rules.LHS.Unify.Types
deleteTypeAgda.TypeChecking.Rules.LHS.Unify.Types
DeletionAgda.TypeChecking.Rules.LHS.Unify.Types
delimiterAgda.Utils.String
deLocationAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dependencySortMetasAgda.TypeChecking.MetaVars
DeprecationWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DeprecationWarning_Agda.Interaction.Options.Warnings
depthofvarAgda.Auto.CaseSplit
derefPtrAgda.Utils.Pointer
DerivingAgda.Utils.Haskell.Syntax
DeserializationAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
destAgda.TypeChecking.SizedTypes.WarshallSolver
desugarDoNotationAgda.Syntax.DoNotation
detecteliminandAgda.Auto.Syntax
detectIdentityFunctionsAgda.Compiler.Treeless.Identity
detectsemiflexAgda.Auto.Syntax
dfPatsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dfPatternVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dfRHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dgetAgda.Utils.Functor
DiagonalAgda.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
didYouMeanAgda.TypeChecking.Pretty.Warning
difference 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BoolSet
3 (Function)Agda.Utils.IntSet.Infinite
4 (Function)Agda.Utils.SmallSet
DioidAgda.TypeChecking.SizedTypes.Utils
DirectAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirEqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirGeqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirLeqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dirToCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Dirty 
1 (Type/Class)Agda.TypeChecking.Unquote
2 (Data Constructor)Agda.TypeChecking.Unquote
dirtyAgda.Utils.Update
disableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisallowedGeneralizeNameAgda.Syntax.Scope.Base
disallowGeneralizedVarsAgda.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
DisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
disambiguateRecordFieldsAgda.Interaction.Highlighting.Generate
discreteAgda.Utils.Graph.AdjacencyMap.Unidirectional
DisplayAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayDebugMessageAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisplayFormAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayFormAgda.TypeChecking.DisplayForm
DisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayFormsEnabledAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisplayInfoAgda.Interaction.Response
DisplayPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
displayRunningInfoAgda.Interaction.EmacsCommand
displayStatusAgda.Interaction.InteractionTop
DisplayTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
display_infoAgda.Interaction.InteractionTop
display_info'Agda.Interaction.EmacsCommand
distinctAgda.Utils.List
distributeFAgda.Utils.Functor
dmapAgda.Utils.Functor
dnameAgda.Compiler.MAlonzo.Misc
DoBindAgda.Syntax.Concrete
DoBlockAgda.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
doclosAgda.Auto.Syntax
doCompileAgda.Compiler.Common
doCompile'Agda.Compiler.Common
DocPAgda.Utils.Parser.MemoisedCPS
docsUrlAgda.Version
doDefAgda.Syntax.Internal.Defs
DoDropAgda.Utils.Permutation
doDropAgda.Utils.Permutation
doesFileExistCaseSensitiveAgda.Utils.FileName
DoesNotConstructAnElementOfAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
doExpandLastAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
DoGeneralizeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
doGlueKanOpAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Glue
DoHCompAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
doHCompUKanOpAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.HCompU
DoHighlightModuleContentsAgda.TypeChecking.Rules.Decl
doIdKanOpAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Id
DoLetAgda.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
domainFreeAgda.TypeChecking.Rules.Term
DomainFull 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
DomainsAgda.Utils.TypeLevel
Domains'Agda.Utils.TypeLevel
doMetaAgda.Syntax.Internal.Defs
domFromArgAgda.Syntax.Internal
domFromNamedArgAgda.Syntax.Internal
domFromNamedArgNameAgda.TypeChecking.Substitute
domHAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
dominatedAgda.Utils.Favorites
DominatesAgda.Utils.Favorites
dominatorAgda.Utils.Favorites
domInfoAgda.Syntax.Internal
domIsFiniteAgda.Syntax.Internal
domNAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
domNameAgda.Syntax.Internal
domOfBVAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
domTacticAgda.Syntax.Internal
Done 
1 (Data Constructor)Agda.TypeChecking.CompiledClause
2 (Data Constructor)Agda.Interaction.Base
DoNotParseSectionsAgda.Syntax.Concrete.Operators.Parser
dontAssignMetasAgda.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
DontCutOffAgda.Termination.CutOff
DontDefaultToInftyAgda.TypeChecking.SizedTypes.Solve
DontExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dontExpandLastAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
DontHightlightModuleContentsAgda.TypeChecking.Rules.Decl
DontKnowAgda.TypeChecking.Patterns.Match
DontOpenAgda.Syntax.Concrete
DontReduceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DontRunMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DontRunRecordPatternTranslationAgda.TypeChecking.CompiledClause.Compile
DontWakeUpAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
DoOpenAgda.Syntax.Concrete
doPathPKanOpAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
doPiKanOpAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
DoQuoteTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
doQuoteTermAgda.TypeChecking.Rules.Term
DoStmtAgda.Syntax.Concrete
Dot 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
dotBackendAgda.Interaction.Highlighting.Dot
DotFlexAgda.TypeChecking.Rules.LHS.Problem
DoThenAgda.Syntax.Concrete
DOtherSizeAgda.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
dotPAgda.Syntax.Internal
DotPatternAgda.TypeChecking.Rules.LHS.Problem
DotPatternCtxAgda.Syntax.Fixity
dotPatternsAgda.TypeChecking.Rules.LHS.Problem
dotPatternsToPatternsAgda.TypeChecking.Patterns.Internal
DoTranspAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
DottedPatternAgda.Interaction.Highlighting.Precise
DoubleAgda.Compiler.JS.Syntax
doubleAgda.Utils.Pretty
doubleACosAgda.Utils.Float
doubleACoshAgda.Utils.Float
doubleASinAgda.Utils.Float
doubleASinhAgda.Utils.Float
doubleATanAgda.Utils.Float
doubleATan2Agda.Utils.Float
doubleATanhAgda.Utils.Float
doubleblockAgda.Auto.NarrowingSearch
doubleCAgda.TypeChecking.Serialise.Base
doubleCeilingAgda.Utils.Float
doubleCosAgda.Utils.Float
doubleCoshAgda.Utils.Float
doubleDAgda.TypeChecking.Serialise.Base
doubleDecodeAgda.Utils.Float
doubleDenotEqAgda.Utils.Float
doubleDenotOrdAgda.Utils.Float
doubleDivAgda.Utils.Float
DoubleDotAgda.Syntax.Concrete
doubleEAgda.TypeChecking.Serialise.Base
doubleEncodeAgda.Utils.Float
doubleEqAgda.Utils.Float
doubleExpAgda.Utils.Float
doubleFloorAgda.Utils.Float
doubleLeAgda.Utils.Float
doubleLogAgda.Utils.Float
doubleLtAgda.Utils.Float
doubleMinusAgda.Utils.Float
doubleNegateAgda.Utils.Float
doublePlusAgda.Utils.Float
doublePowAgda.Utils.Float
doubleQuotes 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
doubleRoundAgda.Utils.Float
doubleSinAgda.Utils.Float
doubleSinhAgda.Utils.Float
doubleSqrtAgda.Utils.Float
doubleTanAgda.Utils.Float
doubleTanhAgda.Utils.Float
doubleTimesAgda.Utils.Float
doubleToRatioAgda.Utils.Float
doubleToWord64Agda.Utils.Float
DoWarn 
1 (Type/Class)Agda.Syntax.Concrete.Fixity
2 (Data Constructor)Agda.Syntax.Concrete.Fixity
downFromAgda.Utils.List
Drop 
1 (Type/Class)Agda.Utils.Permutation
2 (Data Constructor)Agda.Utils.Permutation
dropAgda.Utils.List1
DropArgsAgda.TypeChecking.DropArgs
dropArgsAgda.TypeChecking.DropArgs
dropAtAgda.TypeChecking.Rules.LHS.Unify.Types
dropCommonAgda.Utils.List
dropConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
dropDecodedModuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
dropEndAgda.Utils.List
dropFromAgda.Utils.Permutation
drophidAgda.Auto.CaseSplit
dropMoreAgda.Utils.Permutation
dropNAgda.Utils.Permutation
dropParametersAgda.TypeChecking.ReconstructParameters
droppedPAgda.Utils.Permutation
droppedParsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
dropSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
dropTopLevelModuleAgda.TypeChecking.Errors
dropTypeAndModalityAgda.Syntax.Concrete
dropWhileAgda.Utils.List1
dropWhileEndMAgda.Utils.Monad
dropWhileMAgda.Utils.Monad
dryInstantiateAgda.Auto.NarrowingSearch
DSizeInfAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DSizeMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DSizeVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DummyAgda.Syntax.Internal
dummyDomAgda.Syntax.Internal
dummyLevelAgda.Syntax.Internal
dummyLocNameAgda.Syntax.Internal
DummySAgda.Syntax.Internal
dummySortAgda.Syntax.Internal
dummyTermAgda.Syntax.Internal
DummyTermKindAgda.Syntax.Internal
dummyTermWithAgda.Syntax.Internal
dummyTypeAgda.Syntax.Internal
dunameAgda.Compiler.MAlonzo.Misc
DuplicateAnonDeclarationAgda.Syntax.Concrete.Definitions.Errors
DuplicateBuiltinBindingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateConstructorsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateDefinitionAgda.Syntax.Concrete.Definitions.Errors
DuplicateExecutableAgda.Interaction.Library.Base
DuplicateFields 
1 (Data Constructor)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateFieldsWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateFieldsWarning_Agda.Interaction.Options.Warnings
DuplicateImportsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicatePrimitiveBindingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
duplicatesAgda.Utils.List
DuplicateUsingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateUsing_Agda.Interaction.Options.Warnings
DWithAppAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dwLocationAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dwWarningAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions