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

Index - C

C 
1 (Data Constructor)Agda.Auto.Options
2 (Type/Class)Agda.Utils.Cluster
cacheCurrentLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CachedTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cachingStartsAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CActionAgda.Auto.Syntax
calcAgda.Auto.NarrowingSearch
calcEqRStateAgda.Auto.Typecheck
CALConcatAgda.Auto.Syntax
Call 
1 (Type/Class)Agda.Termination.CallGraph
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callBackendAgda.Compiler.Backend
callByNameAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CallCombAgda.Termination.CallMatrix
callCompilerAgda.Compiler.CallCompiler
callCompiler'Agda.Compiler.CallCompiler
callGHCAgda.Compiler.MAlonzo.Compiler
CallGraph 
1 (Type/Class)Agda.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
CallInfo 
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
callInfoCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callInfoRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callInfosAgda.Termination.Monad
callInfoTargetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CallMatrix 
1 (Type/Class)Agda.Termination.CallMatrix
2 (Data Constructor)Agda.Termination.CallMatrix
CallMatrix'Agda.Termination.CallMatrix
CallMatrixAug 
1 (Type/Class)Agda.Termination.CallMatrix
2 (Data Constructor)Agda.Termination.CallMatrix
callMatrixSetAgda.Termination.CallGraph
CallPath 
1 (Type/Class)Agda.Termination.Monad
2 (Data Constructor)Agda.Termination.Monad
CALNilAgda.Auto.Syntax
Candidate 
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
candidateOverlappableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotCreateMissingClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotEliminateWithPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotResolveAmbiguousPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canonicalizeSizeConstraintAgda.TypeChecking.SizedTypes.Solve
canonicalNameAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canProjectAgda.TypeChecking.Substitute
CantGeneralizeOverSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CantGeneralizeOverSorts_Agda.Interaction.Options.Warnings
CantInvertAgda.TypeChecking.MetaVars
CantResolveOverloadedConstructorsTargetingSameDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConIdxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitFailuresAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitGivenIdxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cArgUsageAgda.Syntax.Treeless, Agda.Compiler.Backend
CarrierAgda.Utils.Zipper
Case 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.CompiledClause
3 (Type/Class)Agda.TypeChecking.CompiledClause
CaseContextAgda.Interaction.MakeCase
caseEitherMAgda.Utils.Either
CaseInfo 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
caseLazyAgda.Syntax.Treeless, Agda.Compiler.Backend
caseListAgda.Utils.List
caseListMAgda.Utils.List
caseListTAgda.Utils.ListT
caseMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
caseMaybeM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
CaseSplitAgda.Syntax.Common
caseSplitSearchAgda.Auto.CaseSplit
caseSplitSearch'Agda.Auto.CaseSplit
caseToSeqAgda.Compiler.Treeless.Uncase
CaseTypeAgda.Syntax.Treeless, Agda.Compiler.Backend
caseTypeAgda.Syntax.Treeless, Agda.Compiler.Backend
castConstraintToCurrentContextAgda.TypeChecking.SizedTypes.Solve
castConstraintToCurrentContext'Agda.TypeChecking.SizedTypes.Solve
catAgda.Utils.Pretty
catchAllAgda.TypeChecking.CompiledClause
catchAllBranchAgda.TypeChecking.CompiledClause
CatchallClauseAgda.Interaction.Highlighting.Precise
CatchallPragmaAgda.Syntax.Concrete
catchAndPrintImpossibleAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchErrorAgda.Utils.Except
catchError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchIlltypedPatternBlockedOnMetaAgda.TypeChecking.Rules.Term
CatchImpossibleAgda.Utils.Impossible
catchImpossibleAgda.Utils.Impossible
catchImpossibleJustAgda.Utils.Impossible
CatchIOAgda.Utils.IO
catchIOAgda.Utils.IO
catchPatternErrAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchPatternErrTCMAgda.TypeChecking.Constraints
categorizedeclAgda.Auto.Syntax
catMaybes 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
catMaybesMPAgda.Utils.Monad
CC 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Type/Class)Agda.Compiler.MAlonzo.Compiler
CCContextAgda.Compiler.MAlonzo.Compiler
ccContextAgda.Compiler.MAlonzo.Compiler
CCEnv 
1 (Type/Class)Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor)Agda.Compiler.MAlonzo.Compiler
ccNameSupplyAgda.Compiler.MAlonzo.Compiler
cdcontAgda.Auto.Syntax
cddeffreevarsAgda.Auto.Syntax
cdnameAgda.Auto.Syntax
cdoriginAgda.Auto.Syntax
cdtypeAgda.Auto.Syntax
CExpAgda.Auto.Syntax
ChangeAgda.Utils.Update
ChangeTAgda.Utils.Update
Char 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
charAgda.Utils.Pretty
chaseDisplayFormsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
chaseMsgAgda.Interaction.Imports
checkAbsurdLambdaAgda.TypeChecking.Rules.Term
checkAliasAgda.TypeChecking.Rules.Def
checkApplicationAgda.TypeChecking.Rules.Application
CheckArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkArgumentsAgda.TypeChecking.Rules.Application
checkArguments_Agda.TypeChecking.Rules.Application
checkAxiomAgda.TypeChecking.Rules.Decl
checkAxiom'Agda.TypeChecking.Rules.Decl
CheckClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkClauseAgda.TypeChecking.Rules.Def
checkClauseLHSAgda.TypeChecking.Rules.Def
checkCoinductiveRecordsAgda.TypeChecking.Rules.Decl
checkCompilerPragmasAgda.Compiler.JS.Compiler
CheckConfluenceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConfluenceOfClauseAgda.TypeChecking.Rewriting.Confluence
checkConfluenceOfRulesAgda.TypeChecking.Rewriting.Confluence
CheckConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConstructorAgda.TypeChecking.Rules.Data
checkConstructorCountAgda.Compiler.MAlonzo.HaskellTypes
CheckConstructorFitsInAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConstructorTypeAgda.Compiler.MAlonzo.Compiler
checkCoverAgda.Compiler.MAlonzo.Compiler
CheckDataDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkDataDefAgda.TypeChecking.Rules.Data
checkDeclAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclCachedAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclsAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDisplayPragmaAgda.TypeChecking.Rules.Display
checkDontExpandLastAgda.TypeChecking.Rules.Term
CheckDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckedTarget 
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
checkeliminandAgda.Auto.Typecheck
checkEmptyTelAgda.TypeChecking.Empty
CheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExprAgda.TypeChecking.Rules.Term, Agda.TheTypeChecker
checkExpr'Agda.TypeChecking.Rules.Term
CheckExprCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExtendedLambdaAgda.TypeChecking.Rules.Term
checkForImportCycleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckFunDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDefAgda.TypeChecking.Rules.Def
checkFunDef'Agda.TypeChecking.Rules.Def
CheckFunDefCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDefSAgda.TypeChecking.Rules.Def
checkGeneralizeAgda.TypeChecking.Rules.Decl
checkGeneralizeTelescopeAgda.TypeChecking.Rules.Term
checkIApplyConfluenceAgda.TypeChecking.IApplyConfluence
checkIApplyConfluence_Agda.TypeChecking.IApplyConfluence
checkImportAgda.TypeChecking.Rules.Decl
checkIndexSortsAgda.TypeChecking.Rules.Data
checkInjectivityAgda.TypeChecking.Injectivity
checkInjectivity'Agda.TypeChecking.Injectivity
checkInjectivity_Agda.TypeChecking.Rules.Decl
checkInternalAgda.TypeChecking.CheckInternal
checkInternal'Agda.TypeChecking.CheckInternal
CheckIsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkKnownArgumentAgda.TypeChecking.Rules.Term
checkKnownArgumentsAgda.TypeChecking.Rules.Term
CheckLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLambdaAgda.TypeChecking.Rules.Term
checkLazyMatchAgda.TypeChecking.CompiledClause
checkLeftHandSideAgda.TypeChecking.Rules.LHS
CheckLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLetBindingAgda.TypeChecking.Rules.Term
checkLetBindingsAgda.TypeChecking.Rules.Term
checkLevelAgda.TypeChecking.Rules.Term
CheckLHS 
1 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLinearityAgda.TypeChecking.MetaVars
checkLiteralAgda.TypeChecking.Rules.Term
checkMacroTypeAgda.TypeChecking.Rules.Def
checkMetaAgda.TypeChecking.Rules.Term
CheckMetaInstAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkMetaInstAgda.TypeChecking.MetaVars
CheckMetaSolutionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkModuleArityAgda.TypeChecking.Rules.Decl
checkModuleNameAgda.Interaction.FindFile
checkMutualAgda.TypeChecking.Rules.Decl
checkNamedArgAgda.TypeChecking.Rules.Term
CheckNamedWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkNoFixityInRenamingModuleAgda.Syntax.Scope.Monad
checkNoShadowingAgda.Syntax.Scope.Monad
checkOptionsCompatibleAgda.Interaction.Imports
checkOptsAgda.Interaction.Options
checkOrInferMetaAgda.TypeChecking.Rules.Term
checkOverapplicationAgda.TypeChecking.Injectivity
checkPathAgda.TypeChecking.Rules.Term
CheckPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPatternLinearityAgda.Syntax.Abstract.Pattern
checkPiTelescopeAgda.TypeChecking.Rules.Term
checkpointAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckpointId 
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
checkpointSubstitutionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkpointSubstitution'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPositivity_Agda.TypeChecking.Rules.Decl
checkPostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
checkPostponedLambdaAgda.TypeChecking.Rules.Term
CheckPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPragmaAgda.TypeChecking.Rules.Decl
CheckPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPrimitiveAgda.TypeChecking.Rules.Decl
CheckProjAppToKnownPrincipalArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjAppToKnownPrincipalArgAgda.TypeChecking.Rules.Application
CheckProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjectionLikeness_Agda.TypeChecking.Rules.Decl
checkQuestionMarkAgda.TypeChecking.Rules.Term
CheckRecDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkRecDefAgda.TypeChecking.Rules.Record
checkRecordExpressionAgda.TypeChecking.Rules.Term
checkRecordProjectionsAgda.TypeChecking.Rules.Record
checkRecordUpdateAgda.TypeChecking.Rules.Term
checkRewriteRuleAgda.TypeChecking.Rewriting
CheckRHSAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkRHSAgda.TypeChecking.Rules.Def
checkSectionAgda.TypeChecking.Rules.Decl
CheckSectionApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSectionApplicationAgda.TypeChecking.Rules.Decl
checkSectionApplication'Agda.TypeChecking.Rules.Decl
checkSizeIndexAgda.TypeChecking.Polarity
CheckSizeLtSatAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSizeLtSatAgda.TypeChecking.SizedTypes
checkSizeNeverZeroAgda.TypeChecking.SizedTypes
checkSizeVarNeverZeroAgda.TypeChecking.SizedTypes
checkSolutionForMetaAgda.TypeChecking.MetaVars
checkSortAgda.TypeChecking.CheckInternal
checkSortOfSplitVarAgda.TypeChecking.Rules.LHS
checkStrictlyPositiveAgda.TypeChecking.Positivity
checkSubtypeIsEqualAgda.TypeChecking.MetaVars
checkSyntacticEqualityAgda.TypeChecking.SyntacticEquality
checkSystemCoverageAgda.TypeChecking.Rules.Def
checkTacticAttributeAgda.TypeChecking.Rules.Term
CheckTargetTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkTelePiSortAgda.TypeChecking.Sort
checkTelescopeAgda.TypeChecking.Rules.Term
checkTelescope'Agda.TypeChecking.Rules.Term
checkTermination_Agda.TypeChecking.Rules.Decl
checkTypeAgda.TypeChecking.CheckInternal
checkType'Agda.TypeChecking.CheckInternal
checkTypeCheckingProblemAgda.TypeChecking.Constraints
checkTypedBindingsAgda.TypeChecking.Rules.Term
checkTypeOfMainAgda.Compiler.MAlonzo.Primitives
checkTypeSignatureAgda.TypeChecking.Rules.Decl
checkTypeSignature'Agda.TypeChecking.Rules.Decl
checkUnderscoreAgda.TypeChecking.Rules.Term
checkUnquoteDeclAgda.TypeChecking.Rules.Decl
checkUnquoteDefAgda.TypeChecking.Rules.Decl
checkWhereAgda.TypeChecking.Rules.Def
checkWithFunctionAgda.TypeChecking.Rules.Def
CheckWithFunctionTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkWithRHSAgda.TypeChecking.Rules.Def
ChoiceAgda.Auto.NarrowingSearch
choiceAgda.TypeChecking.Unquote
choicePAgda.Utils.Parser.MemoisedCPS
chooseAgda.Auto.NarrowingSearch
ChooseEitherAgda.TypeChecking.Rules.LHS.Problem
ChooseFlexAgda.TypeChecking.Rules.LHS.Problem
chooseFlexAgda.TypeChecking.Rules.LHS.Problem
chooseHighlightingMethodAgda.Interaction.Highlighting.Common
ChooseLeftAgda.TypeChecking.Rules.LHS.Problem
choosePrioMetaAgda.Auto.NarrowingSearch
ChooseRightAgda.TypeChecking.Rules.LHS.Problem
chopAgda.Utils.List
chopWhenAgda.Utils.List
ChrAgda.Utils.Pretty
Cl 
1 (Type/Class)Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor)Agda.TypeChecking.CompiledClause.Compile
clAgda.TypeChecking.Names
cl'Agda.TypeChecking.Names
ClashesViaRenamingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashesViaRenaming_Agda.Interaction.Options.Warnings
ClashingDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingFileNamesForAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModuleImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
classifyForeignAgda.Compiler.MAlonzo.Pragmas
classifyPragmaAgda.Compiler.MAlonzo.Pragmas
classifyWarningAgda.TypeChecking.Warnings
classifyWarningsAgda.TypeChecking.Warnings
Clause 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Reflected
6 (Type/Class)Agda.Syntax.Abstract
7 (Data Constructor)Agda.Syntax.Abstract
8 (Type/Class)Agda.Syntax.Concrete.Definitions
9 (Data Constructor)Agda.Syntax.Concrete.Definitions
Clause'Agda.Syntax.Abstract
clauseArgsAgda.Syntax.Internal.Pattern
clauseBodyAgda.Syntax.Internal
clauseCatchall 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Abstract
clauseElimsAgda.Syntax.Internal.Pattern
clauseEllipsisAgda.Syntax.Internal
clauseFullRangeAgda.Syntax.Internal
clauseLHSAgda.Syntax.Abstract
clauseLHSRangeAgda.Syntax.Internal
clausePatsAgda.Syntax.Internal
clausePermAgda.Syntax.Internal.Pattern
clauseQNameAgda.TypeChecking.Rewriting.Clause
clauseRecursiveAgda.Syntax.Internal
clauseRHSAgda.Syntax.Abstract
ClausesPostChecksAgda.TypeChecking.Rules.Def
clauseStrippedPatsAgda.Syntax.Abstract
clauseTelAgda.Syntax.Internal
clauseToRewriteRuleAgda.TypeChecking.Rewriting.Clause
clauseToSplitClauseAgda.TypeChecking.Coverage
clauseTypeAgda.Syntax.Internal
clauseUnreachableAgda.Syntax.Internal
clauseWhereDeclsAgda.Syntax.Abstract
ClauseZipperAgda.Interaction.MakeCase
clBodyAgda.TypeChecking.CompiledClause.Compile
CleanAgda.TypeChecking.Unquote
cleanAgda.Utils.Graph.AdjacencyMap.Unidirectional
cleanCachedLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearAnonInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearRunningInfoAgda.Interaction.EmacsCommand
clearWarningAgda.Interaction.EmacsCommand
clEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClockTimeAgda.Utils.Time
Clos 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
closeBraceAgda.Syntax.Parser.Layout
closedAgda.TypeChecking.Free
ClosedLevelAgda.Syntax.Internal
closedTermAgda.Compiler.MAlonzo.Compiler
closedTermToTreelessAgda.Compiler.ToTreeless
ClosedTypeAgda.TypeChecking.Rules.Data
closeVerboseBracketAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
closifyAgda.Auto.Syntax
Closure 
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
clPatsAgda.TypeChecking.CompiledClause.Compile
ClsAgda.TypeChecking.CompiledClause.Compile
clScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clusterAgda.Utils.Cluster
cluster'Agda.Utils.Cluster
clValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cmdToNameAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Cmd_abortAgda.Interaction.Base
Cmd_autoAllAgda.Interaction.Base
Cmd_autoOneAgda.Interaction.Base
Cmd_compileAgda.Interaction.Base
Cmd_computeAgda.Interaction.Base
Cmd_compute_toplevelAgda.Interaction.Base
Cmd_constraintsAgda.Interaction.Base
Cmd_contextAgda.Interaction.Base
Cmd_elaborate_giveAgda.Interaction.Base
Cmd_exitAgda.Interaction.Base
Cmd_giveAgda.Interaction.Base
Cmd_goal_typeAgda.Interaction.Base
Cmd_goal_type_contextAgda.Interaction.Base
cmd_goal_type_context_andAgda.Interaction.InteractionTop
Cmd_goal_type_context_checkAgda.Interaction.Base
Cmd_goal_type_context_inferAgda.Interaction.Base
Cmd_helper_functionAgda.Interaction.Base
Cmd_highlightAgda.Interaction.Base
Cmd_inferAgda.Interaction.Base
Cmd_infer_toplevelAgda.Interaction.Base
Cmd_introAgda.Interaction.Base
Cmd_loadAgda.Interaction.Base
cmd_load'Agda.Interaction.InteractionTop
Cmd_load_highlighting_infoAgda.Interaction.Base
Cmd_make_caseAgda.Interaction.Base
Cmd_metasAgda.Interaction.Base
Cmd_refineAgda.Interaction.Base
Cmd_refine_or_introAgda.Interaction.Base
Cmd_search_about_toplevelAgda.Interaction.Base
Cmd_show_module_contentsAgda.Interaction.Base
Cmd_show_module_contents_toplevelAgda.Interaction.Base
Cmd_show_versionAgda.Interaction.Base
Cmd_solveAllAgda.Interaction.Base
Cmd_solveOneAgda.Interaction.Base
Cmd_tokenHighlightingAgda.Interaction.Base
Cmd_why_in_scopeAgda.Interaction.Base
Cmd_why_in_scope_toplevelAgda.Interaction.Base
CMFBlockedAgda.Auto.Typecheck
CMFFlexAgda.Auto.Typecheck
CMFlex 
1 (Type/Class)Agda.Auto.Typecheck
2 (Data Constructor)Agda.Auto.Typecheck
CMFSemiAgda.Auto.Typecheck
CModeAgda.Auto.Typecheck
CmpAgda.TypeChecking.SizedTypes.Syntax
cmpAgda.TypeChecking.SizedTypes.Syntax
CmpElimAgda.Interaction.Base
CmpEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpInTypeAgda.Interaction.Base
CmpLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpLevelsAgda.Interaction.Base
CmpSortsAgda.Interaction.Base
CmpTelesAgda.Interaction.Base
CmpTypesAgda.Interaction.Base
CMRigidAgda.Auto.Typecheck
CMSet 
1 (Type/Class)Agda.Termination.CallMatrix
2 (Data Constructor)Agda.Termination.CallMatrix
cmSetAgda.Termination.CallMatrix
CodeAgda.Syntax.Parser.Literate
code 
1 (Function)Agda.Syntax.Parser.Lexer
2 (Function)Agda.Interaction.Highlighting.HTML
CoDomainAgda.Utils.TypeLevel
CoDomain'Agda.Utils.TypeLevel
coerceAgda.TypeChecking.Conversion
coerceAppViewAgda.Syntax.Treeless, Agda.Compiler.Backend
coerceSizeAgda.TypeChecking.Conversion
coerceViewAgda.Syntax.Treeless, Agda.Compiler.Backend
CohesionAgda.Syntax.Common
CohesionAttributeAgda.Syntax.Concrete.Attribute
cohesionAttributeTableAgda.Syntax.Concrete.Attribute
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKit'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInductiveAgda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInfectiveImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInfectiveImport_Agda.Interaction.Options.Warnings
coinfectiveOptionsAgda.Interaction.Options
colAgda.Termination.SparseMatrix
coldescrAgda.Utils.Warshall
collapseDefaultAgda.Utils.WithDefault
collapseOAgda.Termination.Order
collectStatsAgda.TypeChecking.Serialise.Base
colon 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
colsAgda.Termination.SparseMatrix
combineHashesAgda.Utils.Hash
comma 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
Command 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
3 (Type/Class)Agda.Interaction.CommandLine
Command'Agda.Interaction.Base
commandLineFlagsAgda.Compiler.Backend
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CommandMAgda.Interaction.Base
commandMToIOAgda.Interaction.InteractionTop
CommandQueue 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
commandQueueAgda.Interaction.Base
commandsAgda.Interaction.Base
CommandState 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
Comment 
1 (Data Constructor)Agda.Syntax.Parser.Literate
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
commitInfoAgda.VersionCommit
commonParentModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
commonPredsAgda.TypeChecking.SizedTypes.WarshallSolver
commonPrefixAgda.Utils.List
commonSuccsAgda.TypeChecking.SizedTypes.WarshallSolver
commonSuffixAgda.Utils.List
comp'Agda.Auto.Typecheck
CompactionAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compactPAgda.Utils.Permutation
compactSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
ComparableAgda.Utils.PartialOrd
comparableAgda.Utils.PartialOrd
comparableOrdAgda.Utils.PartialOrd
CompareAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compareArgsAgda.TypeChecking.Conversion
CompareAsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compareAsAgda.TypeChecking.Conversion
compareAs'Agda.TypeChecking.Conversion
compareAsDirAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareAtomDirAgda.TypeChecking.Conversion
compareBelowMaxAgda.TypeChecking.SizedTypes
compareCohesionAgda.TypeChecking.Conversion
CompareDirectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compareDomAgda.TypeChecking.Conversion
compareElimsAgda.TypeChecking.Conversion
compareFavoritesAgda.Utils.Favorites
compareFloatAgda.Syntax.Literal
compareIntervalAgda.TypeChecking.Conversion
compareIrrelevantAgda.TypeChecking.Conversion
compareLevelAgda.TypeChecking.Conversion
compareMaxViewsAgda.TypeChecking.SizedTypes
compareOffsetAgda.TypeChecking.SizedTypes.Syntax
compareQuantityAgda.TypeChecking.Conversion
compareRelevanceAgda.TypeChecking.Conversion
CompareResultAgda.Utils.Favorites
compareSizesAgda.TypeChecking.SizedTypes
compareSizeViewsAgda.TypeChecking.SizedTypes
compareSortAgda.TypeChecking.Conversion
compareTelAgda.TypeChecking.Conversion
compareTermAgda.TypeChecking.Conversion
compareTerm'Agda.TypeChecking.Conversion
compareTermOnFaceAgda.TypeChecking.Conversion
compareTermOnFace'Agda.TypeChecking.Conversion
compareTypeAgda.TypeChecking.Conversion
compareWithFavoritesAgda.Utils.Favorites
compareWithPolAgda.TypeChecking.Conversion
ComparisonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compGlueAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
compHCompUAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
CompilationErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compileAgda.TypeChecking.CompiledClause.Compile
compileAltAgda.Compiler.JS.Compiler
compileClausesAgda.TypeChecking.CompiledClause.Compile
compileClauses'Agda.TypeChecking.CompiledClause.Compile
Compiled 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
compiledClauseBodyAgda.TypeChecking.Substitute
CompiledClausesAgda.TypeChecking.CompiledClause
CompiledClauses'Agda.TypeChecking.CompiledClause
compiledcondeclAgda.Compiler.MAlonzo.Compiler
compileDefAgda.Compiler.Backend
compileDirAgda.Compiler.Common
CompiledRepresentationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compiledTypeSynonymAgda.Compiler.MAlonzo.Compiler
CompilePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compilePrim 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
CompilerBackendAgda.Interaction.Base
CompilerPragma 
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
compileTermAgda.Compiler.JS.Compiler
compileTerm'Agda.Compiler.JS.Compiler
compileWithSplitTreeAgda.TypeChecking.CompiledClause.Compile
CompKit 
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
complementAgda.Utils.SmallSet
complete 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.Termination.CallGraph
completeIterAgda.Utils.Graph.AdjacencyMap.Unidirectional
completionStepAgda.Termination.CallGraph
composeAgda.TypeChecking.SizedTypes.Utils
composeCohesionAgda.Syntax.Common
composeFlexRigAgda.TypeChecking.Free.Lazy
composeModalityAgda.Syntax.Common
composePAgda.Utils.Permutation
composePolAgda.TypeChecking.Polarity
composeQuantityAgda.Syntax.Common
composeRelevanceAgda.Syntax.Common
composeSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
composeVarOccAgda.TypeChecking.Free.Lazy
composeWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
ComposeZipAgda.Utils.Zipper
ComposeZipperAgda.Utils.Zipper
CompressAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compressAgda.Interaction.Highlighting.Precise
CompressedFile 
1 (Type/Class)Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
compressedFileInvariantAgda.Interaction.Highlighting.Precise
computeEdgesAgda.TypeChecking.Positivity
computeElimHeadTypeAgda.TypeChecking.Conversion
computeErasedConstructorArgsAgda.Compiler.Treeless.Erase
computeFixitiesAndPolaritiesAgda.Syntax.Scope.Monad
computeForcingAnnotationsAgda.TypeChecking.Forcing
computeIgnoreAbstractAgda.Interaction.BasicOps
ComputeModeAgda.Interaction.Base
computeNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
ComputeOccurrencesAgda.TypeChecking.Positivity
computeOccurrencesAgda.TypeChecking.Positivity
computeOccurrences'Agda.TypeChecking.Positivity
computePolarityAgda.TypeChecking.Polarity
computeSizeConstraintAgda.TypeChecking.SizedTypes.Solve
computeUnsolvedConstraintsAgda.Interaction.Highlighting.Generate
computeUnsolvedMetaWarningsAgda.Interaction.Highlighting.Generate
computeWrapInputAgda.Interaction.BasicOps
Con 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Syntax.Abstract
conAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conAppAgda.TypeChecking.Substitute
ConArgTypeAgda.TypeChecking.Positivity.Occurrence
conArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conBranchesAgda.TypeChecking.CompiledClause
conCaseAgda.TypeChecking.CompiledClause
ConcatAgda.TypeChecking.Positivity
Concat'Agda.TypeChecking.Positivity
concatargsAgda.Auto.CaseSplit
concatListTAgda.Utils.ListT
conCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
concreteNamesInScopeAgda.Syntax.Scope.Base
concreteOptionsToOptionPragmasAgda.Interaction.Imports
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract
conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConDecl 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Utils.Haskell.Syntax
condeclAgda.Compiler.MAlonzo.Compiler
ConditionAgda.TypeChecking.MetaVars
conErasedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conFieldsAgda.Syntax.Internal
ConfluenceProblemAgda.Interaction.Highlighting.Precise
conForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConGraphAgda.TypeChecking.SizedTypes.WarshallSolver
ConGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
ConHead 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
conhqnAgda.Compiler.MAlonzo.Misc
conIndAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conInductiveAgda.Syntax.Internal
ConInfoAgda.Syntax.Internal
ConInsteadOfDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConjAgda.TypeChecking.Conversion
ConNameAgda.Syntax.Scope.Base
conNameAgda.Syntax.Internal
ConnectHandleAgda.Auto.NarrowingSearch
connectInteractionPointAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConOConAgda.Syntax.Common
ConORecAgda.Syntax.Common
ConOriginAgda.Syntax.Common
ConOSplitAgda.Syntax.Common
ConOSystemAgda.Syntax.Common
ConP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
conParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConPatEagerAgda.Syntax.Info
ConPatInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
conPatInfoAgda.Syntax.Info
ConPatLazy 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
conPatLazyAgda.Syntax.Info
conPatOriginAgda.Syntax.Info
ConPatternInfo 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
conPFallThroughAgda.Syntax.Internal
conPInfoAgda.Syntax.Internal
conPLazyAgda.Syntax.Internal
conPRecordAgda.Syntax.Internal
conProjAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conPTypeAgda.Syntax.Internal
Cons 
1 (Data Constructor)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Interaction.EmacsCommand
consecutiveAndSeparatedAgda.Syntax.Position
ConsHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
consListTAgda.Utils.ListT
ConsMap0Agda.Utils.TypeLevel
ConsMap1Agda.Utils.TypeLevel
consMListTAgda.Utils.ListT
consOfHITAgda.TypeChecking.Datatypes
conSrcConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
consSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Const 
1 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Data Constructor)Agda.Auto.Syntax
ConstantAgda.Utils.TypeLevel
Constant0Agda.Utils.TypeLevel
Constant1Agda.Utils.TypeLevel
ConstDef 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
Constr 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
constrainedPrimsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraint 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class)Agda.Utils.Warshall
4 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraint'Agda.TypeChecking.SizedTypes.Syntax
constraintGraphAgda.TypeChecking.SizedTypes.WarshallSolver
constraintGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
constraintMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constraintProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraints 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstraintStatusAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstRefAgda.Auto.Syntax
constructIScopeAgda.Interaction.Imports
Constructor 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorCoverageCodeAgda.Compiler.MAlonzo.Compiler
constructorForm 
1 (Function)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.TypeChecking.Reduce.Monad
constructorForm'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorImpossibleAgda.Auto.Typecheck
ConstructorInfoAgda.TypeChecking.Datatypes
ConstructorNameAgda.Syntax.Scope.Base
ConstructorPatternInWrongDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructPatsAgda.Auto.Convert
constructsAgda.TypeChecking.Rules.Data
containsAbsurdPatternAgda.Syntax.Abstract.Pattern
containsAPatternAgda.Syntax.Abstract.Pattern
containsAsPatternAgda.Syntax.Abstract.Pattern
contains_constructorAgda.Auto.Convert
contentAgda.TypeChecking.CompiledClause
ContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextLetAgda.Interaction.Base
contextOfMetaAgda.Interaction.BasicOps
contextSizeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextVarAgda.Interaction.Base
ContinueAgda.Interaction.CommandLine
continueAfterAgda.Interaction.CommandLine
ContinueInAgda.Interaction.CommandLine
ContinuousAgda.Syntax.Common
continuousAgda.Syntax.Position
continuousPerLineAgda.Syntax.Position
ContravariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conUseSizeLtAgda.Termination.Monad
convErrorAgda.TypeChecking.Conversion
ConversionAgda.Auto.Convert
convertAgda.Auto.Convert
convertGuardsAgda.Compiler.Treeless.GuardsToPrims
CopatternReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
copatternsNotImplementedAgda.Auto.Convert
copyargAgda.Auto.Typecheck
copyDirContentAgda.Utils.IO.Directory
copyRTEModules 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
copyScopeAgda.Syntax.Scope.Monad
copyTermAgda.Syntax.Internal.Generic
CosplitCatchallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoTargetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Cost 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
costAbsurdLamAgda.Auto.SearchControl
costAddVarDepthAgda.Auto.CaseSplit
costAppConstructorAgda.Auto.SearchControl
costAppConstructorSingleAgda.Auto.SearchControl
costAppExtraRefAgda.Auto.SearchControl
costAppHintAgda.Auto.SearchControl
costAppHintUsedAgda.Auto.SearchControl
costAppRecCallAgda.Auto.SearchControl
costAppRecCallUsedAgda.Auto.SearchControl
costAppVarAgda.Auto.SearchControl
costAppVarUsedAgda.Auto.SearchControl
costCaseSplitHighAgda.Auto.CaseSplit
costCaseSplitLowAgda.Auto.CaseSplit
costCaseSplitVeryHighAgda.Auto.CaseSplit
costEqCongAgda.Auto.SearchControl
costEqEndAgda.Auto.SearchControl
costEqStepAgda.Auto.SearchControl
costEqSymAgda.Auto.SearchControl
costIncreaseAgda.Auto.SearchControl
costInferredTypeUnkownAgda.Auto.SearchControl
costIotaStepAgda.Auto.SearchControl
costLamAgda.Auto.SearchControl
costLamUnfoldAgda.Auto.SearchControl
costPiAgda.Auto.SearchControl
costSortAgda.Auto.SearchControl
costUnificationAgda.Auto.SearchControl
costUnificationIfAgda.Auto.SearchControl
costUnificationOccursAgda.Auto.SearchControl
countAgda.Utils.Bag
CountPatternVarsAgda.Syntax.Internal.Pattern
countPatternVarsAgda.Syntax.Internal.Pattern
countTelVarsAgda.Syntax.Concrete
countWithArgsAgda.TypeChecking.With
CovariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
CoverageCheckAgda.Syntax.Common
coverageCheckAgda.TypeChecking.Coverage
CoverageIssueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageIssue_Agda.Interaction.Options.Warnings
CoverageNoExactSplitAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageNoExactSplit_Agda.Interaction.Options.Warnings
CoverageProblemAgda.Interaction.Highlighting.Precise
Covering 
1 (Type/Class)Agda.TypeChecking.Coverage
2 (Data Constructor)Agda.TypeChecking.Coverage
covSplitArgAgda.TypeChecking.Coverage
covSplitClausesAgda.TypeChecking.Coverage
CPatternLikeAgda.Syntax.Concrete.Pattern
CPCAgda.TypeChecking.Rules.Def
cpcPartialSplitsAgda.TypeChecking.Rules.Def
CPUTime 
1 (Type/Class)Agda.Utils.Time
2 (Data Constructor)Agda.Utils.Time
createInterfaceAgda.Interaction.Imports
createMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createModuleAgda.Syntax.Scope.Monad
CSAbsurdAgda.Auto.CaseSplit
CSCtxAgda.Auto.CaseSplit
CSOmittedArgAgda.Auto.CaseSplit
CSPatAgda.Auto.CaseSplit
CSPatConAppAgda.Auto.CaseSplit
CSPatExpAgda.Auto.CaseSplit
CSPatIAgda.Auto.CaseSplit
CSPatVarAgda.Auto.CaseSplit
CSWithAgda.Auto.CaseSplit
CTCharAgda.Syntax.Treeless, Agda.Compiler.Backend
CTDataAgda.Syntax.Treeless, Agda.Compiler.Backend
CTFloatAgda.Syntax.Treeless, Agda.Compiler.Backend
cthandlesAgda.Auto.NarrowingSearch
CTIntAgda.Syntax.Treeless, Agda.Compiler.Backend
CTNatAgda.Syntax.Treeless, Agda.Compiler.Backend
ctparentAgda.Auto.NarrowingSearch
ctpriometaAgda.Auto.NarrowingSearch
CTQNameAgda.Syntax.Treeless, Agda.Compiler.Backend
CTransAgda.TypeChecking.SizedTypes.Syntax
CTree 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
cTreelessAgda.Syntax.Treeless, Agda.Compiler.Backend
CTStringAgda.Syntax.Treeless, Agda.Compiler.Backend
ctsubAgda.Auto.NarrowingSearch
CtxAgda.Auto.Syntax
CTypeAgda.TypeChecking.Rules.Data
curDefsAgda.Compiler.Common
curHsModAgda.Compiler.MAlonzo.Misc
curIFAgda.Compiler.Common
curMNameAgda.Compiler.Common
curModuleAgda.Compiler.JS.Compiler
CurrentAccountAgda.Utils.Benchmark
currentAccountAgda.Utils.Benchmark
currentCxtAgda.TypeChecking.Names
CurrentInputAgda.Syntax.Parser.Alex
currentModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentOrFreshMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CurrentTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
curriedApplyAgda.Compiler.JS.Substitution
curriedLambdaAgda.Compiler.JS.Substitution
curryAtAgda.TypeChecking.Records
CurryingAgda.Utils.TypeLevel
currysAgda.Utils.TypeLevel
curSigAgda.Compiler.Common
CutOff 
1 (Type/Class)Agda.Termination.CutOff
2 (Data Constructor)Agda.Termination.CutOff
cxtSubstAgda.TypeChecking.Names
CyclicModuleDependencyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend