Agda-2.6.2.2.20230105: 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.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
3 (Type/Class)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Internal
5 (Type/Class)Agda.Syntax.Reflected
6 (Data Constructor)Agda.Syntax.Reflected
absAppAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
absAppNAgda.TypeChecking.Names
absBodyAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abslamvarnameAgda.Auto.Convert
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
abspatvarnameAgda.Auto.CaseSplit
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
absurdBodyAgda.Syntax.Internal
AbsurdClauseAgda.Syntax.Reflected
AbsurdLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
AbsurdLambdaAgda.Auto.Syntax
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
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.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addAwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addAwakeConstraint'Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addblkAgda.Auto.Typecheck
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
addendAgda.Auto.Typecheck
AddExtraRefAgda.Auto.NarrowingSearch
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
addImportedInstancesAgda.TypeChecking.Monad.State, 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
addNamedInstanceAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addNameToScopeAgda.Syntax.Scope.Base
addNodeAgda.Utils.Warshall
addOrUnblockerAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
addtrailingargsAgda.Auto.Syntax
addTrustedExecutablesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
addTypedInstanceAgda.TypeChecking.Telescope
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
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
AHMModuleAgda.Auto.Options
AHMNoneAgda.Auto.Options
ALConParAgda.Auto.Syntax
ALConsAgda.Auto.Syntax
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.Utils.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
allBlockingDefsAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allBlockingMetasAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allBlockingProblemsAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
allCohesionsAgda.Syntax.Common
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
allJustMAgda.Utils.Maybe
AllKindsOfNamesAgda.Syntax.Scope.Base
allKindsOfNamesAgda.Syntax.Scope.Base
allLeftAgda.Utils.Either
allListTAgda.Utils.ListT
allMAgda.Utils.Monad
allMetaKindsAgda.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
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
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
allVarsAgda.TypeChecking.Free
AllWarningsAgda.TypeChecking.Warnings
allWarningsAgda.Interaction.Options.Warnings
ALNilAgda.Auto.Syntax
ALProjAgda.Auto.Syntax
Alt 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Utils.Haskell.Syntax
altAgda.Compiler.MAlonzo.Compiler
alterAgda.Utils.BiMap
alterMAgda.Utils.BiMap
alterPreconditionAgda.Utils.BiMap
altM1Agda.Utils.Monad
alwaysUnblockAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
AmbiguousAgda.Interaction.FindFile
AmbiguousAnythingAgda.Syntax.Scope.Base
AmbiguousConProjsAgda.Syntax.Scope.Base
AmbiguousConstructorAgda.Syntax.Concrete.Definitions.Errors
AmbiguousDeclNameAgda.Syntax.Scope.Base
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
AmbiguousParseForApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AmbiguousParseForLHSAgda.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
AndAgda.Auto.NarrowingSearch
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
annotateAgda.Utils.Parser.MemoisedCPS
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
aoHintModeAgda.Auto.Options
aoHintsAgda.Auto.Options
aoModeAgda.Auto.Options
aoPickAgda.Auto.Options
aoTimeOutAgda.Auto.Options
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.Auto.Syntax
4 (Data Constructor)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.EtaContract
appAgda.Syntax.Abstract
appBracketsAgda.Syntax.Fixity
appBrackets'Agda.Syntax.Fixity
appDef'Agda.TypeChecking.Reduce
appDefE'Agda.TypeChecking.Reduce
appElimsAgda.Auto.Syntax
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
appHeadAgda.Auto.Syntax
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 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
3 (Type/Class)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
6 (Type/Class)Agda.Utils.TypeLevel
apply 
1 (Function)Agda.Compiler.JS.Substitution
2 (Function)Agda.Utils.AssocList
3 (Function)Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
apply1Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applyCohesionAgda.Syntax.Common
applyCohesionToContextAgda.TypeChecking.Irrelevance
applyCohesionToContextOnlyAgda.TypeChecking.Irrelevance
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.Irrelevance
applyModalityToContextFunBodyAgda.TypeChecking.Irrelevance
applyModalityToContextOnlyAgda.TypeChecking.Irrelevance
applyModalityToJudgementOnlyAgda.TypeChecking.Irrelevance
applyNAgda.TypeChecking.Names
applyN'Agda.TypeChecking.Names
applyNLPatSubstAgda.TypeChecking.Substitute
applyNLSubstToDomAgda.TypeChecking.Substitute
ApplyOrIApplyAgda.TypeChecking.Coverage.Match
applyPatSubstAgda.TypeChecking.Substitute
applypermAgda.Auto.CaseSplit
applyQuantityAgda.Syntax.Common
applyQuantityToContextAgda.TypeChecking.Irrelevance
applyQuantityToJudgementOnlyAgda.TypeChecking.Irrelevance
applyRelevanceAgda.Syntax.Common
applyRelevanceToContextAgda.TypeChecking.Irrelevance
applyRelevanceToContextFunBodyAgda.TypeChecking.Irrelevance
applyRelevanceToContextOnlyAgda.TypeChecking.Irrelevance
applyRelevanceToJudgementOnlyAgda.TypeChecking.Irrelevance
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
applyWhenAgda.Utils.Function
applyWhenMAgda.Utils.Function
applyWhenVerboseSAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend
appOKAgda.Auto.Syntax
appOriginAgda.Syntax.Info
AppPAgda.Syntax.Concrete
appPAgda.Syntax.Concrete.Operators.Parser
appParensAgda.Syntax.Info
appRangeAgda.Syntax.Info
approxConInductionAgda.Syntax.Scope.Base
appTelAgda.TypeChecking.Names
appUIdAgda.Auto.Syntax
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
ArgListAgda.Auto.Syntax
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.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 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Type/Class)Agda.Interaction.JSON
3 (Data Constructor)Agda.Interaction.JSON
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
askGhcOptsAgda.Compiler.MAlonzo.Compiler
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
asPatternsAgda.TypeChecking.Rules.LHS.Problem
AsPatternShadowsConstructorOrPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
AsPatternShadowsConstructorOrPatternSynonym_Agda.Interaction.Options.Warnings
AspectAgda.Interaction.Highlighting.Precise
aspectAgda.Interaction.Highlighting.Precise
Aspects 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)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
AssignmentsAgda.Auto.CaseSplit
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
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
AttributeAgda.Syntax.Concrete.Attribute
attributesForModalityAgda.Syntax.Concrete.Pretty
attributesMapAgda.Syntax.Concrete.Attribute
augCallInfoAgda.Termination.CallMatrix
augCallMatrixAgda.Termination.CallMatrix
autoAgda.Auto.Auto
AutoHintModeAgda.Auto.Options
autoHintModeAgda.Auto.Options
autoHintsAgda.Auto.Options
autoInlineAgda.TypeChecking.Inlining
autoMessageAgda.Auto.Auto
autoModeAgda.Auto.Options
AutoOptions 
1 (Type/Class)Agda.Auto.Options
2 (Data Constructor)Agda.Auto.Options
autoPickAgda.Auto.Options
AutoProgressAgda.Auto.Auto
autoProgressAgda.Auto.Auto
AutoResult 
1 (Type/Class)Agda.Auto.Auto
2 (Data Constructor)Agda.Auto.Auto
autoTimeOutAgda.Auto.Options
AutoTokenAgda.Auto.Options
autoTokensAgda.Auto.Options
AwakeConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Axiom 
1 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
2 (Data Constructor)Agda.Syntax.Reflected
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