Agda-2.8.0: 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

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
DataBlock | Agda.Syntax.Concrete.Definitions.Types
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
DataDefS | Agda.Syntax.Abstract
dataFiles | Agda.Setup.DataFiles
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataName |
1 (Data Constructor) | Agda.Syntax.Scope.Base
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
DataName_ | Agda.Interaction.Options.Errors
DataOrNew | Agda.Utils.Haskell.Syntax
DataOrRecord |
1 (Type/Class) | Agda.Syntax.Internal
2 (Type/Class) | Agda.TypeChecking.Rules.LHS
DataOrRecord' | Agda.Syntax.Internal
DataOrRecordE | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataOrRecordModule | Agda.Syntax.Scope.Base
DataOrRecord_ | Agda.Syntax.Internal
DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataOrRecSigData |
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
DataOrRecSigDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataPath | Agda.Setup.DataFiles
dataPathCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataRecOrFun | Agda.Syntax.Concrete.Definitions.Types
dataRecOrFunString | Agda.Interaction.Options.Errors
DataRecOrFun_ | Agda.Interaction.Options.Errors
datarecPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataSig |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
DataSigS | Agda.Syntax.Abstract
DataSort | Agda.Interaction.Base
dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dataTranspIx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DataType | Agda.Utils.Haskell.Syntax
Datatype |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DatatypeData |
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
DatatypeDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DatatypeIndexPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DatatypeIndexPolarity_ | Agda.Interaction.Options.Errors
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.Glyph, Agda.Syntax.Concrete.Pretty
2 (Function) | Agda.TypeChecking.Pretty
DBSizeExpr | Agda.TypeChecking.SizedTypes.Syntax
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
DDot' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Deadcode | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
DeadCodeReachable | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
deadStandardOptions | Agda.Interaction.Options
DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeBruijnIndexOutOfScope_ | Agda.Interaction.Options.Errors
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
debugClause | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
debugConstraints | Agda.TypeChecking.Constraints
debugPrintDecl | Agda.TypeChecking.Rules.Decl
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 |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationException | Agda.Syntax.Concrete.Definitions.Monad
DeclarationException' | Agda.Syntax.Concrete.Definitions.Errors
declarationExceptionName | Agda.TypeChecking.Errors.Names
declarationExceptionNameString | Agda.Interaction.Options.Errors
declarationExceptionString | Agda.Syntax.Concrete.Definitions.Errors
DeclarationException_ | Agda.Interaction.Options.Errors
DeclarationsAfterTopLevelModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeclarationsAfterTopLevelModule_ | Agda.Interaction.Options.Errors
DeclarationSpine | Agda.Syntax.Abstract
declarationSpine | Agda.Syntax.Abstract
DeclarationWarning |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationWarning | Agda.Syntax.Concrete.Definitions.Monad
DeclarationWarning' | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationWarning' | Agda.Syntax.Concrete.Definitions.Monad
declarationWarningName | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
declarationWarningName' | Agda.Syntax.Concrete.Definitions.Errors
DeclaredNames | Agda.Syntax.Abstract.Views
declaredNames | Agda.Syntax.Abstract.Views
DeclInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
declName |
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.Syntax.Concrete.Definitions.Types
DeclNum | Agda.Syntax.Concrete.Definitions.Types
declRange | Agda.Syntax.Info
decode |
1 (Function) | Agda.Interaction.JSON
2 (Function) | Agda.TypeChecking.Serialise
decode' | Agda.Interaction.JSON
DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
decodeFile | Agda.TypeChecking.Serialise
decodeFileStrict | Agda.Interaction.JSON
decodeFileStrict' | Agda.Interaction.JSON
decodeHashes | Agda.TypeChecking.Serialise
decodeInterface | Agda.TypeChecking.Serialise
decodeStrict | Agda.Interaction.JSON
decodeStrict' | Agda.Interaction.JSON
decodeStrictText | Agda.Interaction.JSON
decomposeInterval | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
decomposeInterval' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
decorate | Agda.Interaction.InteractionTop
Decoration | Agda.Utils.Functor
Decr | Agda.Termination.Order
decr | Agda.Termination.Order
decrease | Agda.Termination.Order
decreasing | Agda.Termination.Order
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
deException | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
Def |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Abstract
Def' | 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
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
defaultAddCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultAddLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultAnnotation | Agda.Syntax.Common
defaultAppInfo | Agda.Syntax.Info
defaultAppInfo_ | Agda.Syntax.Info
defaultArg | Agda.Syntax.Common
defaultArgDom | Agda.Syntax.Internal
defaultArgInfo | Agda.Syntax.Common
defaultAxiom | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultBuildDoStmt | Agda.Syntax.Parser.Helpers
defaultCheckModality | Agda.Syntax.Common
defaultCohesion | Agda.Syntax.Common
DefaultCompute | Agda.Interaction.Base
defaultCutOff | Agda.Termination.CutOff, 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.Internal
defaultErased | Agda.Syntax.Common
defaultErrorNameString | Agda.Interaction.Options.Errors
defaultFixity | Agda.Syntax.Common
defaultGetConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetProfileOptions | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetRewriteRulesFor | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultGetVerbosity | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultImportDir | Agda.Syntax.Common
defaultInteractionOptions | Agda.Interaction.Options
defaultInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultInteractor | Agda.Main
defaultIrrelevantArg | Agda.Syntax.Parser.Helpers
defaultIrrelevantArgInfo | Agda.Syntax.Common
defaultIsDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultJSONKeyOptions | Agda.Interaction.JSON
defaultJSOptions | Agda.Compiler.JS.Compiler
defaultLevelsToZero | Agda.TypeChecking.Level.Solve
defaultLock | Agda.Syntax.Common
defaultModality | Agda.Syntax.Common
defaultNamedArg | Agda.Syntax.Common
defaultNamedArgDom | Agda.Syntax.Internal
defaultNowDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defaultOpenLevelsToZero | Agda.TypeChecking.Level.Solve
defaultOptions |
1 (Function) | Agda.Interaction.JSON
2 (Function) | Agda.Interaction.Options
DefaultOverlap | Agda.Syntax.Common
defaultPageGen | Agda.Interaction.Highlighting.HTML.Base
defaultParseFlags | Agda.Syntax.Parser.Monad
defaultPatternInfo | Agda.Syntax.Internal
defaultPolarity | Agda.Syntax.Common
defaultPragmaOptions | Agda.Interaction.Options
DefaultProjectConfig | Agda.Interaction.Library.Base, Agda.Interaction.Library
defaultQuantity | Agda.Syntax.Common
defaultRelevance | Agda.Syntax.Common
defaultShapeIrrelevantArg | Agda.Syntax.Parser.Helpers
defaultTaggedObject | Agda.Interaction.JSON
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
defaultWarningMode | Agda.Interaction.Options.Warnings
defaultWarningSet | Agda.Interaction.Options.Warnings
defBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
defCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defCopy | 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
defineConClause | Agda.TypeChecking.Rules.Data
Defined | Agda.Syntax.Scope.Base
DefineDataNotData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefineDataNotData_ | Agda.Interaction.Options.Errors
DefinedName | Agda.Syntax.Scope.Base
defineHCompForFields | Agda.TypeChecking.Rules.Data
defineKanOperationForFields | Agda.TypeChecking.Rules.Data
defineKanOperationR | Agda.TypeChecking.Rules.Record
defineProjections | Agda.TypeChecking.Rules.Data
defineTranspForFields | Agda.TypeChecking.Rules.Data
defineTranspFun | Agda.TypeChecking.Rules.Data
defineTranspIx | Agda.TypeChecking.Rules.Data
DefInfo |
1 (Data Constructor) | Agda.Syntax.Info
2 (Type/Class) | Agda.Syntax.Abstract
defInfo | 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 | Agda.Compiler.JS.Compiler
definition' | Agda.Compiler.JS.Compiler
definitionCheck | Agda.TypeChecking.MetaVars.Occurs
DefinitionInDifferentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionInDifferentModule_ | Agda.Interaction.Options.Errors
DefinitionIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionIsErased_ | Agda.Interaction.Options.Errors
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionIsIrrelevant_ | Agda.Interaction.Options.Errors
Definitions |
1 (Data Constructor) | Agda.Utils.ProfileOptions
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DefinitionSite |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
definitionSite | Agda.Syntax.Common.Aspect, 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
DefInsteadOfCon_ | Agda.Interaction.Options.Errors
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
defLanguage | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defNameKinds | Agda.Syntax.Scope.Base
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
defOpaque |
1 (Function) | Agda.Syntax.Info
2 (Function) | 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
DefS | Agda.Syntax.Internal
defSiteAnchor | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSiteHere | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSiteModule | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defSitePos | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
defTactic | Agda.Syntax.Info
defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DelayedMerge |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
delayedMergeInvariant | Agda.Interaction.Highlighting.Precise
delete |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.BoolSet
5 (Function) | Agda.Utils.AssocList
6 (Function) | Agda.Utils.SmallSet
7 (Function) | Agda.Utils.Trie
deleteAt |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.TypeChecking.Rules.LHS.Unify.Types
deleteFindMax |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
deleteFindMin |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
deleteFromDT | Agda.TypeChecking.DiscrimTree
deleteLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
deleteMax |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
deleteMin |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
deleteRight | Agda.TypeChecking.Rules.LHS.Unify.Types
deleteType | Agda.TypeChecking.Rules.LHS.Unify.Types
Deletion | Agda.TypeChecking.Rules.LHS.Unify.Types
delimiter | Agda.Utils.String
deLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dependencySortMetas | Agda.TypeChecking.MetaVars
DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DeprecationWarning_ | Agda.Interaction.Options.Warnings
Deriving | Agda.Utils.Haskell.Syntax
Deserialization | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
dest | Agda.TypeChecking.SizedTypes.WarshallSolver
desugarDoNotation | Agda.Syntax.DoNotation
detectIdentityFunctions | Agda.Compiler.Treeless.Identity
dfPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dfPatternVars | 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
DiagnosticsColours | Agda.Interaction.Options
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.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.BoolSet
5 (Function) | Agda.Utils.IntSet.Infinite
6 (Function) | Agda.Utils.SmallSet
differenceWith | Agda.Utils.Map1
differenceWithKey | Agda.Utils.Map1
DifferentOpaque | Agda.Syntax.Common
Dioid | Agda.TypeChecking.SizedTypes.Utils
Direct | Agda.TypeChecking.Monad.Base.Types, 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
DisallowedInterleavedMutual | Agda.Syntax.Concrete.Definitions.Errors
DisallowedInterleavedMutual_ | Agda.Interaction.Options.Errors
disallowGeneralizedVars | Agda.Syntax.Scope.Base
DisambiguateConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
disambiguateConstructor' | Agda.TypeChecking.Rules.Application
DisambiguatedName |
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
DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
disambiguateRecordFields | Agda.Interaction.Highlighting.Generate
discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional
DiscrimTree | Agda.TypeChecking.DiscrimTree.Types
disjoint |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
disjointUnion | Agda.Utils.Set1
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
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
DisplayInfo_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response
DisplayLHS | Agda.Syntax.Common
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.Syntax.Common.Pretty
2 (Type/Class) | Agda.Compiler.JS.Pretty
3 (Data Constructor) | Agda.Compiler.JS.Pretty
4 (Type/Class) | Agda.TypeChecking.Pretty
doc |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad
doCompile | Agda.Compiler.Common
doCompile' | Agda.Compiler.Common
DocP | Agda.Utils.Parser.MemoisedCPS
docsUrl | Agda.Version
doDef | Agda.Syntax.Internal.Defs
DoDrop | Agda.Utils.Permutation
doDrop | Agda.Utils.Permutation
doesFileExistCaseSensitive | Agda.Utils.FileName
DoesNotCorrespondToValidModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoesNotMentionTicks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoesNotMentionTicks_ | Agda.Interaction.Options.Errors
DoesNotTargetRewriteRelation | 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
doGlueKanOp | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DoHComp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
doHCompUKanOp | Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DoHighlightModuleContents | Agda.TypeChecking.Rules.Decl
DoLet | Agda.Syntax.Concrete
Dom |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
Dom' | 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
Domains | Agda.Utils.TypeLevel
Domains' | Agda.Utils.TypeLevel
domainUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
doMeta | Agda.Syntax.Internal.Defs
domFromArg | Agda.Syntax.Internal
domFromNamedArg | Agda.Syntax.Internal
domFromNamedArgName | Agda.TypeChecking.Substitute
domH | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
dominated | Agda.Utils.Favorites
Dominates | Agda.Utils.Favorites
dominator | Agda.Utils.Favorites
domInfo | Agda.Syntax.Internal
domIsFinite | Agda.Syntax.Internal
domN | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
domName | Agda.Syntax.Internal
domOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
domTactic | Agda.Syntax.Internal
Done |
1 (Data Constructor) | Agda.TypeChecking.CompiledClause
2 (Data Constructor) | Agda.Interaction.Base
DoneDT | Agda.TypeChecking.DiscrimTree.Types
DoNotationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DoNotationError_ | Agda.Interaction.Options.Errors
DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser
dontAssignMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontCare |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
dontCare | Agda.Syntax.Internal
DontCutOff | Agda.Termination.CutOff
DontDefaultToInfty | Agda.TypeChecking.SizedTypes.Solve
DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dontFoldLetBindings | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl
DontKnow | Agda.TypeChecking.Patterns.Match
DontOpen | Agda.Syntax.Concrete
DontReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile
DontWakeUp | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
DoOpen | Agda.Syntax.Concrete
doPathPKanOp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
doPiKanOp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
dot | Agda.Syntax.Common.Pretty
dotBackend | Agda.Interaction.Highlighting.Dot.Backend, Agda.Interaction.Highlighting.Dot
DotFlex | Agda.TypeChecking.Rules.LHS.Problem
DotGraph | Agda.Interaction.Highlighting.Dot.Base
DoThen | Agda.Syntax.Concrete
DOtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DotNetTime |
1 (Type/Class) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Interaction.JSON
DotP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Abstract
dotP | Agda.Syntax.Internal
DotPattern | Agda.TypeChecking.Rules.LHS.Problem
DotPatternCtx | Agda.Syntax.Fixity
DotPatternInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DotPatternInPatternSynonym_ | Agda.Interaction.Options.Errors
dotPatterns | Agda.TypeChecking.Rules.LHS.Problem
dotPatternsToPatterns | Agda.TypeChecking.Patterns.Internal
DoTransp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
DottedPattern | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
Double | Agda.Compiler.JS.Syntax
double | Agda.Syntax.Common.Pretty
doubleACos | Agda.Utils.Float
doubleACosh | Agda.Utils.Float
doubleASin | Agda.Utils.Float
doubleASinh | Agda.Utils.Float
doubleATan | Agda.Utils.Float
doubleATan2 | Agda.Utils.Float
doubleATanh | Agda.Utils.Float
doubleC | Agda.TypeChecking.Serialise.Base
doubleCeiling | Agda.Utils.Float
doubleCos | Agda.Utils.Float
doubleCosh | Agda.Utils.Float
doubleD | Agda.TypeChecking.Serialise.Base
doubleDecode | Agda.Utils.Float
doubleDenotEq | Agda.Utils.Float
doubleDenotOrd | Agda.Utils.Float
doubleDiv | Agda.Utils.Float
DoubleDot | Agda.Syntax.Concrete
doubleE | Agda.TypeChecking.Serialise.Base
doubleEncode | Agda.Utils.Float
doubleEq | Agda.Utils.Float
doubleExp | Agda.Utils.Float
doubleFloor | Agda.Utils.Float
doubleLe | Agda.Utils.Float
doubleLog | Agda.Utils.Float
doubleLt | Agda.Utils.Float
doubleMinus | Agda.Utils.Float
doubleNegate | Agda.Utils.Float
doublePlus | Agda.Utils.Float
doublePow | Agda.Utils.Float
doubleQuotes |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
doubleRound | Agda.Utils.Float
doubleSin | Agda.Utils.Float
doubleSinh | Agda.Utils.Float
doubleSqrt | Agda.Utils.Float
doubleTan | Agda.Utils.Float
doubleTanh | Agda.Utils.Float
doubleTimes | Agda.Utils.Float
doubleToRatio | Agda.Utils.Float
doubleToWord64 | Agda.Utils.Float
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
drop |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
dropAgdaExtension | Agda.Interaction.FindFile
DropArgs | Agda.TypeChecking.DropArgs
dropArgs | Agda.TypeChecking.DropArgs
dropAt | Agda.TypeChecking.Rules.LHS.Unify.Types
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 |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.Permutation
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
dropTypeAndModality | Agda.Syntax.Concrete
dropWhile | Agda.Utils.List1
dropWhileAntitone |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
dropWhileEndM | Agda.Utils.Monad
dropWhileM | Agda.Utils.Monad
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
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DTerm' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Dummy | Agda.Syntax.Internal
dummyDom | Agda.Syntax.Internal
dummyLevel | Agda.Syntax.Internal
dummyLocName | Agda.Syntax.Internal
DummyS | Agda.Syntax.Internal
dummySort | Agda.Syntax.Internal
dummyTerm | Agda.Syntax.Internal
DummyTermKind | Agda.Syntax.Internal
dummyTermWith | Agda.Syntax.Internal
dummyType | Agda.Syntax.Internal
duname | Agda.Compiler.MAlonzo.Misc
DuplicateAnonDeclaration | Agda.Syntax.Concrete.Definitions.Errors
DuplicateAnonDeclaration_ | Agda.Interaction.Options.Errors
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateBuiltinBinding_ | Agda.Interaction.Options.Errors
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateConstructors_ | Agda.Interaction.Options.Errors
DuplicateDefinition | Agda.Syntax.Concrete.Definitions.Errors
DuplicateDefinition_ | Agda.Interaction.Options.Errors
DuplicateExecutable | Agda.Interaction.Library.Base
DuplicateFields |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Warning
2 (Data Constructor) | Agda.Interaction.Library.Base
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateFields_ |
1 (Data Constructor) | Agda.Interaction.Options.Warnings
2 (Data Constructor) | Agda.Interaction.Options.Errors
DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateImports_ | Agda.Interaction.Options.Errors
DuplicateOverlapPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateOverlapPragma_ | Agda.Interaction.Options.Errors
DuplicatePrimitiveBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicatePrimitiveBinding_ | Agda.Interaction.Options.Errors
DuplicateRecordDirective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateRecordDirective_ | Agda.Interaction.Options.Warnings
DuplicateRewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateRewriteRule_ | Agda.Interaction.Options.Warnings
duplicates | Agda.Utils.List
DuplicateUsing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
DuplicateUsing_ | Agda.Interaction.Options.Warnings
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
dwLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dwWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions