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 |
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 |
dataOrRecordType' | Agda.TypeChecking.Rules.LHS.Unify |
dataOrRecordTypeHH | Agda.TypeChecking.Rules.LHS.Unify |
dataParameters | Agda.Compiler.Epic.Forcing |
dataParametersTCM | Agda.Compiler.Epic.Forcing |
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dataPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DataSig | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
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 |
dbraces | |
1 (Function) | Agda.Syntax.Concrete.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
DCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DDot | 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 |
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 |
defArgs | Agda.TypeChecking.MetaVars.Occurs |
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 |
defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defDelayed | |
1 (Function) | Agda.Compiler.Epic.Interface |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DefElim | Agda.TypeChecking.Eliminators |
defEpicDef | 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 |
Definitely | Agda.TypeChecking.Rules.LHS.Unify |
Definition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
definition | |
1 (Function) | Agda.Compiler.MAlonzo.Compiler |
2 (Function) | Agda.Compiler.JS.Compiler |
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
definitions | |
1 (Function) | Agda.Compiler.Epic.Interface |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
definitionSite | Agda.Interaction.Highlighting.Precise |
defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defJSDef | 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 |
defn | |
1 (Function) | Agda.Compiler.JS.Syntax |
2 (Function) | Agda.Compiler.JS.Compiler |
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 | |
1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Function) | Agda.Compiler.Epic.Primitive |
DefNode | Agda.TypeChecking.Positivity |
defnPars | Agda.Compiler.Epic.Smashing |
DefP | Agda.Syntax.Abstract |
defProjection | Agda.Compiler.JS.Compiler |
defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DefSh | Agda.TypeChecking.Rules.LHS.Unify |
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 |
delete | Agda.Utils.VarSet |
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 |
diff | Agda.Compiler.Epic.Erasure |
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 |
domainFree | Agda.TypeChecking.Rules.Term |
DomainFull | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Done | Agda.TypeChecking.CompiledClause |
DontCare | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (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.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 |
DotM | Agda.Interaction.Highlighting.Dot |
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 |
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 |
DotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
dotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
Double | Agda.Compiler.JS.Syntax |
double | Agda.Utils.Pretty |
doubleblock | Agda.Auto.NarrowingSearch |
doubleQuotes | Agda.Utils.Pretty |
doWorkOnTypes | Agda.TypeChecking.Irrelevance |
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 |
dsConnection | Agda.Interaction.Highlighting.Dot |
dsModules | Agda.Interaction.Highlighting.Dot |
dsNameSupply | Agda.Interaction.Highlighting.Dot |
dsubname | Agda.Compiler.MAlonzo.Misc |
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dummy | Agda.Compiler.MAlonzo.Misc |
dummyLambda | Agda.Compiler.JS.Compiler |
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 |