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

Data | Agda.Syntax.Concrete
dataAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataDecls | Agda.Compiler.Epic.CompileState
DataDef |
1 (Data Constructor) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions
dataHsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataInfo | Agda.TypeChecking.Datatypes
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify
dataParameters | Agda.Compiler.Epic.Forcing
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Datatype |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DatatypeInfo | Agda.TypeChecking.Datatypes
datatypeIxs | Agda.TypeChecking.Datatypes
datatypeIxTel | Agda.TypeChecking.Datatypes
datatypeName | Agda.TypeChecking.Datatypes
datatypePars | Agda.TypeChecking.Datatypes
datatypeParTel | Agda.TypeChecking.Datatypes
deBruijnIndex | Agda.Interaction.MakeCase
DeBruijnPat | Agda.Termination.TermCheck
debug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad
decDigit | Agda.Utils.Char
Declaration |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
DeclarationException | Agda.Syntax.Concrete.Definitions
DeclarationPanic | Agda.Syntax.Concrete.Definitions
DeclCont | Agda.Auto.Syntax
DeclInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
declName | Agda.Syntax.Info
declRange | Agda.Syntax.Info
declsForPrim | Agda.Compiler.MAlonzo.Primitives
decode | Agda.TypeChecking.Serialise
DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
decodeFile | Agda.TypeChecking.Serialise
decompress | Agda.Interaction.Highlighting.Precise
decr | Agda.Termination.CallGraph
decrConf | Agda.TypeChecking.Test.Generators
decreasing | Agda.Termination.CallGraph
Def |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
defAbstract |
1 (Function) | Agda.Syntax.Info
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defAccess | Agda.Syntax.Info
DefArg | Agda.TypeChecking.Positivity
Default | Agda.Compiler.Epic.AuxAST
defaultArg | Agda.Syntax.Common
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defaultFixity | Agda.Syntax.Fixity
defaultFixity' | Agda.Syntax.Fixity
defaultFrequencies | Agda.TypeChecking.Test.Generators
defaultImportDir | Agda.Syntax.Concrete
defaultNotation | Agda.Syntax.Notation
defaultOptions | Agda.Interaction.Options
defaultParseFlags | Agda.Syntax.Parser.Monad
defaultVerbosity | Agda.Interaction.Options
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defDelayed |
1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Function) | Agda.Compiler.Epic.CompileState
defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defFixity | Agda.Syntax.Info
defFreq | Agda.TypeChecking.Test.Generators
DefinedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
DefInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
defInfo | Agda.Syntax.Info
Definition |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definition | Agda.Compiler.MAlonzo.Compiler
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
definitions |
1 (Function) | Agda.Compiler.Epic.CompileState
2 (Function) | Agda.Compiler.MAlonzo.Compiler
definitionSite | Agda.Interaction.Highlighting.Precise
defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Defn |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefName |
1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class) | Agda.TypeChecking.Test.Generators
3 (Data Constructor) | Agda.TypeChecking.Test.Generators
defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DefNode | Agda.TypeChecking.Positivity
DefP | Agda.Syntax.Abstract
defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Delayed |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Dependent | Agda.Interaction.GhciTop
depthofvar | Agda.Auto.CaseSplit
deref | Agda.Utils.Pointer
detecteliminand | Agda.Auto.Syntax
detectsemiflex | Agda.Auto.Syntax
diagonal |
1 (Function) | Agda.Termination.SparseMatrix
2 (Function) | Agda.Termination.Matrix
DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
disjoin | Agda.Utils.QuickCheck
Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayErrorAndExit | Agda.Interaction.GhciTop
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
displayForm | Agda.TypeChecking.DisplayForm
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
displayStatus | Agda.Interaction.GhciTop
DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
display_info | Agda.Interaction.GhciTop
display_info' | Agda.Interaction.GhciTop
display_infoD | Agda.Interaction.GhciTop
Dist | Agda.Utils.Warshall
Distance | Agda.Utils.Warshall
distinct | Agda.Utils.List
divConf | Agda.TypeChecking.Test.Generators
DLub | Agda.Syntax.Internal
dLub | Agda.TypeChecking.Substitute
Doc |
1 (Type/Class) | Agda.Utils.Pretty
2 (Type/Class) | Agda.TypeChecking.Pretty
doclos | Agda.Auto.Syntax
DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
doEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DomainFree |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
DomainFull |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Done | Agda.TypeChecking.CompiledClause
DontCare |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
dontCare | Agda.Auto.Syntax
dontEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontExpandLast | Agda.TypeChecking.Rules.Term
DontKnow |
1 (Data Constructor) | Agda.TypeChecking.Patterns.Match
2 (Data Constructor) | Agda.Compiler.Epic.Erasure
3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify
DontOpen | Agda.Syntax.Concrete
dontReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
DoOpen | Agda.Syntax.Concrete
Dot | Agda.Syntax.Concrete
DotP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Abstract
DotPatternCtx | Agda.Syntax.Fixity
DotPatternInst | Agda.TypeChecking.Rules.LHS
dotPatternInsts | Agda.TypeChecking.Rules.LHS
DottedPattern | Agda.Interaction.Highlighting.Precise
DotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
dotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
double | Agda.Utils.Pretty
doubleblock | Agda.Auto.NarrowingSearch
doubleQuotes | Agda.Utils.Pretty
DPI | Agda.TypeChecking.Rules.LHS
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
drophid | Agda.Auto.CaseSplit
dropI | Agda.Syntax.Position, Agda.Interaction.GhciTop
dryInstantiate | Agda.Auto.NarrowingSearch
dsubname | Agda.Compiler.MAlonzo.Misc
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
dummy | Agda.Compiler.MAlonzo.Misc
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad