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 |
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 |
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dataName | Agda.Compiler.Alonzo.Names |
dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify |
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 |
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 |
decrConf | Agda.TypeChecking.Test.Generators |
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 |
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defaultFixity | Agda.Syntax.Fixity |
defaultFrequencies | Agda.TypeChecking.Test.Generators |
defaultImportDir | Agda.Syntax.Concrete |
defaultOptions | Agda.Interaction.Options |
defaultParseFlags | Agda.Syntax.Parser.Monad |
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
definitions | Agda.Compiler.MAlonzo.Compiler |
definitionSite | Agda.Interaction.Highlighting.Precise |
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 |
Defs | Agda.Compiler.Alonzo.PatternMonad |
defs | Agda.Compiler.Alonzo.PatternMonad |
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 |
DependentPatternMatchingOnCodata | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
deref | Agda.Utils.Pointer |
dfName | Agda.Compiler.Alonzo.Names |
dfNameSub | Agda.Compiler.Alonzo.Names |
dfQName | Agda.Compiler.Alonzo.Names |
dfQStr | Agda.Compiler.Alonzo.Names |
dfStr | Agda.Compiler.Alonzo.Names |
diagonal | Agda.Termination.Matrix |
DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
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.Typecheck |
DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, 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 |
DontExpandLast | Agda.TypeChecking.Rules.Term |
DontKnow | |
1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
2 (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 |
dopat | Agda.Auto.Typecheck |
dopats | Agda.Auto.Typecheck |
dorule | Agda.Auto.Typecheck |
dorules | Agda.Auto.Typecheck |
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 |
dropArgs | Agda.Compiler.Agate.Common |
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
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 |
dummyLoc | Agda.Compiler.Alonzo.Haskell |
DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |