Agda-2.6.0: 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
caseListNeAgda.Utils.NonemptyList
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
catchConstraintAgda.TypeChecking.Constraints
catchErrorAgda.Utils.Except
catchError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchIlltypedPatternBlockedOnMetaAgda.TypeChecking.Rules.Term
catchImpossibleAgda.Utils.Impossible
CatchIOAgda.Utils.IO
catchIOAgda.Utils.IO
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
chainlAgda.Utils.Parser.ReadP
chainl1Agda.Utils.Parser.ReadP
chainrAgda.Utils.Parser.ReadP
chainr1Agda.Utils.Parser.ReadP
ChangeAgda.Utils.Update
Char 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
char 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Utils.Parser.ReadP
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
checkCoinductiveRecordsAgda.TypeChecking.Rules.Decl
checkCompilerPragmasAgda.Compiler.JS.Compiler
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
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.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
CheckLHSAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkLinearityAgda.TypeChecking.MetaVars
checkLiteralAgda.TypeChecking.Rules.Term
checkMacroTypeAgda.TypeChecking.Rules.Def
checkMetaAgda.TypeChecking.Rules.Term
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
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
CheckPatternShadowingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
checkSortAgda.TypeChecking.CheckInternal
checkSortOfSplitVarAgda.TypeChecking.Rules.LHS
checkStrictlyPositiveAgda.TypeChecking.Positivity
checkSyntacticEqualityAgda.TypeChecking.SyntacticEquality
checkSystemCoverageAgda.TypeChecking.Rules.Def
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
choice 
1 (Function)Agda.Utils.Parser.ReadP
2 (Function)Agda.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
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.Reflected
3 (Data Constructor)Agda.Syntax.Reflected
4 (Type/Class)Agda.Syntax.Internal
5 (Data Constructor)Agda.Syntax.Internal
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
clauseFullRangeAgda.Syntax.Internal
clauseLHSAgda.Syntax.Abstract
clauseLHSRangeAgda.Syntax.Internal
clausePatsAgda.Syntax.Internal
clausePermAgda.Syntax.Internal.Pattern
clauseRHSAgda.Syntax.Abstract
ClausesPostChecksAgda.TypeChecking.Rules.Def
clauseStrippedPatsAgda.Syntax.Abstract
clauseTelAgda.Syntax.Internal
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
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
Cmd_abortAgda.Interaction.InteractionTop
Cmd_autoAllAgda.Interaction.InteractionTop
Cmd_autoOneAgda.Interaction.InteractionTop
Cmd_compileAgda.Interaction.InteractionTop
Cmd_computeAgda.Interaction.InteractionTop
Cmd_compute_toplevelAgda.Interaction.InteractionTop
Cmd_constraintsAgda.Interaction.InteractionTop
Cmd_contextAgda.Interaction.InteractionTop
Cmd_elaborate_giveAgda.Interaction.InteractionTop
Cmd_giveAgda.Interaction.InteractionTop
Cmd_goal_typeAgda.Interaction.InteractionTop
Cmd_goal_type_contextAgda.Interaction.InteractionTop
cmd_goal_type_context_andAgda.Interaction.InteractionTop
Cmd_goal_type_context_checkAgda.Interaction.InteractionTop
Cmd_goal_type_context_inferAgda.Interaction.InteractionTop
Cmd_helper_functionAgda.Interaction.InteractionTop
cmd_helper_functionAgda.Interaction.InteractionTop
Cmd_highlightAgda.Interaction.InteractionTop
Cmd_inferAgda.Interaction.InteractionTop
Cmd_infer_toplevelAgda.Interaction.InteractionTop
Cmd_introAgda.Interaction.InteractionTop
Cmd_loadAgda.Interaction.InteractionTop
cmd_load'Agda.Interaction.InteractionTop
Cmd_load_highlighting_infoAgda.Interaction.InteractionTop
Cmd_make_caseAgda.Interaction.InteractionTop
Cmd_metasAgda.Interaction.InteractionTop
Cmd_refineAgda.Interaction.InteractionTop
Cmd_refine_or_introAgda.Interaction.InteractionTop
Cmd_search_about_toplevelAgda.Interaction.InteractionTop
Cmd_show_module_contentsAgda.Interaction.InteractionTop
Cmd_show_module_contents_toplevelAgda.Interaction.InteractionTop
Cmd_show_versionAgda.Interaction.InteractionTop
Cmd_solveAllAgda.Interaction.InteractionTop
Cmd_solveOneAgda.Interaction.InteractionTop
Cmd_tokenHighlightingAgda.Interaction.InteractionTop
Cmd_why_in_scopeAgda.Interaction.InteractionTop
Cmd_why_in_scope_toplevelAgda.Interaction.InteractionTop
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.BasicOps
CmpEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpInTypeAgda.Interaction.BasicOps
CmpLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpLevelsAgda.Interaction.BasicOps
CmpSortsAgda.Interaction.BasicOps
CmpTelesAgda.Interaction.BasicOps
CmpTypesAgda.Interaction.BasicOps
CMRigidAgda.Auto.Typecheck
CMSet 
1 (Type/Class)Agda.Termination.CallMatrix
2 (Data Constructor)Agda.Termination.CallMatrix
cmSetAgda.Termination.CallMatrix
CodataAgda.Syntax.Concrete.Definitions
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
coerceSizeAgda.TypeChecking.Conversion
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Monad.Builtin
2 (Data Constructor)Agda.TypeChecking.Monad.Builtin
coinductionKitAgda.TypeChecking.Monad.Builtin
coinductionKit'Agda.TypeChecking.Monad.Builtin
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.CommandLine
2 (Type/Class)Agda.Interaction.InteractionTop
3 (Data Constructor)Agda.Interaction.InteractionTop
Command'Agda.Interaction.InteractionTop
commandLineFlagsAgda.Compiler.Backend
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CommandMAgda.Interaction.InteractionTop
commandMToIOAgda.Interaction.InteractionTop
CommandQueue 
1 (Type/Class)Agda.Interaction.InteractionTop
2 (Data Constructor)Agda.Interaction.InteractionTop
commandQueueAgda.Interaction.InteractionTop
commandsAgda.Interaction.InteractionTop
CommandState 
1 (Type/Class)Agda.Interaction.InteractionTop
2 (Data Constructor)Agda.Interaction.InteractionTop
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
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
compareAtomAgda.TypeChecking.Conversion
compareAtomDirAgda.TypeChecking.Conversion
compareBelowMaxAgda.TypeChecking.SizedTypes
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
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
compareTermDirAgda.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
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.InteractionTop
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
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
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.BasicOps
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.Reflected
3 (Data Constructor)Agda.Syntax.Internal
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
conArityAndParsAgda.Compiler.Common
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
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
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.Reflected
2 (Data Constructor)Agda.Syntax.Internal
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
ConPatLazy 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
ConPatternInfo 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
conPFallThroughAgda.Syntax.Internal
conPLazyAgda.Syntax.Internal
conPRecordAgda.Syntax.Internal
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
consNeAgda.Utils.NonemptyList
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
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
2 (Function)Agda.TypeChecking.Reduce.Monad
constructorForm'Agda.TypeChecking.Monad.Builtin
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
contextOfMetaAgda.Interaction.BasicOps
contextSizeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContinueAgda.Interaction.CommandLine
continueAfterAgda.Interaction.CommandLine
ContinueInAgda.Interaction.CommandLine
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
count 
1 (Function)Agda.Utils.Bag
2 (Function)Agda.Utils.Parser.ReadP
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.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
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