Agda-2.6.2.0.20211129: 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
absBodyAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
abslamvarnameAgda.Auto.Convert
AbsModuleAgda.Syntax.Scope.Base
AbsNameAgda.Syntax.Scope.Base
absNameAgda.Syntax.Internal
AbsNameWithFixity 
1 (Type/Class)Agda.TypeChecking.Serialise.Instances.Abstract
2 (Data Constructor)Agda.TypeChecking.Serialise.Instances.Abstract
AbsOfConAgda.Syntax.Translation.ConcreteToAbstract
AbsOfRefAgda.Syntax.Translation.ReflectedToAbstract
absoluteAgda.Utils.FileName
AbsolutePath 
1 (Type/Class)Agda.Utils.FileName
2 (Data Constructor)Agda.Utils.FileName
absPathDAgda.TypeChecking.Serialise.Base
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.Compiler.Backend, Agda.TypeChecking.Monad
AbstractDefAgda.Syntax.Common
AbstractDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AbstractMode 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AbstractModuleAgda.Syntax.Scope.Base
AbstractNameAgda.Syntax.Scope.Base
AbstractRHSAgda.Syntax.Translation.ConcreteToAbstract
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
AbsurdPatternRequiresNoRHS_Agda.Interaction.Options.Warnings
absurdPatternsAgda.TypeChecking.Rules.LHS.Problem
AbsurdRHS 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
acceptableFileExtsAgda.Syntax.Parser
AccessAgda.Syntax.Common
acConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Account 
1 (Type/Class)Agda.Utils.Benchmark
2 (Type/Class)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
acDataAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
acElimsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
aConAgda.Syntax.Treeless, Agda.Compiler.Backend
acRangesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ACStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Action 
1 (Type/Class)Agda.TypeChecking.CheckInternal
2 (Data Constructor)Agda.TypeChecking.CheckInternal
activateLoadedFileCacheAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
activeBackendAgda.Compiler.Backend
activeBackendMayEraseTypeAgda.Compiler.Backend
acTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
acyclicAgda.Utils.Graph.AdjacencyMap.Unidirectional
add 
1 (Function)Agda.Termination.Semiring
2 (Function)Agda.Termination.SparseMatrix
addAndUnblockerAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addAwakeConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addAwakeConstraint'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addblkAgda.Auto.Typecheck
addClausesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addCoercionsAgda.Compiler.MAlonzo.Coerce
addCohesionAgda.Syntax.Common
addColumnAgda.Termination.SparseMatrix
addCompilerPragmaAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addCompositionForRecordAgda.TypeChecking.Rules.Record
addConstantAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addConstant'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addConstraint 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addConstraint'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addConstraintTCMAgda.TypeChecking.Constraints
addConstraintToAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
AddContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addCPUTimeAgda.Utils.Benchmark
addCtxAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addDataConsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addDefaultLibrariesAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addDisplayFormAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addDisplayFormsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addEdge 
1 (Function)Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Function)Agda.Utils.Warshall
addendAgda.Auto.Typecheck
AddExtraRefAgda.Auto.NarrowingSearch
addFinalNewLineAgda.Utils.String
addFlexAgda.Utils.Warshall
addFlexRigAgda.TypeChecking.Free.Lazy
addForeignCodeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addImportAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
addImportCycleCheckAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
addImportedInstancesAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addLetBindingAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addLetBinding'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addLoneSigAgda.Syntax.Concrete.Definitions.Monad
addModalityAgda.Syntax.Common
addModuleToScopeAgda.Syntax.Scope.Base
addNamedInstanceAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addNameToScopeAgda.Syntax.Scope.Base
addNodeAgda.Utils.Warshall
addOrUnblockerAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
addPragmaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addQuantityAgda.Syntax.Common
addRecordNameContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
addRelevanceAgda.Syntax.Common
addRewriteRulesAgda.TypeChecking.Rewriting
addRewriteRulesForAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addRowAgda.Termination.SparseMatrix
addSectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
addSuffixAgda.Utils.Suffix
addtrailingargsAgda.Auto.Syntax
addTrustedExecutablesAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addTypedInstanceAgda.TypeChecking.Telescope
addTypedPatternsAgda.TypeChecking.Rules.Term
addUniqueIntsAgda.Utils.Graph.AdjacencyMap.Unidirectional
addUnknownInstanceAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
addVarToBindAgda.Syntax.Scope.Monad
addWarningAgda.TypeChecking.Warnings
ADefAgda.TypeChecking.Positivity
aDefToModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
AllowAmbiguousNamesAgda.Syntax.Scope.Base
AllowedReductionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AllowedReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AllowedVarAgda.TypeChecking.MetaVars.Occurs
allowedVarsAgda.TypeChecking.MetaVars.Occurs
allowNonTerminatingReductionsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
allProjElimsAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
allReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
AmbiguousFunClausesAgda.Syntax.Concrete.Definitions.Errors
AmbiguousLibAgda.Interaction.Library.Base
AmbiguousModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousNothingAgda.Syntax.Scope.Base
AmbiguousParseForApplicationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousParseForLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbiguousQNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
AmbiguousTopLevelModuleNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
aModeToDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Auto.Syntax
3 (Data Constructor)Agda.Syntax.Concrete
4 (Data Constructor)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.EtaContract
appAgda.Syntax.Abstract
appBracketsAgda.Syntax.Fixity
appBrackets'Agda.Syntax.Fixity
appDefAgda.TypeChecking.Reduce
appDef'Agda.TypeChecking.Reduce
appDefEAgda.TypeChecking.Reduce
appDefE'Agda.TypeChecking.Reduce
appDefE_Agda.TypeChecking.Reduce
appDef_Agda.TypeChecking.Reduce
appElimsAgda.Auto.Syntax
appendAgda.Utils.List1
appendArgNamesAgda.Syntax.Common
appendListAgda.Utils.List1
appHeadAgda.Auto.Syntax
AppInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
appInteractionOutputCallbackAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
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.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
applySection'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
applySplitPSubstAgda.TypeChecking.Coverage.Match
applySubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
applySubstTermAgda.TypeChecking.Substitute
applyTermEAgda.TypeChecking.Substitute
applyUnlessAgda.Utils.Function
applyUnlessMAgda.Utils.Function
applyWhenAgda.Utils.Function
applyWhenMAgda.Utils.Function
applyWhenVerboseSAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Reduce.Monad, Agda.TypeChecking.Monad
appOKAgda.Auto.Syntax
appOriginAgda.Syntax.Info
AppPAgda.Syntax.Concrete
appPAgda.Syntax.Concrete.Operators.Parser
appParensAgda.Syntax.Info
appRangeAgda.Syntax.Info
approxConInductionAgda.Syntax.Scope.Base
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.Compiler.Backend, Agda.TypeChecking.Monad
apTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ArcAgda.Utils.Warshall
areWeCachingAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
Arg 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
ArgDescrAgda.Interaction.Options
argFromDomAgda.Syntax.Internal
argHAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
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, Agda.TypeChecking.Primitive.Base
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.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Compiler.Backend, Agda.TypeChecking.Reduce.Monad, Agda.TypeChecking.Monad
asksTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
askTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
assignTermTCM'Agda.TypeChecking.MetaVars
assignVAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
assignWrapperAgda.TypeChecking.MetaVars
AsSizesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AssociativityAgda.Syntax.Common
AssocListAgda.Utils.AssocList
AsTermsOfAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AsTypesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
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.Compiler.Backend, Agda.TypeChecking.Monad
axiomConstTranspAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
AxiomNameAgda.Syntax.Scope.Base
axiomNameAgda.Syntax.Abstract