A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
%
&
+
.
/
<
=
>
^
|
-
_
All

Index - D

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
dataClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataCons	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataDef
1 (Data Constructor)	Agda.Syntax.Concrete.Definitions
2 (Data Constructor)	Agda.Syntax.Abstract
dataInduction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataIxs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataMutual	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataNonLinPars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataOrRecord	Agda.TypeChecking.Datatypes
dataOrRecordType	Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordType'	Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordTypeHH	Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordTypeHH'	Agda.TypeChecking.Rules.LHS.Unify
dataParameters	Agda.Compiler.Epic.Forcing
dataParametersTCM	Agda.Compiler.Epic.Forcing
dataPars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataSig
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
dataSmallPars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Datatype
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
DDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DDot	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
deal	Agda.Utils.List
deBruijnIndex	Agda.Interaction.MakeCase
DeBruijnPat	Agda.Termination.Monad, Agda.Termination.TermCheck
DeBruijnPat'	Agda.Termination.Monad
DeBruijnPats	Agda.Termination.Monad
DeBruijnPattern	Agda.Syntax.Internal
debug	Agda.TypeChecking.SizedTypes.Utils
debugPrintDecl	Agda.TypeChecking.Rules.Decl
decDigit	Agda.Utils.Char
Declaration
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
DeclarationException	Agda.Syntax.Concrete.Definitions
DeclarationPanic	Agda.Syntax.Concrete.Definitions
DeclCont	Agda.Auto.Syntax
DeclInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
declName	Agda.Syntax.Info
declRange	Agda.Syntax.Info
declsForPrim	Agda.Compiler.MAlonzo.Primitives
decode	Agda.TypeChecking.Serialise
DecodedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
decodeFile	Agda.TypeChecking.Serialise
decodeHashes	Agda.TypeChecking.Serialise
decodeInterface	Agda.TypeChecking.Serialise
decompress	Agda.Interaction.Highlighting.Precise
Decoration	Agda.Utils.Functor
decr	Agda.Termination.Order
decrConf	Agda.TypeChecking.Test.Generators
decrease	Agda.Termination.Order
decreasing	Agda.Termination.Order
DeepSizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
deepSizeView	Agda.TypeChecking.SizedTypes
deepUnScope	Agda.Syntax.Abstract.Views
Def
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
defAbstract
1 (Function)	Agda.Syntax.Info
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defAccess	Agda.Syntax.Info
defApp	Agda.TypeChecking.Substitute
DefArg	Agda.TypeChecking.Positivity
defArgInfo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defArgOccurrences	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defArgs	Agda.TypeChecking.MetaVars.Occurs
Default	Agda.Compiler.Epic.AuxAST
defaultArg	Agda.Syntax.Common
defaultArgInfo	Agda.Syntax.Common
defaultColoredArg	Agda.Syntax.Common
defaultCSSFile	Agda.Interaction.Highlighting.HTML
defaultCutOff	Agda.Interaction.Options
defaultDefn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultDisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultDom	Agda.Syntax.Common
defaultFixity	Agda.Syntax.Fixity
defaultFixity'	Agda.Syntax.Fixity
defaultFlexibleVar	Agda.TypeChecking.Rules.LHS.Problem
defaultFrequencies	Agda.TypeChecking.Test.Generators
defaultGetRewriteRulesFor	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
defaultImportDir	Agda.Syntax.Concrete
defaultInteractionOptions	Agda.Interaction.Options
defaultInteractionOutputCallback	Agda.Interaction.Response
defaultLibDir	Agda.Interaction.Options
defaultNamedArg	Agda.Syntax.Common
defaultNotation	Agda.Syntax.Notation
defaultOptions	Agda.Interaction.Options
defaultParseFlags	Agda.Syntax.Parser.Monad
defaultTerEnv	Agda.Termination.Monad
defaultVerbosity	Agda.Interaction.Options
defClauses	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defColors	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiledRep	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCopy	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDelayed
1 (Function)	Agda.Compiler.Epic.Interface
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDisplay	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defEpicDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixity	Agda.Syntax.Info
defFreq	Agda.TypeChecking.Test.Generators
Defined	Agda.Syntax.Scope.Base
DefinedName	Agda.Syntax.Scope.Monad
DefInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
defInfo	Agda.Syntax.Info
Definitely	Agda.TypeChecking.Rules.LHS.Unify
Definition	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definition
1 (Function)	Agda.Compiler.JS.Compiler
2 (Function)	Agda.Compiler.MAlonzo.Compiler
DefinitionIsIrrelevant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Definitions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definitions
1 (Function)	Agda.Compiler.Epic.Interface
2 (Function)	Agda.Compiler.MAlonzo.Compiler
definitionSite	Agda.Interaction.Highlighting.Precise
defInstance
1 (Function)	Agda.Syntax.Info
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefInsteadOfCon	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defIsDataOrRecord	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defIsRecord	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defJSDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defMutual	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Defn
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defn
1 (Function)	Agda.Compiler.JS.Syntax
2 (Function)	Agda.Compiler.JS.Compiler
DefName
1 (Data Constructor)	Agda.Syntax.Scope.Base
2 (Type/Class)	Agda.TypeChecking.Test.Generators
3 (Data Constructor)	Agda.TypeChecking.Test.Generators
defName
1 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Function)	Agda.Compiler.Epic.Primitive
defNeedsChecking	Agda.TypeChecking.MetaVars.Occurs
DefNode	Agda.TypeChecking.Positivity
defNonterminating	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defnPars	Agda.Compiler.Epic.Smashing
defOrVar	Agda.TypeChecking.Rules.Term
DefP	Agda.Syntax.Abstract
defPars	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
defPolarity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defRelevance	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefSh	Agda.TypeChecking.Rules.LHS.Unify
defType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Delayed
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
delete
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Trie
dependentPolarity	Agda.TypeChecking.Polarity
depthofvar	Agda.Auto.CaseSplit
derefPtr	Agda.Utils.Pointer, Agda.Syntax.Internal
Deserialization	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
dest	Agda.TypeChecking.SizedTypes.WarshallSolver
detecteliminand	Agda.Auto.Syntax
detectsemiflex	Agda.Auto.Syntax
dfFreeVars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dfPats	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dfRHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dget	Agda.Utils.Functor
Diagonal	Agda.Termination.SparseMatrix
diagonal
1 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)	Agda.Termination.SparseMatrix
diff	Agda.Compiler.Epic.Erasure
difference
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
DifferentArities	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Dioid	Agda.TypeChecking.SizedTypes.Utils
Direct	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirEq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirGeq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirLeq	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dirToCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dirty	Agda.Utils.Update
disableDestructiveUpdate	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
disableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisambiguatedNames	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Discard
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
discard	Agda.Utils.QuickCheck
discrete	Agda.Utils.Graph.AdjacencyMap.Unidirectional
disjoin	Agda.Utils.QuickCheck
Display	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayDebugMessage	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayForm	Agda.TypeChecking.DisplayForm
displayFormArities	Agda.TypeChecking.DisplayForm
displayFormsEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayInfo	Agda.Interaction.Response
displayRunningInfo	Agda.Interaction.EmacsCommand
displayStatus	Agda.Interaction.InteractionTop
DisplayTerm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_info	Agda.Interaction.InteractionTop
display_info'	Agda.Interaction.EmacsCommand
Distance	Agda.Utils.Warshall
distinct	Agda.Utils.List
distributeF	Agda.Utils.Functor
distributive	Agda.Utils.TestHelpers
divConf	Agda.TypeChecking.Test.Generators
DLub	Agda.Syntax.Internal
dLub	Agda.TypeChecking.Substitute
dmap	Agda.Utils.Functor
Doc
1 (Type/Class)	Agda.Utils.Pretty
2 (Type/Class)	Agda.TypeChecking.Pretty
doclos	Agda.Auto.Syntax
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
doEtaContractImplicit	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
doExpandLast	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
Dom
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
3 (Type/Class)	Agda.Syntax.Abstract
4 (Type/Class)	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
domColors	Agda.Syntax.Common
doMeta	Agda.Syntax.Internal.Defs
domFromArg	Agda.Syntax.Common
domH	Agda.TypeChecking.Primitive
dominated	Agda.Utils.Favorites
Dominates	Agda.Utils.Favorites
dominator	Agda.Utils.Favorites
domInfo	Agda.Syntax.Common
domN	Agda.TypeChecking.Primitive
Done	Agda.TypeChecking.CompiledClause
dontAssignMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
DontCare
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
dontCare
1 (Function)	Agda.Auto.Syntax
2 (Function)	Agda.Syntax.Internal
DontCutOff	Agda.Termination.CutOff
dontDescendInto	Agda.Utils.Geniplate
dontEtaContractImplicit	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandInstanceArguments	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dontExpandLast	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
DontKnow
1 (Data Constructor)	Agda.TypeChecking.Patterns.Match
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Unify
DontOpen	Agda.Syntax.Concrete
dontReifyInteractionPoints	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontRunMetaOccursCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontTouchMe	Agda.Syntax.Translation.AbstractToConcrete
DoOpen	Agda.Syntax.Concrete
Dot	Agda.Syntax.Concrete
DotFlex	Agda.TypeChecking.Rules.LHS.Problem
DOtherSize	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DotM	Agda.Interaction.Highlighting.Dot
DotP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
DotPatternCtx	Agda.Syntax.Fixity
DotPatternInst	Agda.TypeChecking.Rules.LHS.Problem
dotPatternInsts	Agda.TypeChecking.Rules.LHS
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
doubleQuotes	Agda.Utils.Pretty
downFrom	Agda.Utils.List
doWorkOnTypes	Agda.TypeChecking.Irrelevance
DPI	Agda.TypeChecking.Rules.LHS.Problem
Drop
1 (Type/Class)	Agda.Utils.Permutation
2 (Data Constructor)	Agda.Utils.Permutation
DropArgs	Agda.TypeChecking.DropArgs
dropArgs	Agda.TypeChecking.DropArgs
dropConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
dropDecodedModule	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
dropFrom	Agda.Utils.Permutation
drophid	Agda.Auto.CaseSplit
dropI	Agda.Syntax.Position
dropMore	Agda.Utils.Permutation
dropN	Agda.Utils.Permutation
droppedP	Agda.Utils.Permutation
droppedPars	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
dropProjElims	Agda.Syntax.Internal
dropS	Agda.TypeChecking.Substitute
dropWhileM	Agda.Utils.Monad
dryInstantiate	Agda.Auto.NarrowingSearch
dsConnection	Agda.Interaction.Highlighting.Dot
DSizeInf	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeMeta	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeVar	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
dsModules	Agda.Interaction.Highlighting.Dot
dsNameSupply	Agda.Interaction.Highlighting.Dot
dsubname	Agda.Compiler.MAlonzo.Misc
DTerm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dtermToTerm	Agda.TypeChecking.DisplayForm
dummy	Agda.Compiler.MAlonzo.Misc
dummyDom	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
dummyLambda	Agda.Compiler.JS.Compiler
DuplicateBuiltinBinding	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateConstructors	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateDefinition	Agda.Syntax.Concrete.Definitions
DuplicateFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
duplicates	Agda.Utils.List
DWithApp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad