Agda-2.6.1.3: 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.TypeChecking.Monad, Agda.Compiler.Backend
dataClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataConAgda.TypeChecking.Datatypes
dataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
dataIxsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataMustEndInSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataNameAgda.Syntax.Scope.Base
DataOrNewAgda.Utils.Haskell.Syntax
DataOrRecordAgda.Syntax.Common
DataOrRecSigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataPathConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
datarecParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataSig 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
dataSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.Pretty
2 (Function)Agda.TypeChecking.Pretty
DBSizeExprAgda.TypeChecking.SizedTypes.Solve
DConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DDotAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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
debugConstraintsAgda.TypeChecking.Constraints
debugPrintDeclAgda.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
DeclarationExceptionAgda.Syntax.Concrete.Definitions
DeclarationPanicAgda.Syntax.Concrete.Definitions
DeclarationWarningAgda.Syntax.Concrete.Definitions
declarationWarningNameAgda.Syntax.Concrete.Definitions
DeclContAgda.Auto.Syntax
DeclInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
declNameAgda.Syntax.Info
declRangeAgda.Syntax.Info
decodeAgda.TypeChecking.Serialise
DecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
decodeFileAgda.TypeChecking.Serialise
decodeHashesAgda.TypeChecking.Serialise
decodeInterfaceAgda.TypeChecking.Serialise
decomposeIntervalAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
decomposeInterval'Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
decompressAgda.Interaction.Highlighting.Precise
DecorationAgda.Utils.Functor
DecrAgda.Termination.Order
decrAgda.Termination.Order
decreaseAgda.Termination.Order
decreasingAgda.Termination.Order
deepEtaExpandAgda.TypeChecking.EtaExpand
DeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
deepSizeViewAgda.TypeChecking.SizedTypes
deepUnscopeAgda.Syntax.Abstract.Views
deepUnscopeDeclAgda.Syntax.Abstract.Views
deepUnscopeDeclsAgda.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
defAccessAgda.Syntax.Info
defAppAgda.TypeChecking.Substitute
DefArgAgda.TypeChecking.Positivity.Occurrence
defArgGeneralizableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgsAgda.TypeChecking.MetaVars.Occurs
DefaultAgda.Utils.WithDefault
defaultActionAgda.TypeChecking.CheckInternal
defaultAddCtxAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultAddLetBinding'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultAppInfoAgda.Syntax.Info
defaultAppInfo_Agda.Syntax.Info
defaultArgAgda.Syntax.Common
defaultArgDomAgda.Syntax.Internal
defaultArgInfoAgda.Syntax.Common
defaultCohesionAgda.Syntax.Common
DefaultComputeAgda.Interaction.Base
defaultCSSFileAgda.Interaction.Highlighting.HTML
defaultCutOffAgda.Interaction.Options
defaultDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultDisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultDomAgda.Syntax.Internal
defaultFixityAgda.Syntax.Common
defaultGetConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetRewriteRulesForAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGHCOptionsAgda.Compiler.MAlonzo.Compiler
defaultImportDirAgda.Syntax.Common
defaultInteractionAgda.Main
defaultInteractionOptionsAgda.Interaction.Options
defaultInteractionOutputCallbackAgda.Interaction.Response
defaultJSOptionsAgda.Compiler.JS.Compiler
defaultLevelsToZeroAgda.TypeChecking.Level.Solve
defaultLibDirAgda.Interaction.Options
defaultModalityAgda.Syntax.Common
defaultNamedArgAgda.Syntax.Common
defaultNamedArgDomAgda.Syntax.Internal
defaultOpenLevelsToZeroAgda.TypeChecking.Level.Solve
defaultOptionsAgda.Interaction.Options
defaultParseFlagsAgda.Syntax.Parser.Monad
defaultPatternInfoAgda.Syntax.Internal
defaultPragmaOptionsAgda.Interaction.Options
defaultQuantityAgda.Syntax.Common
defaultRelevanceAgda.Syntax.Common
defaultTerEnvAgda.Termination.Monad
DefaultToInfty 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Solve
defaultUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultVerbosityAgda.Interaction.Options
defaultWarningModeAgda.Interaction.Options.Warnings
defaultWarningSetAgda.Interaction.Options.Warnings
defBlockedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompilerPragmasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCopatternLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCopyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defDelayedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defDisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defFixityAgda.Syntax.Info
defForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defGeneralizedParamsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defineCompDataAgda.TypeChecking.Rules.Data
defineCompKitRAgda.TypeChecking.Rules.Record
DefinedAgda.Syntax.Scope.Base
DefinedNameAgda.Syntax.Scope.Base
defineHCompForFieldsAgda.TypeChecking.Rules.Data
defineProjectionsAgda.TypeChecking.Rules.Data
defineTranspForFieldsAgda.TypeChecking.Rules.Data
defineTranspOrHCompForFieldsAgda.TypeChecking.Rules.Data
defineTranspOrHCompRAgda.TypeChecking.Rules.Record
DefInfo 
1 (Data Constructor)Agda.Syntax.Info
2 (Type/Class)Agda.Syntax.Abstract
defInfoAgda.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
definitionCheckAgda.TypeChecking.MetaVars.Occurs
DefinitionIsErasedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionSite 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
definitionSiteAgda.Interaction.Highlighting.Precise
defInjectiveAgda.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
DefInsteadOfConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defInverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defIsDataOrRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defIsRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defJSDefAgda.Compiler.JS.Compiler
defMacroAgda.Syntax.Info
defMatchableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defMutualAgda.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
defnAgda.Compiler.JS.Syntax
defNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defNeedsCheckingAgda.TypeChecking.MetaVars.Occurs
defNoCompilationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefNodeAgda.TypeChecking.Positivity
defNonterminatingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defOrVarAgda.TypeChecking.Rules.Term
DefP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
defParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
defTypeAgda.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
delimiterAgda.Utils.String
dependencySortMetasAgda.TypeChecking.MetaVars
dependentPolarityAgda.TypeChecking.Polarity
DeprecationWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
dfFreeVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfPatsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
difference 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.IntSet.Infinite
3 (Function)Agda.Utils.SmallSet
DioidAgda.TypeChecking.SizedTypes.Utils
DirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirGeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dirToCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Dirty 
1 (Type/Class)Agda.TypeChecking.Unquote
2 (Data Constructor)Agda.TypeChecking.Unquote
dirtyAgda.Utils.Update
disableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DisallowedGeneralizeNameAgda.Syntax.Scope.Base
disallowGeneralizedVarsAgda.Syntax.Scope.Base
DisambiguatedNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
disambiguateRecordFieldsAgda.Interaction.Highlighting.Generate
discreteAgda.Utils.Graph.AdjacencyMap.Unidirectional
DisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayDebugMessageAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayFormAgda.TypeChecking.DisplayForm
displayFormAritiesAgda.TypeChecking.DisplayForm
DisplayFormsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayFormsEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Pretty
doc 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser.Monad
doclosAgda.Auto.Syntax
doCompileAgda.Compiler.Common
DocPAgda.Utils.Parser.MemoisedCPS
doDefAgda.Syntax.Internal.Defs
DoDropAgda.Utils.Permutation
doDropAgda.Utils.Permutation
doesFileExistCaseSensitiveAgda.Utils.FileName
DoesNotConstructAnElementOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
doExpandLastAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoGeneralizeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoHCompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DoHighlightModuleContentsAgda.TypeChecking.Rules.Decl
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
domFiniteAgda.Syntax.Internal
domFromArgAgda.Syntax.Internal
domFromNamedArgAgda.Syntax.Internal
domFromNamedArgNameAgda.TypeChecking.Substitute
domHAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
dominatedAgda.Utils.Favorites
DominatesAgda.Utils.Favorites
dominatorAgda.Utils.Favorites
domInfoAgda.Syntax.Internal
domNAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
domNameAgda.Syntax.Internal
domOfBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
domTacticAgda.Syntax.Internal
Done 
1 (Data Constructor)Agda.TypeChecking.CompiledClause
2 (Data Constructor)Agda.Interaction.Base
DoNotParseSectionsAgda.Syntax.Concrete.Operators.Parser
dontAssignMetasAgda.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
DontCutOffAgda.Termination.CutOff
DontDefaultToInftyAgda.TypeChecking.SizedTypes.Solve
dontDescendIntoAgda.Utils.Geniplate
DontExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontExpandLastAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontHightlightModuleContentsAgda.TypeChecking.Rules.Decl
DontKnow 
1 (Data Constructor)Agda.TypeChecking.Patterns.Match
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify
DontOpenAgda.Syntax.Concrete
DontRunMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunRecordPatternTranslationAgda.TypeChecking.CompiledClause.Compile
DoOpenAgda.Syntax.Concrete
DoQuoteTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
DotFlexAgda.TypeChecking.Rules.LHS.Problem
DoThenAgda.Syntax.Concrete
DOtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DotMAgda.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
dotPAgda.Syntax.Internal
DotPatternAgda.TypeChecking.Rules.LHS.Problem
DotPatternCtxAgda.Syntax.Fixity
dotPatternsAgda.TypeChecking.Rules.LHS.Problem
dotPatternsToPatternsAgda.TypeChecking.Patterns.Internal
DoTranspAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DotState 
1 (Type/Class)Agda.Interaction.Highlighting.Dot
2 (Data Constructor)Agda.Interaction.Highlighting.Dot
DottedPatternAgda.Interaction.Highlighting.Precise
dottifyAgda.Interaction.Highlighting.Dot
DoubleAgda.Compiler.JS.Syntax
doubleAgda.Utils.Pretty
doubleblockAgda.Auto.NarrowingSearch
doubleCAgda.TypeChecking.Serialise.Base
doubleDAgda.TypeChecking.Serialise.Base
DoubleDotAgda.Syntax.Concrete
doubleEAgda.TypeChecking.Serialise.Base
doubleQuotesAgda.Utils.Pretty
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
DropArgsAgda.TypeChecking.DropArgs
dropArgsAgda.TypeChecking.DropArgs
dropCommonAgda.Utils.List
dropConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropEndAgda.Utils.List
dropFromAgda.Utils.Permutation
drophidAgda.Auto.CaseSplit
dropMoreAgda.Utils.Permutation
dropNAgda.Utils.Permutation
dropParametersAgda.TypeChecking.ReconstructParameters
droppedPAgda.Utils.Permutation
droppedParsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
dropTopLevelModuleAgda.TypeChecking.Errors
dropWhileEndMAgda.Utils.Monad
dropWhileMAgda.Utils.Monad
dryInstantiateAgda.Auto.NarrowingSearch
dsConnectionAgda.Interaction.Highlighting.Dot
DSizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DSizeMetaAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DSizeVarAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dsModulesAgda.Interaction.Highlighting.Dot
dsNameSupplyAgda.Interaction.Highlighting.Dot
DTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dtermToTermAgda.TypeChecking.DisplayForm
DummyAgda.Syntax.Internal
dummyDomAgda.Syntax.Internal
dummyLevelAgda.Syntax.Internal
dummyLevel'Agda.Syntax.Internal
DummySAgda.Syntax.Internal
dummySortAgda.Syntax.Internal
dummyTermAgda.Syntax.Internal
dummyTerm'Agda.Syntax.Internal
dummyTypeAgda.Syntax.Internal
dunameAgda.Compiler.MAlonzo.Misc
DuplicateBuiltinBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateDefinitionAgda.Syntax.Concrete.Definitions
DuplicateFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicatePrimitiveBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
duplicatesAgda.Utils.List
DWithAppAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend