Agda-2.6.20240714: A dependently typed functional programming language and proof assistant

Index - A

A 
1 (Data Constructor)Agda.Interaction.EmacsCommand
2 (Data Constructor)Agda.Compiler.MAlonzo.Misc
aArityAgda.Syntax.Treeless, Agda.Compiler.Backend
aBodyAgda.Syntax.Treeless, Agda.Compiler.Backend
abort 
1 (Function)Agda.Interaction.Base
2 (Function)Agda.TypeChecking.MetaVars.Occurs
abortIfBlockedAgda.TypeChecking.Reduce
AboveAgda.Compiler.JS.Pretty
aboveAgda.Utils.IntSet.Infinite
Abs 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Syntax.Reflected
absAppAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
absAppNAgda.TypeChecking.Names
absBodyAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
AbsModuleAgda.Syntax.Scope.Base
AbsN 
1 (Type/Class)Agda.TypeChecking.Names
2 (Data Constructor)Agda.TypeChecking.Names
AbsNameAgda.Syntax.Scope.Base
absNameAgda.Syntax.Internal
AbsNameWithFixity 
1 (Type/Class)Agda.TypeChecking.Serialise.Instances.Abstract
2 (Data Constructor)Agda.TypeChecking.Serialise.Instances.Abstract
absNNameAgda.TypeChecking.Names
AbsOfConAgda.Syntax.Translation.ConcreteToAbstract
AbsOfRefAgda.Syntax.Translation.ReflectedToAbstract
absoluteAgda.Utils.FileName
AbsolutePath 
1 (Type/Class)Agda.Utils.FileName
2 (Data Constructor)Agda.Utils.FileName
AbsTermAgda.TypeChecking.Abstract
absTermAgda.TypeChecking.Abstract
AbsToConAgda.Syntax.Translation.AbstractToConcrete
Abstract 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abstractAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abstractArgsAgda.TypeChecking.Substitute
AbstractConstructorNotInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractDefAgda.Syntax.Common
AbstractDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbstractMode 
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
AbstractModuleAgda.Syntax.Scope.Base
abstractNAgda.TypeChecking.Names
AbstractNameAgda.Syntax.Scope.Base
AbstractRHSAgda.Syntax.Translation.ConcreteToAbstract
abstractTAgda.TypeChecking.Names
abstractTermAgda.TypeChecking.Abstract
abstractToConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
abstractToConcreteHidingAgda.Syntax.Translation.AbstractToConcrete
abstractToConcreteScopeAgda.Syntax.Translation.AbstractToConcrete
abstractToConcrete_Agda.Syntax.Translation.AbstractToConcrete
abstractTypeAgda.TypeChecking.Abstract
Absurd 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
absurdAgda.Utils.Empty
absurdBindingAgda.Syntax.Parser.Helpers
absurdBodyAgda.Syntax.Internal
AbsurdClauseAgda.Syntax.Reflected
AbsurdLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
absurdLambdaNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsurdMatchAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
AbsurdP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
absurdPAgda.Syntax.Internal
AbsurdPatternAgda.TypeChecking.Rules.LHS.Problem
absurdPatternNameAgda.Syntax.Internal
AbsurdPatternRequiresNoRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AbsurdPatternRequiresNoRHS_Agda.Interaction.Options.Warnings
absurdPatternsAgda.TypeChecking.Rules.LHS.Problem
AbsurdRHS 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AbsurdRHSSAgda.Syntax.Abstract
absVAgda.TypeChecking.Substitute
acceptableFileExtsAgda.Syntax.Parser
AccessAgda.Syntax.Common
acConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Account 
1 (Type/Class)Agda.Utils.Benchmark
2 (Type/Class)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
accumAgda.Utils.IArray
accumArrayAgda.Utils.IArray
acDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
acElimsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
aConAgda.Syntax.Treeless, Agda.Compiler.Backend
acRangesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ACStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Action 
1 (Type/Class)Agda.TypeChecking.CheckInternal
2 (Data Constructor)Agda.TypeChecking.CheckInternal
activateLoadedFileCacheAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
activeBackendAgda.Compiler.Backend
activeBackendMayEraseTypeAgda.Compiler.Backend
acTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
acyclicAgda.Utils.Graph.AdjacencyMap.Unidirectional
add 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
addAndUnblockerAgda.TypeChecking.Constraints
addAwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addAwakeConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addClausesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCoercionsAgda.Compiler.MAlonzo.Coerce
addCohesionAgda.Syntax.Common
addColumnAgda.Termination.SparseMatrix
addCompilerPragmaAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCompositionForRecordAgda.TypeChecking.Rules.Record
addConstantAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstant'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstraint 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addConstraintTCMAgda.TypeChecking.Constraints
addConstraintToAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AddContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addCPUTimeAgda.Utils.Benchmark
addCtxAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDataConsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDefaultLibrariesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDisplayFormAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addDisplayFormsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addEdge 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.SizedTypes.WarshallSolver
addFinalNewLineAgda.Utils.String
addFlexAgda.Utils.Warshall
addFlexRigAgda.TypeChecking.Free.Lazy
addForeignCodeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImportAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addImportCycleCheckAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addLetBindingAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addLetBinding'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addLoneSigAgda.Syntax.Concrete.Definitions.Monad
addModalityAgda.Syntax.Common
addModuleToScopeAgda.Syntax.Scope.Base
addNameToScopeAgda.Syntax.Scope.Base
addNodeAgda.Utils.Warshall
addOrUnblockerAgda.TypeChecking.Constraints
addPragmaAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addProfileOptionAgda.Utils.ProfileOptions
addQuantityAgda.Syntax.Common
addRecordNameContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addRelevanceAgda.Syntax.Common
addRewriteRulesAgda.TypeChecking.Rewriting
addRewriteRulesForAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addRowAgda.Termination.SparseMatrix
addSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addSuffixAgda.Utils.Suffix
addTrustedExecutablesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addTypeAgda.Syntax.Parser.Helpers
addTypedInstanceAgda.TypeChecking.InstanceArguments
addTypedInstance'Agda.TypeChecking.InstanceArguments
addTypedPatternsAgda.TypeChecking.Rules.Term
addUniqueIntsAgda.Utils.Graph.AdjacencyMap.Unidirectional
addUnknownInstanceAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addVarToBindAgda.Syntax.Scope.Monad
addWarningAgda.TypeChecking.Warnings
ADefAgda.TypeChecking.Positivity
aDefToModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AdjListAgda.Utils.Warshall
adjust 
1 (Function)Agda.Utils.Trie
2 (Function)Agda.Utils.BiMap
adjustMAgda.Utils.Map
adjustM'Agda.Utils.Map
adjustPreconditionAgda.Utils.BiMap
ADotTAgda.Syntax.Abstract.Pattern
AesonException 
1 (Type/Class)Agda.Interaction.JSON
2 (Data Constructor)Agda.Interaction.JSON
AffineHoleAgda.Utils.AffineHole
AgdaErrorAgda.Interaction.ExitCode
agdaErrorFromIntAgda.Interaction.ExitCode
agdaErrorToIntAgda.Interaction.ExitCode
AgdaFileTypeAgda.Syntax.Common
AgdaLibFile 
1 (Type/Class)Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library.Base, Agda.Interaction.Library
agdaTermTypeAgda.TypeChecking.Unquote
agdaTypeTypeAgda.TypeChecking.Unquote
aGuardAgda.Syntax.Treeless, Agda.Compiler.Backend
AlexEOFAgda.Syntax.Parser.Lexer
AlexErrorAgda.Syntax.Parser.Lexer
alexGetByteAgda.Syntax.Parser.Alex
alexGetCharAgda.Syntax.Parser.Alex
AlexInput 
1 (Type/Class)Agda.Syntax.Parser.Alex
2 (Data Constructor)Agda.Syntax.Parser.Alex
alexInputPrevCharAgda.Syntax.Parser.Alex
AlexReturnAgda.Syntax.Parser.Lexer
alexScanUserAgda.Syntax.Parser.Lexer
AlexSkipAgda.Syntax.Parser.Lexer
AlexTokenAgda.Syntax.Parser.Lexer
alignAgda.Syntax.Common.Pretty
aLitAgda.Syntax.Treeless, Agda.Compiler.Backend
All 
1 (Type/Class)Agda.Utils.IndexedList
2 (Type/Class)Agda.Utils.TypeLevel
allApplyElimsAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
AllAreOpaqueAgda.Syntax.Common
allBlockingDefsAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allBlockingMetasAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allBlockingProblemsAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allCohesionsAgda.Syntax.Common
allConsecutiveAgda.Utils.List
allDuplicatesAgda.Utils.List
allEqual 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
allFlexVarsAgda.TypeChecking.Rules.LHS.Problem
allFreeVarsAgda.TypeChecking.Free
allHelpTopicsAgda.Interaction.Options.Help
allIndicesAgda.Utils.IndexedList
allIrrelevantOrPropTelAgda.TypeChecking.Irrelevance
allJustMAgda.Utils.Maybe
AllKindsOfNamesAgda.Syntax.Scope.Base
allKindsOfNamesAgda.Syntax.Scope.Base
allLeftAgda.Utils.Either
allListTAgda.Utils.ListT
allMAgda.Utils.Monad
allMetaClassesAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllMetasAgda.Syntax.Internal.MetaVars
allMetasAgda.Syntax.Internal.MetaVars
allMetas'Agda.Syntax.Internal.MetaVars
allMetasListAgda.Syntax.Internal.MetaVars
AllModulesAgda.Mimer.Options
allNamesInScopeAgda.Syntax.Scope.Base
allNamesInScope'Agda.Syntax.Scope.Base
allNameSpacesAgda.Syntax.Scope.Base
allNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
allNullaryToStringTagAgda.Interaction.JSON
allowAllReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllowAmbiguousNamesAgda.Syntax.Scope.Base
AllowedReductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllowedReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AllowedVarAgda.TypeChecking.MetaVars.Occurs
allowedVarsAgda.TypeChecking.MetaVars.Occurs
allowNonTerminatingReductionsAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allowOmittedFieldsAgda.Interaction.JSON
allProjElimsAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
allReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
allRelevancesAgda.Syntax.Common
allRelevantVarsAgda.TypeChecking.Free
allRelevantVarsIgnoringAgda.TypeChecking.Free
allRightAgda.Utils.Either
allThingsInScopeAgda.Syntax.Scope.Base
allUsedNamesAgda.Syntax.Abstract.UsedNames
allVarsAgda.TypeChecking.Free
AllWarningsAgda.TypeChecking.Warnings
allWarningsAgda.Interaction.Options.Warnings
Alt 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Utils.Haskell.Syntax
alterAgda.Utils.BiMap
alterMAgda.Utils.BiMap
alterPreconditionAgda.Utils.BiMap
altM1Agda.Utils.Monad
AlwaysColourAgda.Interaction.Options
alwaysMakeAbstractAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
alwaysReportSDocAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
alwaysReportSLnAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
alwaysUnblockAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
amapAgda.Utils.IArray
AmbiguousAgda.Interaction.FindFile
AmbiguousAnythingAgda.Syntax.Scope.Base
AmbiguousConProjsAgda.Syntax.Scope.Base
AmbiguousConstructor 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions.Errors
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousDeclNameAgda.Syntax.Scope.Base
AmbiguousFieldAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousFunClausesAgda.Syntax.Concrete.Definitions.Errors
AmbiguousLibAgda.Interaction.Library.Base
AmbiguousLocalVarAgda.Syntax.Scope.Base
AmbiguousModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousNameReasonAgda.Syntax.Scope.Base
ambiguousNamesInReasonAgda.Syntax.Scope.Base
AmbiguousNothingAgda.Syntax.Scope.Base
AmbiguousOverloadedProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AmbiguousTopLevelModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
aModeToDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
amodLineageAgda.Syntax.Scope.Base
amodNameAgda.Syntax.Scope.Base
anameKindAgda.Syntax.Scope.Base
anameLineageAgda.Syntax.Scope.Base
anameMetadataAgda.Syntax.Scope.Base
anameNameAgda.Syntax.Scope.Base
AnArgAgda.TypeChecking.Positivity
and2MAgda.Utils.Monad
andMAgda.Utils.Monad
andThenAgda.Syntax.Parser.LexActions
Ann 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
annLockAgda.Syntax.Common
annotate 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.Utils.Parser.MemoisedCPS
annotateAspectAgda.Syntax.Common.Pretty
annotateDeclsAgda.Syntax.Scope.Monad
annotateExprAgda.Syntax.Scope.Monad
annotatePatternAgda.Syntax.Translation.ReflectedToAbstract
Annotation 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
AnnotationPatternAgda.TypeChecking.Rules.LHS.Problem
AnnPAgda.Syntax.Abstract
antiUnifyAgda.TypeChecking.Conversion
antiUnifyArgsAgda.TypeChecking.Conversion
antiUnifyElimsAgda.TypeChecking.Conversion
antiUnifyTypeAgda.TypeChecking.Conversion
AnyAbstractAgda.Syntax.Abstract
anyAbstractAgda.Syntax.Abstract
anyDefsAgda.Termination.RecCheck
anyEllipsisVarAgda.Interaction.MakeCase
AnyIsAbstractAgda.Syntax.Common
anyIsAbstractAgda.Syntax.Common
anyListTAgda.Utils.ListT
anyMAgda.Utils.Monad
AnyRigidAgda.TypeChecking.MetaVars.Occurs
anyRigidAgda.TypeChecking.MetaVars.Occurs
AnyWhereAgda.Syntax.Concrete
APatNameAgda.Syntax.Translation.ConcreteToAbstract
APatternLikeAgda.Syntax.Abstract.Pattern
App 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.TypeChecking.EtaContract
appAgda.Syntax.Abstract
appBracketsAgda.Syntax.Fixity
appBrackets'Agda.Syntax.Fixity
appDef'Agda.TypeChecking.Reduce
appDefE'Agda.TypeChecking.Reduce
append 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
appendArgNamesAgda.Syntax.Common
appendList 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
AppInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
appInteractionOutputCallbackAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AppKAgda.Syntax.Concrete.Operators.Parser.Monad
ApplicationAgda.Syntax.Abstract.Views
AppliedAgda.Syntax.Scope.Base
Apply 
1 (Type/Class)Agda.Utils.TypeLevel
2 (Data Constructor)Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Compiler.JS.Syntax
5 (Type/Class)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
6 (Data Constructor)Agda.Syntax.Abstract
apply 
1 (Function)Agda.Utils.AssocList
2 (Function)Agda.Compiler.JS.Substitution
3 (Function)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
apply1Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyAttrAgda.Syntax.Parser.Helpers
applyAttrsAgda.Syntax.Parser.Helpers
applyAttrs1Agda.Syntax.Parser.Helpers
applyCohesionAgda.Syntax.Common
applyCohesionToContextAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyCohesionToContextOnlyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyEAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyFlagsToTCWarningsAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
applyFlagsToTCWarningsPreservingAgda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
applyImportDirectiveAgda.Syntax.Scope.Base
applyImportDirectiveMAgda.Syntax.Scope.Monad
applyImportDirective_Agda.Syntax.Scope.Base
applyModalityAgda.Syntax.Common
applyModalityToContextAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyModalityToContextFunBodyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyModalityToContextOnlyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyModalityToJudgementOnlyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyNAgda.TypeChecking.Names
applyN'Agda.TypeChecking.Names
applyNLPatSubstAgda.TypeChecking.Substitute
applyNLSubstToDomAgda.TypeChecking.Substitute
ApplyOrIApplyAgda.TypeChecking.Coverage.Match
applyPatSubstAgda.TypeChecking.Substitute
applyQuantityAgda.Syntax.Common
applyQuantityToJudgementAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyRelevanceAgda.Syntax.Common
applyRelevanceToContextAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyRelevanceToContextFunBodyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyRelevanceToContextOnlyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applyRelevanceToJudgementOnlyAgda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ApplySAgda.Syntax.Abstract
applysAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applySection'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
applySplitPSubstAgda.TypeChecking.Coverage.Match
applySubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySubstTermAgda.TypeChecking.Substitute
applyTermEAgda.TypeChecking.Substitute
applyUnderAgda.TypeChecking.Rules.LHS.Unify.Types
applyUnlessAgda.Utils.Function
applyUnlessMAgda.Utils.Function
applyUnlessNullAgda.Utils.Null
applyWhenAgda.Utils.Function
applyWhenJustAgda.Utils.Function
applyWhenMAgda.Utils.Function
applyWhenNothingAgda.Utils.Function
applyWhenVerboseSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend
appOriginAgda.Syntax.Info
AppPAgda.Syntax.Concrete
appPAgda.Syntax.Concrete.Operators.Parser
appParensAgda.Syntax.Info
appRangeAgda.Syntax.Info
approxConInductionAgda.Syntax.Scope.Base
appTelAgda.TypeChecking.Names
AppVAgda.Syntax.Concrete.Operators.Parser
AppView 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract.Views
appView 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract.Views
AppView'Agda.Syntax.Abstract.Views
appView'Agda.Syntax.Abstract.Views
apReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
apTCMTAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ArcAgda.Utils.Warshall
areWeCachingAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Arg 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
ArgDescrAgda.Interaction.Options
argFromDomAgda.Syntax.Internal
argHAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
ArgInfo 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
argInfoAgda.Syntax.Common
argInfoAnnotationAgda.Syntax.Common
argInfoFreeVariablesAgda.Syntax.Common
argInfoHidingAgda.Syntax.Common
argInfoModalityAgda.Syntax.Common
argInfoOriginAgda.Syntax.Common
argNAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
ArgNameAgda.Syntax.Common
argNameToStringAgda.Syntax.Common
ArgNodeAgda.TypeChecking.Positivity
Args 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Type/Class)Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Reflected
4 (Type/Class)Agda.Syntax.Abstract
ArgsCheckStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
argsFromElimsAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
argsPAgda.Syntax.Concrete.Operators.Parser
argsToElimsAgda.Syntax.Reflected
ArgTAgda.TypeChecking.Records
argToDontCareAgda.TypeChecking.Substitute
ArgumentAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
ArgumentCtxAgda.Syntax.Fixity
argumentCtx_Agda.Syntax.Fixity
ArgumentIndexAgda.Termination.CallMatrix
ArgUnusedAgda.Syntax.Treeless, Agda.Compiler.Backend
ArgUsageAgda.Syntax.Treeless, Agda.Compiler.Backend
ArgUsedAgda.Syntax.Treeless, Agda.Compiler.Backend
ArgVarsAgda.TypeChecking.Names
ArityAgda.Syntax.Common
arity 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.TypeChecking.CompiledClause
arityPiPathAgda.TypeChecking.Telescope.Path
Array 
1 (Type/Class)Agda.Utils.IArray
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Type/Class)Agda.Interaction.JSON
4 (Data Constructor)Agda.Interaction.JSON
arrayAgda.Utils.IArray
arrowAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
ArrowsAgda.Utils.TypeLevel
AsAgda.Syntax.Concrete
AsBAgda.TypeChecking.Rules.LHS.Problem
AsBindingAgda.TypeChecking.Rules.LHS.Problem
AsciiCounterAgda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AsciiOnlyAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty, Agda.Interaction.Options
asFiniteAgda.Utils.Float
AsIsAgda.Interaction.Base
askGHCEnvAgda.Compiler.MAlonzo.Misc
askGHCModuleEnvAgda.Compiler.MAlonzo.Misc
askHsModuleEnvAgda.Compiler.MAlonzo.Misc
askNameAgda.Syntax.Translation.ReflectedToAbstract
askRAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend
asksTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
askTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
askVarAgda.Syntax.Translation.ReflectedToAbstract
asMainFunctionDefAgda.Compiler.MAlonzo.Primitives
AsName 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
asNameAgda.Syntax.Concrete
AsName'Agda.Syntax.Concrete
AsP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AsPatternInPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
asPatternsAgda.TypeChecking.Rules.LHS.Problem
AsPatternShadowsConstructorOrPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AsPatternShadowsConstructorOrPatternSynonym_Agda.Interaction.Options.Warnings
AspectAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
aspectAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
Aspects 
1 (Type/Class)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
asQuantityAgda.Syntax.Common
asRangeAgda.Syntax.Concrete
assertConOfAgda.TypeChecking.Rewriting.NonLinPattern
assertPathAgda.TypeChecking.Rewriting.NonLinPattern
assertPiAgda.TypeChecking.Rewriting.NonLinPattern
assertProjOfAgda.TypeChecking.Rewriting.NonLinPattern
Assign 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Interaction.Base
assignAgda.TypeChecking.MetaVars
assignEAgda.TypeChecking.Conversion
assignMetaAgda.TypeChecking.MetaVars
assignMeta'Agda.TypeChecking.MetaVars
AssignsAgda.Syntax.Abstract
assignTermAgda.TypeChecking.MetaVars
assignTerm'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
assignTermTCM'Agda.TypeChecking.MetaVars
assignVAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
assignWrapperAgda.TypeChecking.MetaVars
AsSizesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AssociativityAgda.Syntax.Common
AssocListAgda.Utils.AssocList
assocsAgda.Utils.IArray
AsTermsOfAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AsTypesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
asViewAgda.Syntax.Abstract.Views
atClauseAgda.TypeChecking.Rules.Def
atLeastTwoPartsAgda.Syntax.Concrete.Operators.Parser
atomicLevelAgda.Syntax.Internal
atomicModifyIORefAgda.Utils.IORef
atomicModifyIORef'Agda.Utils.IORef
atomicWriteIORefAgda.Utils.IORef
atomizeLayersAgda.Syntax.Parser.Literate
atomP 
1 (Function)Agda.Utils.Parser.MemoisedCPS
2 (Function)Agda.Syntax.Concrete.Operators.Parser
atTopLevel 
1 (Function)Agda.Interaction.BasicOps
2 (Function)Agda.Interaction.InteractionTop
Attr 
1 (Type/Class)Agda.Syntax.Parser.Helpers
2 (Data Constructor)Agda.Syntax.Parser.Helpers
AttributeAgda.Syntax.Concrete.Attribute
AttributeKindNotEnabledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AttributesAgda.Syntax.Concrete.Attribute
attributesForModalityAgda.Syntax.Concrete.Pretty
attributesMapAgda.Syntax.Concrete.Attribute
attrNameAgda.Syntax.Parser.Helpers
attrRangeAgda.Syntax.Parser.Helpers
augCallInfoAgda.Termination.CallMatrix
augCallMatrixAgda.Termination.CallMatrix
AutoColourAgda.Interaction.Options
autoInlineAgda.TypeChecking.Inlining
AwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Axiom 
1 (Data Constructor)Agda.Syntax.Reflected
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
3 (Data Constructor)Agda.Syntax.Abstract
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
axiomConstTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AxiomData 
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
AxiomDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AxiomNameAgda.Syntax.Scope.Base
axiomNameAgda.Syntax.Abstract
AxiomSAgda.Syntax.Abstract