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

- 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

D | Agda.Auto.Options
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, Agda.Compiler.Backend
dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataCon | Agda.TypeChecking.Datatypes
dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataConstructor | Agda.Syntax.Reflected
DataDecl | Agda.Utils.Haskell.Syntax
DataDef |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
dataDefGeneralizedParams | Agda.Syntax.Abstract
DataDefParams |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
dataDefParams | Agda.Syntax.Abstract
dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataOrNew | Agda.Utils.Haskell.Syntax
DataOrRecord | Agda.Syntax.Common
DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataPathCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
datarecPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataSig |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataType | Agda.Utils.Haskell.Syntax
Datatype |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dbPatPerm | Agda.Syntax.Internal.Pattern
dbPatPerm' | Agda.Syntax.Internal.Pattern
DBPatVar |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
dbPatVarIndex | Agda.Syntax.Internal
dbPatVarName | Agda.Syntax.Internal
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, Agda.Compiler.Backend
DDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DDot | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Deadcode | Agda.Interaction.Highlighting.Precise
deadStandardOptions | Agda.Interaction.Options
deal | Agda.Utils.List
DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
debruijnNamedVar | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnPattern | Agda.Syntax.Internal
deBruijnVar | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
deBruijnView | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
debug | Agda.TypeChecking.SizedTypes.Utils
debugConstraints | Agda.TypeChecking.Constraints
debugPrintDecl | Agda.TypeChecking.Rules.Decl
decDigit | Agda.Utils.Char
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 | Agda.Syntax.Concrete.Definitions
DeclarationPanic | Agda.Syntax.Concrete.Definitions
DeclarationWarning | Agda.Syntax.Concrete.Definitions
declarationWarningName | 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
decode | Agda.TypeChecking.Serialise
DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
decodeFile | Agda.TypeChecking.Serialise
decodeHashes | Agda.TypeChecking.Serialise
decodeInterface | Agda.TypeChecking.Serialise
decomposeInterval | Agda.TypeChecking.Primitive
decomposeInterval' | Agda.TypeChecking.Primitive
decompress | Agda.Interaction.Highlighting.Precise
Decoration | Agda.Utils.Functor
Decr | Agda.Termination.Order
decr | Agda.Termination.Order
decrease | Agda.Termination.Order
decreasing | Agda.Termination.Order
deepEtaExpand | Agda.TypeChecking.EtaExpand
DeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
deepSizeView | Agda.TypeChecking.SizedTypes
deepUnscope | Agda.Syntax.Abstract.Views
deepUnscopeDecl | Agda.Syntax.Abstract.Views
deepUnscopeDecls | Agda.Syntax.Abstract.Views
Def |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
defAbstract |
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defAccess | Agda.Syntax.Info
defApp | Agda.TypeChecking.Substitute
DefArg | Agda.TypeChecking.Positivity.Occurrence
defArgGeneralizable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defArgs | Agda.TypeChecking.MetaVars.Occurs
Default | Agda.Utils.WithDefault
defaultAction | Agda.TypeChecking.CheckInternal
defaultAppInfo | Agda.Syntax.Info
defaultAppInfo_ | Agda.Syntax.Info
defaultArg | Agda.Syntax.Common
defaultArgDom | Agda.Syntax.Common
defaultArgInfo | Agda.Syntax.Common
DefaultCompute | Agda.Interaction.BasicOps
defaultCSSFile | Agda.Interaction.Highlighting.HTML
defaultCutOff | Agda.Interaction.Options
defaultDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultDom | Agda.Syntax.Common
defaultFixity | Agda.Syntax.Fixity
defaultGetConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetRewriteRulesFor | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGHCOptions | Agda.Compiler.MAlonzo.Compiler
defaultImportDir | Agda.Syntax.Common
defaultInteraction | Agda.Main
defaultInteractionOptions | Agda.Interaction.Options
defaultInteractionOutputCallback | Agda.Interaction.Response
defaultJSOptions | Agda.Compiler.JS.Compiler
defaultLibDir | Agda.Interaction.Options
defaultModality | Agda.Syntax.Common
defaultNamedArg | Agda.Syntax.Common
defaultNamedArgDom | Agda.Syntax.Common
defaultOptions | Agda.Interaction.Options
defaultParseFlags | Agda.Syntax.Parser.Monad
defaultPragmaOptions | Agda.Interaction.Options
defaultQuantity | Agda.Syntax.Common
defaultRelevance | Agda.Syntax.Common
defaultTerEnv | Agda.Termination.Monad
DefaultToInfty |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Solve
defaultUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultVerbosity | Agda.Interaction.Options
defaultWarningMode | Agda.Interaction.Options.Warnings
defaultWarningSet | Agda.Interaction.Options.Warnings
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCompilerPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCopy | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defFixity | Agda.Syntax.Info
defForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defGeneralizedParams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defineCompData | Agda.TypeChecking.Rules.Data
defineCompKitR | Agda.TypeChecking.Rules.Record
Defined | Agda.Syntax.Scope.Base
DefinedName | Agda.Syntax.Scope.Base
defineHCompForFields | Agda.TypeChecking.Rules.Data
defineProjections | Agda.TypeChecking.Rules.Data
defineTranspForFields | Agda.TypeChecking.Rules.Data
defineTranspOrHCompForFields | Agda.TypeChecking.Rules.Data
defineTranspOrHCompR | Agda.TypeChecking.Rules.Record
DefInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.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
definition |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
definition' | Agda.Compiler.JS.Compiler
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionSite |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
definitionSite | Agda.Interaction.Highlighting.Precise
defInjective | Agda.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
DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defJSDef | Agda.Compiler.JS.Compiler
defMacro | Agda.Syntax.Info
defMatchable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defMutual | Agda.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
defn | Agda.Compiler.JS.Syntax
DefName | Agda.Syntax.Scope.Base
defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs
defNoCompilation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefNode | Agda.TypeChecking.Positivity
defNonterminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defOrVar | Agda.TypeChecking.Rules.Term
DefP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
defParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefS | Agda.Syntax.Internal
defSiteAnchor | Agda.Interaction.Highlighting.Precise
defSiteHere | Agda.Interaction.Highlighting.Precise
defSiteModule | Agda.Interaction.Highlighting.Precise
defSitePos | Agda.Interaction.Highlighting.Precise
defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
4 (Function) | Agda.Utils.AssocList
delimiter | Agda.Utils.String
dependentPolarity | Agda.TypeChecking.Polarity
DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeprecationWarning_ | Agda.Interaction.Options.Warnings
depthofvar | Agda.Auto.CaseSplit
derefPtr | Agda.Utils.Pointer
Deriving | Agda.Utils.Haskell.Syntax
Deserialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
dest | Agda.TypeChecking.SizedTypes.WarshallSolver
desugarDoNotation | Agda.Syntax.DoNotation
detecteliminand | Agda.Auto.Syntax
detectIdentityFunctions | Agda.Compiler.Treeless.Identity
detectsemiflex | Agda.Auto.Syntax
dfFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dget | Agda.Utils.Functor
Diagonal | Agda.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
difference |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.IntSet.Infinite
differenceWith | Agda.Utils.HashMap
Dioid | Agda.TypeChecking.SizedTypes.Utils
Direct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirGeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DirLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dirToCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Dirty |
1 (Type/Class) | Agda.TypeChecking.Unquote
2 (Data Constructor) | Agda.TypeChecking.Unquote
dirty | Agda.Utils.Update
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DisallowedGeneralizeName | Agda.Syntax.Scope.Base
disallowGeneralizedVars | Agda.Syntax.Scope.Base
DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
disambiguateRecordFields | Agda.Interaction.Highlighting.Generate
discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional
Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayForm | Agda.TypeChecking.DisplayForm
displayFormArities | Agda.TypeChecking.DisplayForm
DisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DisplayInfo | Agda.Interaction.Response
DisplayPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
displayRunningInfo | Agda.Interaction.EmacsCommand
displayStatus | Agda.Interaction.InteractionTop
DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
display_info | Agda.Interaction.InteractionTop
display_info' | Agda.Interaction.EmacsCommand
distinct | Agda.Utils.List
distributeF | Agda.Utils.Functor
dmap | Agda.Utils.Functor
dname | Agda.Compiler.MAlonzo.Misc
DoBind | Agda.Syntax.Concrete
DoBlock | Agda.Syntax.Concrete
Doc |
1 (Type/Class) | Agda.Utils.Pretty
2 (Type/Class) | Agda.TypeChecking.Pretty
doc |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad
doclos | Agda.Auto.Syntax
doCompile | Agda.Compiler.Common
DocP | Agda.Utils.Parser.MemoisedCPS
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, Agda.Compiler.Backend
doExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoGeneralize | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoHComp | Agda.TypeChecking.Primitive
DoHighlightModuleContents | Agda.TypeChecking.Rules.Decl
DoLet | Agda.Syntax.Concrete
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
Domains | Agda.Utils.TypeLevel
Domains' | Agda.Utils.TypeLevel
doMeta | Agda.Syntax.Internal.Defs
domFinite | Agda.Syntax.Common
domFromArg | Agda.Syntax.Common
domFromNamedArg | Agda.Syntax.Common
domFromNamedArgName | Agda.TypeChecking.Substitute
domH | Agda.TypeChecking.Primitive
dominated | Agda.Utils.Favorites
Dominates | Agda.Utils.Favorites
dominator | Agda.Utils.Favorites
domInfo | Agda.Syntax.Common
domN | Agda.TypeChecking.Primitive
domName | Agda.Syntax.Common
Done |
1 (Data Constructor) | Agda.TypeChecking.CompiledClause
2 (Data Constructor) | Agda.Interaction.InteractionTop
DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser
dontAssignMetas | Agda.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
DontCutOff | Agda.Termination.CutOff
DontDefaultToInfty | Agda.TypeChecking.SizedTypes.Solve
dontDescendInto | Agda.Utils.Geniplate
DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl
DontKnow |
1 (Data Constructor) | Agda.TypeChecking.Patterns.Match
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify
3 (Data Constructor) | Agda.TypeChecking.Empty
DontOpen | Agda.Syntax.Concrete
DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile
DoOpen | Agda.Syntax.Concrete
DoQuoteTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
doQuoteTerm | Agda.TypeChecking.Rules.Term
DoStmt | Agda.Syntax.Concrete
Dot |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
DotFlex | Agda.TypeChecking.Rules.LHS.Problem
dotForcedPatterns | Agda.TypeChecking.Forcing
DoThen | Agda.Syntax.Concrete
DOtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DotM | Agda.Interaction.Highlighting.Dot
DotP |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
dotP | Agda.Syntax.Internal
DotPattern | Agda.TypeChecking.Rules.LHS.Problem
DotPatternCtx | Agda.Syntax.Fixity
dotPatternsToPatterns | Agda.TypeChecking.Patterns.Internal
DoTransp | Agda.TypeChecking.Primitive
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
doubleC | Agda.TypeChecking.Serialise.Base
doubleD | Agda.TypeChecking.Serialise.Base
doubleE | Agda.TypeChecking.Serialise.Base
doubleQuotes | Agda.Utils.Pretty
DoWarn |
1 (Type/Class) | Agda.Syntax.Concrete.Fixity
2 (Data Constructor) | Agda.Syntax.Concrete.Fixity
downFrom | Agda.Utils.List
Drop |
1 (Type/Class) | Agda.Utils.Permutation
2 (Data Constructor) | Agda.Utils.Permutation
DropArgs | Agda.TypeChecking.DropArgs
dropArgs | Agda.TypeChecking.DropArgs
dropCommon | Agda.Utils.List
dropConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropEnd | Agda.Utils.List
dropFrom | Agda.Utils.Permutation
drophid | Agda.Auto.CaseSplit
dropMore | Agda.Utils.Permutation
dropN | Agda.Utils.Permutation
dropParameters | Agda.TypeChecking.ReconstructParameters
droppedP | Agda.Utils.Permutation
droppedPars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dropS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
dropTopLevelModule | Agda.TypeChecking.Errors
dropWhileEndM | Agda.Utils.Monad
dropWhileM | Agda.Utils.Monad
dryInstantiate | Agda.Auto.NarrowingSearch
dsConnection | Agda.Interaction.Highlighting.Dot
DSizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DSizeMeta | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DSizeVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dsModules | Agda.Interaction.Highlighting.Dot
dsNameSupply | Agda.Interaction.Highlighting.Dot
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dtermToTerm | Agda.TypeChecking.DisplayForm
Dummy | Agda.Syntax.Internal
dummyDom | Agda.Syntax.Internal
dummyLevel | Agda.Syntax.Internal
dummyLevel' | Agda.Syntax.Internal
DummyS | Agda.Syntax.Internal
dummySort | Agda.Syntax.Internal
dummyTerm | Agda.Syntax.Internal
dummyTerm' | Agda.Syntax.Internal
dummyType | Agda.Syntax.Internal
duname | Agda.Compiler.MAlonzo.Misc
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateDefinition | Agda.Syntax.Concrete.Definitions
DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicatePrimitiveBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
duplicates | Agda.Utils.List
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend