Agda-2.4.0: A dependently typed functional programming language and proof assistant

Index - D

DataAgda.Syntax.Concrete
dataAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataDef 
1 (Data Constructor)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Concrete.Definitions
dataInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataIxsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataNonLinParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataOrRecordAgda.TypeChecking.Datatypes
dataOrRecordTypeAgda.TypeChecking.Rules.LHS.Unify
dataOrRecordType'Agda.TypeChecking.Rules.LHS.Unify
dataOrRecordTypeHHAgda.TypeChecking.Rules.LHS.Unify
dataOrRecordTypeHH'Agda.TypeChecking.Rules.LHS.Unify
dataParametersAgda.Compiler.Epic.Forcing
dataParametersTCMAgda.Compiler.Epic.Forcing
dataParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataSig 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
dataSmallParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataSortAgda.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
dbIndexToLevelAgda.TypeChecking.Coverage
dbraces 
1 (Function)Agda.Syntax.Concrete.Pretty
2 (Function)Agda.TypeChecking.Pretty
DBSizeExprAgda.TypeChecking.SizedTypes.Solve
DConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DDotAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dealAgda.Utils.List
deBruijnIndexAgda.Interaction.MakeCase
DeBruijnPatAgda.Termination.Monad, Agda.Termination.TermCheck
DeBruijnPat'Agda.Termination.Monad
DeBruijnPatsAgda.Termination.Monad
debug 
1 (Function)Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad
2 (Function)Agda.TypeChecking.SizedTypes.Utils
decDigitAgda.Utils.Char
Declaration 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
DeclarationExceptionAgda.Syntax.Concrete.Definitions
DeclarationPanicAgda.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
declsForPrimAgda.Compiler.MAlonzo.Primitives
decodeAgda.TypeChecking.Serialise
DecodedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
decodeFileAgda.TypeChecking.Serialise
decodeHashesAgda.TypeChecking.Serialise
decodeInterfaceAgda.TypeChecking.Serialise
decompressAgda.Interaction.Highlighting.Precise
DecorationAgda.Utils.Functor
decrAgda.Termination.Order
decrConfAgda.TypeChecking.Test.Generators
decreaseAgda.Termination.Order
decreasingAgda.Termination.Order
DeepSizeViewAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
deepSizeViewAgda.TypeChecking.SizedTypes
deepUnScopeAgda.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
defAccessAgda.Syntax.Info
defAppAgda.TypeChecking.Substitute
DefArgAgda.TypeChecking.Positivity
defArgInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defArgOccurrencesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defArgsAgda.TypeChecking.MetaVars.Occurs
DefaultAgda.Compiler.Epic.AuxAST
defaultArgAgda.Syntax.Common
defaultArgInfoAgda.Syntax.Common
defaultColoredArgAgda.Syntax.Common
defaultCutOffAgda.Interaction.Options
defaultDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultDisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultDomAgda.Syntax.Common
defaultFixityAgda.Syntax.Fixity
defaultFixity'Agda.Syntax.Fixity
defaultFlexibleVarAgda.TypeChecking.Rules.LHS.Problem
defaultFrequenciesAgda.TypeChecking.Test.Generators
defaultImportDirAgda.Syntax.Concrete
defaultInteractionOptionsAgda.Interaction.Options
defaultInteractionOutputCallbackAgda.Interaction.Response
defaultNamedArgAgda.Syntax.Common
defaultNotationAgda.Syntax.Notation
defaultOptionsAgda.Interaction.Options
defaultParseFlagsAgda.Syntax.Parser.Monad
defaultTerEnvAgda.Termination.Monad
defaultVerbosityAgda.Interaction.Options
defClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defColorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCopyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDelayed 
1 (Function)Agda.Compiler.Epic.Interface
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defEpicDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixityAgda.Syntax.Info
defFreqAgda.TypeChecking.Test.Generators
DefinedAgda.Syntax.Scope.Base
DefinedNameAgda.Syntax.Scope.Monad
DefInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
defInfoAgda.Syntax.Info
DefinitelyAgda.TypeChecking.Rules.LHS.Unify
DefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definition 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
DefinitionIsIrrelevantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definitions 
1 (Function)Agda.Compiler.Epic.Interface
2 (Function)Agda.Compiler.MAlonzo.Compiler
definitionSiteAgda.Interaction.Highlighting.Precise
defIsDataOrRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defIsRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defJSDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defMutualAgda.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
defNeedsCheckingAgda.TypeChecking.MetaVars.Occurs
DefNodeAgda.TypeChecking.Positivity
defNonterminatingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defnParsAgda.Compiler.Epic.Smashing
defOrVarAgda.TypeChecking.Rules.Term
DefPAgda.Syntax.Abstract
defPolarityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefShAgda.TypeChecking.Rules.LHS.Unify
defTypeAgda.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
dependentPolarityAgda.TypeChecking.Polarity
depthofvarAgda.Auto.CaseSplit
derefPtrAgda.Utils.Pointer, Agda.Syntax.Internal
DeserializationAgda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
destAgda.TypeChecking.SizedTypes.WarshallSolver
detecteliminandAgda.Auto.Syntax
detectsemiflexAgda.Auto.Syntax
dgetAgda.Utils.Functor
DiagonalAgda.Termination.SparseMatrix
diagonal 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.Termination.SparseMatrix
diffAgda.Compiler.Epic.Erasure
differenceAgda.Utils.HashMap
DifferentAritiesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DioidAgda.TypeChecking.SizedTypes.Utils
DirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirGeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DirLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dirToCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dirtyAgda.Utils.Update
disableDestructiveUpdateAgda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad
disableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Discard 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
discardAgda.Utils.QuickCheck
disjoinAgda.Utils.QuickCheck
DisplayAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayDebugMessageAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayFormAgda.TypeChecking.DisplayForm
displayFormsEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DisplayInfoAgda.Interaction.Response
displayRunningInfoAgda.Interaction.EmacsCommand
displayStatusAgda.Interaction.InteractionTop
DisplayTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_infoAgda.Interaction.InteractionTop
display_info'Agda.Interaction.EmacsCommand
DistAgda.Utils.Warshall
DistanceAgda.Utils.Warshall
distinctAgda.Utils.List
distributeFAgda.Utils.Functor
distributiveAgda.Utils.TestHelpers
divConfAgda.TypeChecking.Test.Generators
divPropSizeAgda.Utils.QuickCheck
DLubAgda.Syntax.Internal
dLubAgda.TypeChecking.Substitute
dmapAgda.Utils.Functor
Doc 
1 (Type/Class)Agda.Utils.Pretty
2 (Type/Class)Agda.TypeChecking.Pretty
doclosAgda.Auto.Syntax
doDefAgda.Syntax.Internal.Defs
DoDropAgda.Utils.Permutation
doDropAgda.Utils.Permutation
doesFileExistCaseSensitiveAgda.Utils.FileName
DoesNotConstructAnElementOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
doExpandLastAgda.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
domainFreeAgda.TypeChecking.Rules.Term
DomainFull 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
domColorsAgda.Syntax.Common
doMetaAgda.Syntax.Internal.Defs
domFromArgAgda.Syntax.Common
domHAgda.TypeChecking.Primitive
dominatedAgda.Utils.Favorites
DominatesAgda.Utils.Favorites
dominatorAgda.Utils.Favorites
domInfoAgda.Syntax.Common
domNAgda.TypeChecking.Primitive
DoneAgda.TypeChecking.CompiledClause
dontAssignMetasAgda.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
DontCutOffAgda.Termination.CutOff
dontDescendIntoAgda.Utils.Geniplate
dontEtaContractImplicitAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandInstanceArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dontExpandLastAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
DontKnow 
1 (Data Constructor)Agda.TypeChecking.Patterns.Match
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify
DontOpenAgda.Syntax.Concrete
dontReduceProjectionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
dontReifyInteractionPointsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontRunMetaOccursCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DontTouchMeAgda.Syntax.Translation.AbstractToConcrete
DontUseBoundNamesAgda.Syntax.Concrete.Operators
DoOpenAgda.Syntax.Concrete
DotAgda.Syntax.Concrete
DotFlexAgda.TypeChecking.Rules.LHS.Problem
DOtherSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DotMAgda.Interaction.Highlighting.Dot
DotP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Data Constructor)Agda.Syntax.Internal
DotPatternCtxAgda.Syntax.Fixity
DotPatternInstAgda.TypeChecking.Rules.LHS.Problem
dotPatternInstsAgda.TypeChecking.Rules.LHS
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
doubleQuotesAgda.Utils.Pretty
downFromAgda.Utils.List
doWorkOnTypesAgda.TypeChecking.Irrelevance
DPIAgda.TypeChecking.Rules.LHS.Problem
Drop 
1 (Type/Class)Agda.Utils.Permutation
2 (Data Constructor)Agda.Utils.Permutation
DropArgsAgda.TypeChecking.DropArgs
dropArgsAgda.TypeChecking.DropArgs
dropConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
dropDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
dropFromAgda.Utils.Permutation
drophidAgda.Auto.CaseSplit
dropIAgda.Syntax.Position
dropMoreAgda.Utils.Permutation
dropNAgda.Utils.Permutation
droppedPAgda.Utils.Permutation
dropProjElimsAgda.Syntax.Internal
dropSAgda.TypeChecking.Substitute
dropWhileMAgda.Utils.Monad
dryInstantiateAgda.Auto.NarrowingSearch
dsConnectionAgda.Interaction.Highlighting.Dot
DSizeInfAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeMetaAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
DSizeVarAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
dsModulesAgda.Interaction.Highlighting.Dot
dsNameSupplyAgda.Interaction.Highlighting.Dot
dsubnameAgda.Compiler.MAlonzo.Misc
DTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dummyAgda.Compiler.MAlonzo.Misc
dummyDomAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
dummyLambdaAgda.Compiler.JS.Compiler
DuplicateBuiltinBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateConstructorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DWithAppAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad