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

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.Abstract
2 (Data Constructor)	Agda.Syntax.Concrete.Definitions
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
DataOrRecord	Agda.TypeChecking.Datatypes
dataOrRecordType	Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordType'	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
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
dbIndexToLevel	Agda.TypeChecking.Coverage
dbraces
1 (Function)	Agda.Syntax.Concrete.Pretty
2 (Function)	Agda.TypeChecking.Pretty
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.TermCheck
debug	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad
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
decompress	Agda.Interaction.Highlighting.Precise
decr	Agda.Termination.CallGraph
decrConf	Agda.TypeChecking.Test.Generators
decrease	Agda.Termination.CallGraph
decreasing	Agda.Termination.CallGraph
DeepSizeView	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
deepSizeView	Agda.TypeChecking.SizedTypes
Def
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
defAbstract
1 (Function)	Agda.Syntax.Info
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defAccess	Agda.Syntax.Info
DefArg	Agda.TypeChecking.Positivity
defArgOccurrences	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defArgs	Agda.TypeChecking.MetaVars.Occurs
Default	Agda.Compiler.Epic.AuxAST
defaultArg	Agda.Syntax.Common
defaultDisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultFixity	Agda.Syntax.Fixity
defaultFixity'	Agda.Syntax.Fixity
defaultFrequencies	Agda.TypeChecking.Test.Generators
defaultImportDir	Agda.Syntax.Concrete
defaultInteractionOptions	Agda.Interaction.Options
defaultInteractionOutputCallback	Agda.Interaction.Response
defaultNamedArg	Agda.Syntax.Common
defaultNotation	Agda.Syntax.Notation
defaultOptions	Agda.Interaction.Options
defaultParseFlags	Agda.Syntax.Parser.Monad
defaultVerbosity	Agda.Interaction.Options
defClauses	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
DefElim	Agda.TypeChecking.Eliminators
defEpicDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixity	Agda.Syntax.Info
defFreq	Agda.TypeChecking.Test.Generators
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.MAlonzo.Compiler
2 (Function)	Agda.Compiler.JS.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
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
defnPars	Agda.Compiler.Epic.Smashing
defOrVar	Agda.TypeChecking.Rules.Term
DefP	Agda.Syntax.Abstract
defPolarity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defProjection	Agda.Compiler.JS.Compiler
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
dependentPolarity	Agda.TypeChecking.Polarity
depthofvar	Agda.Auto.CaseSplit
derefPtr	Agda.Utils.Pointer, Agda.Syntax.Internal
detecteliminand	Agda.Auto.Syntax
detectsemiflex	Agda.Auto.Syntax
diagonal
1 (Function)	Agda.Termination.Matrix
2 (Function)	Agda.Termination.SparseMatrix
diff	Agda.Compiler.Epic.Erasure
difference	Agda.Utils.HashMap
DifferentArities	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Direct	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDestructiveUpdate	Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
disableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
discard	Agda.Utils.QuickCheck
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
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
Dist	Agda.Utils.Warshall
Distance	Agda.Utils.Warshall
distinct	Agda.Utils.List
divConf	Agda.TypeChecking.Test.Generators
DLub	Agda.Syntax.Internal
dLub	Agda.TypeChecking.Substitute
Doc
1 (Type/Class)	Agda.Utils.Pretty
2 (Type/Class)	Agda.TypeChecking.Pretty
doclos	Agda.Auto.Syntax
doesFileExistCaseSensitive	Agda.Utils.FileName
DoesNotConstructAnElementOf	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicit	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Dom
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
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
domFromArg	Agda.Syntax.Common
domH	Agda.TypeChecking.Primitive
domHiding	Agda.Syntax.Common
domN	Agda.TypeChecking.Primitive
domRelevance	Agda.Syntax.Common
Done	Agda.TypeChecking.CompiledClause
dontAssignMetas	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
DontCare
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
dontCare	Agda.Auto.Syntax
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
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
DontUseBoundNames	Agda.Syntax.Concrete.Operators
DoOpen	Agda.Syntax.Concrete
Dot	Agda.Syntax.Concrete
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.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
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
DropArgs	Agda.TypeChecking.DropArgs
dropArgs	Agda.TypeChecking.DropArgs
dropConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
dropDecodedModule	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
drophid	Agda.Auto.CaseSplit
dropI	Agda.Syntax.Position
dropNonHidden	Agda.TypeChecking.Rules.Def
dropS	Agda.TypeChecking.Substitute
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
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
DuplicateFields	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DWithApp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad