Agda-2.6.4: 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
DataBlockAgda.Syntax.Concrete.Definitions.Types
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
DataDefSAgda.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
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.TypeChecking.Monad, Agda.Compiler.Backend
DataOrRecSigData 
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
DataOrRecSigDefnAgda.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
DataRecOrFunAgda.Syntax.Concrete.Definitions.Types
datarecParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataSig 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
DataSigSAgda.Syntax.Abstract
DataSortAgda.Interaction.Base
dataSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataTranspIxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataTypeAgda.Utils.Haskell.Syntax
Datatype 
1 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DatatypeData 
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
DatatypeDefnAgda.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.Glyph, 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
DDot'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeadCodeAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
DeadcodeAgda.Syntax.Common.Aspect, Agda.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
debugClauseAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
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.TypeChecking.Monad, Agda.Compiler.Backend
decodeFileAgda.TypeChecking.Serialise
decodeFileStrictAgda.Interaction.JSON
decodeFileStrict'Agda.Interaction.JSON
decodeHashesAgda.TypeChecking.Serialise
decodeInterfaceAgda.TypeChecking.Serialise
decodeStrictAgda.Interaction.JSON
decodeStrict'Agda.Interaction.JSON
decodeStrictTextAgda.Interaction.JSON
decomposeIntervalAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
decomposeInterval'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DecorationAgda.Utils.Functor
DecrAgda.Termination.Order
decrAgda.Termination.Order
decreaseAgda.Termination.Order
decreasingAgda.Termination.Order
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
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.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
defaultAnnotationAgda.Syntax.Common
defaultAppInfoAgda.Syntax.Info
defaultAppInfo_Agda.Syntax.Info
defaultArgAgda.Syntax.Common
defaultArgDomAgda.Syntax.Internal
defaultArgInfoAgda.Syntax.Common
defaultAxiomAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultCohesionAgda.Syntax.Common
DefaultComputeAgda.Interaction.Base
defaultCutOffAgda.Termination.CutOff, Agda.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
defaultErasedAgda.Syntax.Common
defaultFixityAgda.Syntax.Common
defaultGetConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetProfileOptionsAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetRewriteRulesForAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetVerbosityAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultImportDirAgda.Syntax.Common
defaultInteractionOptionsAgda.Interaction.Options
defaultInteractionOutputCallbackAgda.Interaction.Response
defaultInteractorAgda.Main
defaultIsDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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
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
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.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
definitionAgda.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
Definitions 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionSite 
1 (Type/Class)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
definitionSiteAgda.Syntax.Common.Aspect, Agda.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
defLanguageAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
defOpaque 
1 (Function)Agda.Syntax.Info
2 (Function)Agda.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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSiteHereAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSiteModuleAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSitePosAgda.Syntax.Common.Aspect, Agda.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
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.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
dfPatsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfPatternVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dgetAgda.Utils.Functor
DiagnosticsColoursAgda.Interaction.Options
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
DifferentOpaqueAgda.Syntax.Common
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
DisallowedInterleavedMutualAgda.Syntax.Concrete.Definitions.Errors
disallowGeneralizedVarsAgda.Syntax.Scope.Base
DisambiguatedName 
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
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
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.Syntax.Common.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.TypeChecking.Monad, Agda.Compiler.Backend
DoesNotMentionTicksAgda.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
doGlueKanOpAgda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DoHCompAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
doHCompUKanOpAgda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DoHighlightModuleContentsAgda.TypeChecking.Rules.Decl
doIdKanOpAgda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
domainUnivAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
doMetaAgda.Syntax.Internal.Defs
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
domIsFiniteAgda.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
DontExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontExpandLastAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontFoldLetBindingsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontHightlightModuleContentsAgda.TypeChecking.Rules.Decl
DontKnowAgda.TypeChecking.Patterns.Match
DontOpenAgda.Syntax.Concrete
DontReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunRecordPatternTranslationAgda.TypeChecking.CompiledClause.Compile
DontWakeUpAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
DoOpenAgda.Syntax.Concrete
doPathPKanOpAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
doPiKanOpAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
dotBackendAgda.Interaction.Highlighting.Dot
DotFlexAgda.TypeChecking.Rules.LHS.Problem
DoThenAgda.Syntax.Concrete
DOtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DottedPatternAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
DoubleAgda.Compiler.JS.Syntax
doubleAgda.Syntax.Common.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.Syntax.Common.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.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
dropTypeAndModalityAgda.Syntax.Concrete
dropWhileAgda.Utils.List1
dropWhileEndMAgda.Utils.Monad
dropWhileMAgda.Utils.Monad
dryInstantiateAgda.Auto.NarrowingSearch
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
DTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DTerm'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateDefinitionAgda.Syntax.Concrete.Definitions.Errors
DuplicateExecutableAgda.Interaction.Library.Base
DuplicateFields 
1 (Data Constructor)Agda.TypeChecking.Monad.Base.Warning
2 (Data Constructor)Agda.Interaction.Library.Base
3 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateFields_Agda.Interaction.Options.Warnings
DuplicateImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicatePrimitiveBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
duplicatesAgda.Utils.List
DuplicateUsingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateUsing_Agda.Interaction.Options.Warnings
DWithAppAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dwLocationAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dwWarningAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions