Agda-2.6.2.2: 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.Compiler.Backend, Agda.TypeChecking.Monad
DataBlock | Agda.Syntax.Concrete.Definitions.Types
dataClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataCon | Agda.TypeChecking.Datatypes
dataCons | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataConstructor | Agda.Syntax.Reflected
DataDecl | Agda.Utils.Haskell.Syntax
DataDef |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Reflected
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
dataIxs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataName |
1 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor) | Agda.Syntax.Scope.Base
DataOrNew | Agda.Utils.Haskell.Syntax
DataOrRecord |
1 (Type/Class) | Agda.Syntax.Internal
2 (Type/Class) | Agda.TypeChecking.Rules.LHS
DataOrRecordModule | Agda.Syntax.Scope.Base
DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dataPathCons | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataRecOrFun | Agda.Syntax.Concrete.Definitions.Types
datarecPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DataSig |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
dataSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Solve
DCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DDot | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Deadcode | Agda.Interaction.Highlighting.Precise
deadStandardOptions | Agda.Interaction.Options
DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute
DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
Decl |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
DeclarationPanic | Agda.Syntax.Concrete.Definitions.Errors
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
DeclCont | Agda.Auto.Syntax
DeclInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
declName |
1 (Function) | Agda.Syntax.Concrete.Definitions.Types
2 (Function) | Agda.Syntax.Info
DeclNum | Agda.Syntax.Concrete.Definitions.Types
declRange | Agda.Syntax.Info
decode |
1 (Function) | Agda.TypeChecking.Serialise
2 (Function) | Agda.Interaction.JSON
decode' | Agda.Interaction.JSON
DecodedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
decomposeInterval | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
decomposeInterval' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
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.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Abstract
Def' | Agda.Syntax.Abstract
defAbstract |
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defAccess | Agda.Syntax.Info
defApp | Agda.TypeChecking.Substitute
DefArg | Agda.TypeChecking.Positivity.Occurrence
defArgGeneralizable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defArgs | Agda.TypeChecking.MetaVars.Occurs
Default | Agda.Utils.WithDefault
defaultAction | Agda.TypeChecking.CheckInternal
defaultAddCtx | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
defaultAddLetBinding' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
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.Compiler.Backend, Agda.TypeChecking.Monad
defaultCohesion | Agda.Syntax.Common
DefaultCompute | Agda.Interaction.Base
defaultCutOff | Agda.Termination.CutOff, Agda.Interaction.Options
defaultDefn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultDom | Agda.Syntax.Internal
defaultErased | Agda.Syntax.Common
defaultFixity | Agda.Syntax.Common
defaultGetConstInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
defaultGetRewriteRulesFor | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
defaultGetVerbosity | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defaultGHCFlags | Agda.Compiler.MAlonzo.Compiler
defaultImportDir | Agda.Syntax.Common
defaultInteractionOptions | Agda.Interaction.Options
defaultInteractionOutputCallback | Agda.Interaction.Response
defaultInteractor | Agda.Main
defaultIsDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
defaultOpenLevelsToZero | Agda.TypeChecking.Level.Solve
defaultOptions |
1 (Function) | Agda.Interaction.Options
2 (Function) | Agda.Interaction.JSON
defaultParseFlags | Agda.Syntax.Parser.Monad
defaultPatternInfo | Agda.Syntax.Internal
defaultPragmaOptions | Agda.Interaction.Options
DefaultProjectConfig | Agda.Interaction.Library.Base, Agda.Interaction.Library
defaultQuantity | Agda.Syntax.Common
defaultRelevance | Agda.Syntax.Common
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.Compiler.Backend, Agda.TypeChecking.Monad
defaultVerbosity | Agda.Interaction.Options
defaultWarningMode | Agda.Interaction.Options.Warnings
defaultWarningSet | Agda.Interaction.Options.Warnings
defBlocked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defClauses | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompiled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCompilerPragmas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defConstructors | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defCopy | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defDelayed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defDisplay | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defFixity | Agda.Syntax.Info
defForced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defGeneralizedParams | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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 (Data Constructor) | Agda.Syntax.Info
2 (Type/Class) | Agda.Syntax.Abstract
defInfo | Agda.Syntax.Info
DefInfo' | Agda.Syntax.Info
definitelyNonRecursive_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
Definition |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class) | Agda.Syntax.Reflected
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
definition |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
definition' | Agda.Compiler.JS.Compiler
definitionCheck | Agda.TypeChecking.MetaVars.Occurs
DefinitionIsErased | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Definitions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
defInstance |
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defInverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defIsRecord | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defJSDef | Agda.Compiler.JS.Compiler
defLanguage | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defMacro | Agda.Syntax.Info
defMatchable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defMutual | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Defn |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defn | Agda.Compiler.JS.Syntax
defName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs
defNoCompilation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefNode | Agda.TypeChecking.Positivity
defNonterminating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defOrVar | Agda.TypeChecking.Rules.Term
DefP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
defParameters | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defPolarity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DefS | Agda.Syntax.Internal
defSiteAnchor | Agda.Interaction.Highlighting.Precise
defSiteHere | Agda.Interaction.Highlighting.Precise
defSiteModule | Agda.Interaction.Highlighting.Precise
defSitePos | Agda.Interaction.Highlighting.Precise
defTactic | Agda.Syntax.Info
defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
defType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Delayed |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
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.SmallSet
3 (Function) | Agda.Utils.Trie
4 (Function) | Agda.Utils.AssocList
delimiter | Agda.Utils.String
deLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dependencySortMetas | Agda.TypeChecking.MetaVars
DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
dfPats | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dfPatternVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dfRHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
didYouMean | Agda.TypeChecking.Pretty.Warning
difference |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.IntSet.Infinite
3 (Function) | Agda.Utils.SmallSet
Dioid | Agda.TypeChecking.SizedTypes.Utils
Direct | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirGeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DirLeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dirToCmp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Dirty |
1 (Type/Class) | Agda.TypeChecking.Unquote
2 (Data Constructor) | Agda.TypeChecking.Unquote
dirty | Agda.Utils.Update
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisallowedGeneralizeName | Agda.Syntax.Scope.Base
disallowGeneralizedVars | Agda.Syntax.Scope.Base
DisambiguatedName |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
disambiguateRecordFields | Agda.Interaction.Highlighting.Generate
discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional
Display | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayForm | Agda.TypeChecking.DisplayForm
DisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.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
doclos | Agda.Auto.Syntax
doCompile | Agda.Compiler.Common
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.Compiler.Backend, Agda.TypeChecking.Monad
doExpandLast | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
DoGeneralize | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DoHComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
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
doMeta | Agda.Syntax.Internal.Defs
domFinite | Agda.Syntax.Internal
domFromArg | Agda.Syntax.Internal
domFromNamedArg | Agda.Syntax.Internal
domFromNamedArgName | Agda.TypeChecking.Substitute
domH | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
dominated | Agda.Utils.Favorites
Dominates | Agda.Utils.Favorites
dominator | Agda.Utils.Favorites
domInfo | Agda.Syntax.Internal
domN | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
domName | Agda.Syntax.Internal
domOfBV | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
domTactic | Agda.Syntax.Internal
Done |
1 (Data Constructor) | Agda.TypeChecking.CompiledClause
2 (Data Constructor) | Agda.Interaction.Base
DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser
dontAssignMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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
DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dontExpandLast | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl
DontKnow | Agda.TypeChecking.Patterns.Match
DontOpen | Agda.Syntax.Concrete
DontReduceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile
DontWakeUp | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
DoOpen | Agda.Syntax.Concrete
DoQuoteTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
dotBackend | Agda.Interaction.Highlighting.Dot
DotFlex | Agda.TypeChecking.Rules.LHS.Problem
DoThen | Agda.Syntax.Concrete
DOtherSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DotNetTime |
1 (Type/Class) | Agda.Interaction.JSON
2 (Data Constructor) | Agda.Interaction.JSON
DotP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Abstract
dotP | Agda.Syntax.Internal
DotPattern | Agda.TypeChecking.Rules.LHS.Problem
DotPatternCtx | Agda.Syntax.Fixity
dotPatterns | Agda.TypeChecking.Rules.LHS.Problem
dotPatternsToPatterns | Agda.TypeChecking.Patterns.Internal
DoTransp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
DottedPattern | Agda.Interaction.Highlighting.Precise
Double | Agda.Compiler.JS.Syntax
double | Agda.Utils.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
doubleblock | Agda.Auto.NarrowingSearch
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.Utils.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 | Agda.Utils.List1
DropArgs | Agda.TypeChecking.DropArgs
dropArgs | Agda.TypeChecking.DropArgs
dropCommon | Agda.Utils.List
dropConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
dropDecodedModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
dropS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
dropTopLevelModule | Agda.TypeChecking.Errors
dropTypeAndModality | Agda.Syntax.Concrete
dropWhile | Agda.Utils.List1
dropWhileEndM | Agda.Utils.Monad
dropWhileM | Agda.Utils.Monad
dryInstantiate | Agda.Auto.NarrowingSearch
DSizeInf | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DSizeMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DSizeVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
DTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateDefinition | Agda.Syntax.Concrete.Definitions.Errors
DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateFieldsWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateFieldsWarning_ | Agda.Interaction.Options.Warnings
DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicatePrimitiveBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
duplicates | Agda.Utils.List
DuplicateUsing | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
DuplicateUsing_ | Agda.Interaction.Options.Warnings
DWithApp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
dwLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
dwWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions