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
dataArgOccurrences	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
DataInfo	Agda.TypeChecking.Datatypes
dataIxs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
dataPolarity	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
DatatypeInfo	Agda.TypeChecking.Datatypes
datatypeIxs	Agda.TypeChecking.Datatypes
datatypeIxTel	Agda.TypeChecking.Datatypes
datatypeName	Agda.TypeChecking.Datatypes
datatypePars	Agda.TypeChecking.Datatypes
datatypeParTel	Agda.TypeChecking.Datatypes
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
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
decreasing	Agda.Termination.CallGraph
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
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
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
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, Agda.Interaction.GhciTop
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
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, Agda.Interaction.GhciTop
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
DefNode	Agda.TypeChecking.Positivity
defnPars	Agda.Compiler.Epic.Smashing
DefP	Agda.Syntax.Abstract
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
delete	Agda.Utils.VarSet
Dependent	Agda.Interaction.GhciTop
depthofvar	Agda.Auto.CaseSplit
deref	Agda.Utils.Pointer
detecteliminand	Agda.Auto.Syntax
detectsemiflex	Agda.Auto.Syntax
diagonal
1 (Function)	Agda.Termination.SparseMatrix
2 (Function)	Agda.Termination.Matrix
diff	Agda.Compiler.Epic.Erasure
DifferentArities	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
disjoin	Agda.Utils.QuickCheck
Display	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayErrorAndExit	Agda.Interaction.GhciTop
DisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayForm	Agda.TypeChecking.DisplayForm
displayFormsEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
displayStatus	Agda.Interaction.GhciTop
DisplayTerm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_info	Agda.Interaction.GhciTop
display_info'	Agda.Interaction.GhciTop
display_infoD	Agda.Interaction.GhciTop
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
DoesNotConstructAnElementOf	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicit	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
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
Done	Agda.TypeChecking.CompiledClause
DontCare
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Abstract
dontCare	Agda.Auto.Syntax
dontEtaContractImplicit	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandLast	Agda.TypeChecking.Rules.Term
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
DontTouchMe	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
DoOpen	Agda.Syntax.Concrete
Dot	Agda.Syntax.Concrete
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
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
DotVars	Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
dotVars	Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
Double	Agda.Compiler.JS.Syntax
double	Agda.Utils.Pretty
doubleblock	Agda.Auto.NarrowingSearch
doubleQuotes	Agda.Utils.Pretty
doWorkOnTypes	Agda.TypeChecking.Irrelevance
DPI	Agda.TypeChecking.Rules.LHS
dropDecodedModule	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
drophid	Agda.Auto.CaseSplit
dropI	Agda.Syntax.Position, Agda.Interaction.GhciTop
dryInstantiate	Agda.Auto.NarrowingSearch
dsConnection	Agda.Interaction.Highlighting.Dot
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
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