Data | Agda.Syntax.Concrete |
dataAbstr | 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 |
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dataNonLinPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DataOrRecord | Agda.TypeChecking.Datatypes |
dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify |
dataOrRecordType' | Agda.TypeChecking.Rules.LHS.Unify |
dataOrRecordTypeHH | 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 |
DataSig | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
dataSmallPars | 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 |
dbraces | |
1 (Function) | Agda.Syntax.Concrete.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
DBSizeExpr | Agda.TypeChecking.SizedTypes.Solve |
DCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DDot | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
deal | Agda.Utils.List |
deBruijnIndex | Agda.Interaction.MakeCase |
DeBruijnPat | Agda.Termination.Monad, Agda.Termination.TermCheck |
DeBruijnPat' | Agda.Termination.Monad |
DeBruijnPats | Agda.Termination.Monad |
debug | |
1 (Function) | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad |
2 (Function) | Agda.TypeChecking.SizedTypes.Utils |
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 |
decodeHashes | Agda.TypeChecking.Serialise |
decodeInterface | Agda.TypeChecking.Serialise |
decompress | Agda.Interaction.Highlighting.Precise |
Decoration | Agda.Utils.Functor |
decr | Agda.Termination.Order |
decrConf | Agda.TypeChecking.Test.Generators |
decrease | Agda.Termination.Order |
decreasing | Agda.Termination.Order |
DeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
deepSizeView | Agda.TypeChecking.SizedTypes |
deepUnScope | Agda.Syntax.Abstract.Views |
Def | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
defAbstract | |
1 (Function) | Agda.Syntax.Info |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defAccess | Agda.Syntax.Info |
defApp | Agda.TypeChecking.Substitute |
DefArg | Agda.TypeChecking.Positivity |
defArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defArgs | Agda.TypeChecking.MetaVars.Occurs |
Default | Agda.Compiler.Epic.AuxAST |
defaultArg | Agda.Syntax.Common |
defaultArgInfo | Agda.Syntax.Common |
defaultColoredArg | Agda.Syntax.Common |
defaultCutOff | Agda.Interaction.Options |
defaultDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defaultDom | Agda.Syntax.Common |
defaultFixity | Agda.Syntax.Fixity |
defaultFixity' | Agda.Syntax.Fixity |
defaultFlexibleVar | Agda.TypeChecking.Rules.LHS.Problem |
defaultFrequencies | Agda.TypeChecking.Test.Generators |
defaultImportDir | Agda.Syntax.Concrete |
defaultInteractionOptions | Agda.Interaction.Options |
defaultInteractionOutputCallback | Agda.Interaction.Response |
defaultNamedArg | Agda.Syntax.Common |
defaultNotation | Agda.Syntax.Notation |
defaultOptions | Agda.Interaction.Options |
defaultParseFlags | Agda.Syntax.Parser.Monad |
defaultTerEnv | Agda.Termination.Monad |
defaultVerbosity | Agda.Interaction.Options |
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defColors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defCopy | 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 |
defEpicDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defFixity | Agda.Syntax.Info |
defFreq | Agda.TypeChecking.Test.Generators |
Defined | Agda.Syntax.Scope.Base |
DefinedName | Agda.Syntax.Scope.Monad |
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 |
defInstance | |
1 (Function) | Agda.Syntax.Info |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
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 |
defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs |
DefNode | Agda.TypeChecking.Positivity |
defNonterminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defnPars | Agda.Compiler.Epic.Smashing |
defOrVar | Agda.TypeChecking.Rules.Term |
DefP | Agda.Syntax.Abstract |
defPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
defRewriteRules | 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.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
delete | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.Trie |
dependentPolarity | Agda.TypeChecking.Polarity |
depthofvar | Agda.Auto.CaseSplit |
derefPtr | Agda.Utils.Pointer, Agda.Syntax.Internal |
Deserialization | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
dest | Agda.TypeChecking.SizedTypes.WarshallSolver |
detecteliminand | Agda.Auto.Syntax |
detectsemiflex | Agda.Auto.Syntax |
dfFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dfPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dfRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dget | Agda.Utils.Functor |
Diagonal | Agda.Termination.SparseMatrix |
diagonal | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
2 (Function) | Agda.Termination.SparseMatrix |
diff | Agda.Compiler.Epic.Erasure |
difference | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Dioid | Agda.TypeChecking.SizedTypes.Utils |
Direct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DirEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DirGeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DirLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dirToCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dirty | Agda.Utils.Update |
disableDestructiveUpdate | Agda.TypeChecking.Monad.Sharing, Agda.TypeChecking.Monad |
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Discard | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
discard | Agda.Utils.QuickCheck |
disjoin | Agda.Utils.QuickCheck |
Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
displayDebugMessage | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
displayForm | Agda.TypeChecking.DisplayForm |
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
DisplayInfo | Agda.Interaction.Response |
displayRunningInfo | Agda.Interaction.EmacsCommand |
displayStatus | Agda.Interaction.InteractionTop |
DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
display_info | Agda.Interaction.InteractionTop |
display_info' | Agda.Interaction.EmacsCommand |
Dist | Agda.Utils.Warshall |
Distance | Agda.Utils.Warshall |
distinct | Agda.Utils.List |
distributeF | Agda.Utils.Functor |
distributive | Agda.Utils.TestHelpers |
divConf | Agda.TypeChecking.Test.Generators |
DLub | Agda.Syntax.Internal |
dLub | Agda.TypeChecking.Substitute |
dmap | Agda.Utils.Functor |
Doc | |
1 (Type/Class) | Agda.Utils.Pretty |
2 (Type/Class) | Agda.TypeChecking.Pretty |
doclos | Agda.Auto.Syntax |
doDef | Agda.Syntax.Internal.Defs |
DoDrop | Agda.Utils.Permutation |
doDrop | Agda.Utils.Permutation |
doesFileExistCaseSensitive | Agda.Utils.FileName |
DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
doEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
doExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
Dom | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Type/Class) | 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 |
domColors | Agda.Syntax.Common |
doMeta | Agda.Syntax.Internal.Defs |
domFromArg | Agda.Syntax.Common |
domH | Agda.TypeChecking.Primitive |
dominated | Agda.Utils.Favorites |
Dominates | Agda.Utils.Favorites |
dominator | Agda.Utils.Favorites |
domInfo | Agda.Syntax.Common |
domN | Agda.TypeChecking.Primitive |
Done | Agda.TypeChecking.CompiledClause |
dontAssignMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
DontCare | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
dontCare | |
1 (Function) | Agda.Auto.Syntax |
2 (Function) | Agda.Syntax.Internal |
DontCutOff | Agda.Termination.CutOff |
dontDescendInto | Agda.Utils.Geniplate |
dontEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
DontExpandInstanceArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
dontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
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 |
DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete |
DoOpen | Agda.Syntax.Concrete |
Dot | Agda.Syntax.Concrete |
DotFlex | Agda.TypeChecking.Rules.LHS.Problem |
DOtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
DotM | Agda.Interaction.Highlighting.Dot |
DotP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
DotPatternCtx | Agda.Syntax.Fixity |
DotPatternInst | Agda.TypeChecking.Rules.LHS.Problem |
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 |
Double | Agda.Compiler.JS.Syntax |
double | Agda.Utils.Pretty |
doubleblock | Agda.Auto.NarrowingSearch |
doubleQuotes | Agda.Utils.Pretty |
downFrom | Agda.Utils.List |
doWorkOnTypes | Agda.TypeChecking.Irrelevance |
DPI | Agda.TypeChecking.Rules.LHS.Problem |
Drop | |
1 (Type/Class) | Agda.Utils.Permutation |
2 (Data Constructor) | Agda.Utils.Permutation |
DropArgs | Agda.TypeChecking.DropArgs |
dropArgs | Agda.TypeChecking.DropArgs |
dropConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
dropFrom | Agda.Utils.Permutation |
drophid | Agda.Auto.CaseSplit |
dropI | Agda.Syntax.Position |
dropMore | Agda.Utils.Permutation |
dropN | Agda.Utils.Permutation |
droppedP | Agda.Utils.Permutation |
dropProjElims | Agda.Syntax.Internal |
dropS | Agda.TypeChecking.Substitute |
dropWhileM | Agda.Utils.Monad |
dryInstantiate | Agda.Auto.NarrowingSearch |
dsConnection | Agda.Interaction.Highlighting.Dot |
DSizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
DSizeMeta | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
DSizeVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
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 |
dummyDom | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
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 |
duplicates | Agda.Utils.List |
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |