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.TypeChecking.Monad, Agda.Compiler.Backend |
DataBlock | Agda.Syntax.Concrete.Definitions.Types |
dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataCon | Agda.TypeChecking.Datatypes |
dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
DataDefS | Agda.Syntax.Abstract |
dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
DataOrRecord' | Agda.Syntax.Internal |
DataOrRecordE | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataOrRecordModule | Agda.Syntax.Scope.Base |
DataOrRecSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataOrRecSigData | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataOrRecSigDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dataPathCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataRecOrFun | Agda.Syntax.Concrete.Definitions.Types |
datarecPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataSig | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
DataSigS | Agda.Syntax.Abstract |
DataSort | Agda.Interaction.Base |
dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dataTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dataTranspIx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DataType | Agda.Utils.Haskell.Syntax |
Datatype | |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DatatypeData | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DatatypeDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.Syntax |
DCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DDot | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DDot' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DeadCode | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Deadcode | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
DeadCodeReachable | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
deadStandardOptions | Agda.Interaction.Options |
DeBruijn | Agda.TypeChecking.Substitute.DeBruijn, Agda.TypeChecking.Substitute |
DeBruijnIndexOutOfScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
debugClause | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
DeclarationSpine | Agda.Syntax.Abstract |
declarationSpine | Agda.Syntax.Abstract |
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 |
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.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
decodeStrictText | Agda.Interaction.JSON |
decomposeInterval | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
decomposeInterval' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
decorate | Agda.Interaction.InteractionTop |
Decoration | Agda.Utils.Functor |
Decr | Agda.Termination.Order |
decr | Agda.Termination.Order |
decrease | Agda.Termination.Order |
decreasing | Agda.Termination.Order |
DeepSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Abstract |
Def' | Agda.Syntax.Abstract |
defAbstract | |
1 (Function) | Agda.Syntax.Info |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defAccess | Agda.Syntax.Info |
defApp | Agda.TypeChecking.Substitute |
DefArg | Agda.TypeChecking.Positivity.Occurrence |
defArgGeneralizable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defArgInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defArgs | Agda.TypeChecking.MetaVars.Occurs |
Default | Agda.Utils.WithDefault |
defaultAction | Agda.TypeChecking.CheckInternal |
defaultAddCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultAddLetBinding' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
defaultBuildDoStmt | Agda.Syntax.Parser.Helpers |
defaultCohesion | Agda.Syntax.Common |
DefaultCompute | Agda.Interaction.Base |
defaultCutOff | Agda.Termination.CutOff, Agda.Interaction.Options |
defaultDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultDom | Agda.Syntax.Internal |
defaultErased | Agda.Syntax.Common |
defaultFixity | Agda.Syntax.Common |
defaultGetConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultGetProfileOptions | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultGetRewriteRulesFor | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultGetVerbosity | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultImportDir | Agda.Syntax.Common |
defaultInteractionOptions | Agda.Interaction.Options |
defaultInteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defaultInteractor | Agda.Main |
defaultIsDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
defaultOpenLevelsToZero | Agda.TypeChecking.Level.Solve |
defaultOptions | |
1 (Function) | Agda.Interaction.Options |
2 (Function) | Agda.Interaction.JSON |
DefaultOverlap | Agda.Syntax.Common |
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.TypeChecking.Monad, Agda.Compiler.Backend |
defaultWarningMode | Agda.Interaction.Options.Warnings |
defaultWarningSet | Agda.Interaction.Options.Warnings |
defBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defCompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defCompilerPragmas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defCopy | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defFixity | Agda.Syntax.Info |
defForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defGeneralizedParams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defineCompData | Agda.TypeChecking.Rules.Data |
defineCompKitR | Agda.TypeChecking.Rules.Record |
defineConClause | Agda.TypeChecking.Rules.Data |
Defined | Agda.Syntax.Scope.Base |
DefinedName | Agda.Syntax.Scope.Base |
defineHCompForFields | Agda.TypeChecking.Rules.Data |
defineKanOperationForFields | Agda.TypeChecking.Rules.Data |
defineKanOperationR | Agda.TypeChecking.Rules.Record |
defineProjections | Agda.TypeChecking.Rules.Data |
defineTranspForFields | Agda.TypeChecking.Rules.Data |
defineTranspFun | Agda.TypeChecking.Rules.Data |
defineTranspIx | Agda.TypeChecking.Rules.Data |
DefInfo | |
1 (Data Constructor) | Agda.Syntax.Info |
2 (Type/Class) | Agda.Syntax.Abstract |
defInfo | Agda.Syntax.Info |
DefInfo' | Agda.Syntax.Info |
definitelyNonRecursive_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Definition | |
1 (Type/Class) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
definition | Agda.Compiler.JS.Compiler |
definition' | Agda.Compiler.JS.Compiler |
definitionCheck | Agda.TypeChecking.MetaVars.Occurs |
DefinitionInDifferentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefinitionIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Definitions | |
1 (Data Constructor) | Agda.Utils.ProfileOptions |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefinitionSite | |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
definitionSite | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
defInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defInstance | |
1 (Function) | Agda.Syntax.Info |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefInsteadOfCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defIsDataOrRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defJSDef | Agda.Compiler.JS.Compiler |
defLanguage | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defMacro | Agda.Syntax.Info |
defMatchable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Defn | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defn | Agda.Compiler.JS.Syntax |
defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defNeedsChecking | Agda.TypeChecking.MetaVars.Occurs |
defNoCompilation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefNode | Agda.TypeChecking.Positivity |
defNonterminating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defOpaque | |
1 (Function) | Agda.Syntax.Info |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defOrVar | Agda.TypeChecking.Rules.Term |
DefP | |
1 (Data Constructor) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Abstract |
defParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DefS | Agda.Syntax.Internal |
defSiteAnchor | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
defSiteHere | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
defSiteModule | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
defSitePos | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
defTactic | Agda.Syntax.Info |
defTerminationUnconfirmed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.BoolSet |
3 (Function) | Agda.Utils.AssocList |
4 (Function) | Agda.Utils.SmallSet |
5 (Function) | Agda.Utils.Trie |
deleteAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
deleteFromDT | Agda.TypeChecking.DiscrimTree |
deleteLeft | Agda.TypeChecking.Rules.LHS.Unify.Types |
deleteRight | Agda.TypeChecking.Rules.LHS.Unify.Types |
deleteType | Agda.TypeChecking.Rules.LHS.Unify.Types |
Deletion | Agda.TypeChecking.Rules.LHS.Unify.Types |
delimiter | Agda.Utils.String |
deLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
dependencySortMetas | Agda.TypeChecking.MetaVars |
DeprecationWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DeprecationWarning_ | Agda.Interaction.Options.Warnings |
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 |
detectIdentityFunctions | Agda.Compiler.Treeless.Identity |
dfPats | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dfPatternVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dfRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dget | Agda.Utils.Functor |
DiagnosticsColours | Agda.Interaction.Options |
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.BoolSet |
3 (Function) | Agda.Utils.IntSet.Infinite |
4 (Function) | Agda.Utils.SmallSet |
DifferentOpaque | Agda.Syntax.Common |
Dioid | Agda.TypeChecking.SizedTypes.Utils |
Direct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DirEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DirGeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DirLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dirToCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Dirty | |
1 (Type/Class) | Agda.TypeChecking.Unquote |
2 (Data Constructor) | Agda.TypeChecking.Unquote |
dirty | Agda.Utils.Update |
disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DisallowedGeneralizeName | Agda.Syntax.Scope.Base |
DisallowedInterleavedMutual | Agda.Syntax.Concrete.Definitions.Errors |
disallowGeneralizedVars | Agda.Syntax.Scope.Base |
DisambiguatedName | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
disambiguateRecordFields | Agda.Interaction.Highlighting.Generate |
discrete | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
DiscrimTree | Agda.TypeChecking.DiscrimTree.Types |
Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
displayDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
displayForm | Agda.TypeChecking.DisplayForm |
DisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DisplayInfo | Agda.Interaction.Response |
DisplayInfo_boot | Agda.Interaction.Response.Base, 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.TypeChecking.Monad, Agda.Compiler.Backend |
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.Syntax.Common.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 |
doCompile | Agda.Compiler.Common |
doCompile' | Agda.Compiler.Common |
DocP | Agda.Utils.Parser.MemoisedCPS |
docsUrl | Agda.Version |
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, Agda.Compiler.Backend |
DoesNotCorrespondToValidModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DoesNotMentionTicks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DoesNotTargetRewriteRelation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
doExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DoGeneralize | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
doGlueKanOp | Agda.TypeChecking.Primitive.Cubical.Glue, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
DoHComp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
doHCompUKanOp | Agda.TypeChecking.Primitive.Cubical.HCompU, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
DoHighlightModuleContents | Agda.TypeChecking.Rules.Decl |
doIdKanOp | Agda.TypeChecking.Primitive.Cubical.Id, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
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 |
domainUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
doMeta | Agda.Syntax.Internal.Defs |
domFromArg | Agda.Syntax.Internal |
domFromNamedArg | Agda.Syntax.Internal |
domFromNamedArgName | Agda.TypeChecking.Substitute |
domH | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
dominated | Agda.Utils.Favorites |
Dominates | Agda.Utils.Favorites |
dominator | Agda.Utils.Favorites |
domInfo | Agda.Syntax.Internal |
domIsFinite | Agda.Syntax.Internal |
domN | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
domName | Agda.Syntax.Internal |
domOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
domTactic | Agda.Syntax.Internal |
Done | |
1 (Data Constructor) | Agda.TypeChecking.CompiledClause |
2 (Data Constructor) | Agda.Interaction.Base |
DoneDT | Agda.TypeChecking.DiscrimTree.Types |
DoNotParseSections | Agda.Syntax.Concrete.Operators.Parser |
dontAssignMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DontCare | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Abstract |
dontCare | Agda.Syntax.Internal |
DontCutOff | Agda.Termination.CutOff |
DontDefaultToInfty | Agda.TypeChecking.SizedTypes.Solve |
DontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dontExpandLast | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dontFoldLetBindings | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DontHightlightModuleContents | Agda.TypeChecking.Rules.Decl |
DontKnow | Agda.TypeChecking.Patterns.Match |
DontOpen | Agda.Syntax.Concrete |
DontReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DontRunMetaOccursCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DontRunRecordPatternTranslation | Agda.TypeChecking.CompiledClause.Compile |
DontWakeUp | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
DoOpen | Agda.Syntax.Concrete |
doPathPKanOp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
doPiKanOp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
DoQuoteTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
DotPatternInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dotPatterns | Agda.TypeChecking.Rules.LHS.Problem |
dotPatternsToPatterns | Agda.TypeChecking.Patterns.Internal |
DoTransp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
DottedPattern | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
Double | Agda.Compiler.JS.Syntax |
double | Agda.Syntax.Common.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 |
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.Syntax.Common.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 |
dropAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
dropCommon | Agda.Utils.List |
dropConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dropEnd | Agda.Utils.List |
dropFrom | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.Permutation |
dropMore | Agda.Utils.Permutation |
dropN | Agda.Utils.Permutation |
dropParameters | Agda.TypeChecking.ReconstructParameters |
droppedP | Agda.Utils.Permutation |
droppedPars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
DSizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DSizeMeta | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DSizeVar | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DTerm' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateDefinition | Agda.Syntax.Concrete.Definitions.Errors |
DuplicateExecutable | Agda.Interaction.Library.Base |
DuplicateFields | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Warning |
2 (Data Constructor) | Agda.Interaction.Library.Base |
3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateFields_ | Agda.Interaction.Options.Warnings |
DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateInterfaceFiles | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateInterfaceFiles_ | Agda.Interaction.Options.Warnings |
DuplicateOverlapPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicatePrimitiveBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateRecordDirective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateRecordDirective_ | Agda.Interaction.Options.Warnings |
DuplicateRewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateRewriteRule_ | Agda.Interaction.Options.Warnings |
duplicates | Agda.Utils.List |
DuplicateUsing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
DuplicateUsing_ | Agda.Interaction.Options.Warnings |
DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
dwLocation | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
dwWarning | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |