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

Index - C

CActionAgda.Auto.Syntax
calcAgda.Auto.NarrowingSearch
calcEqRStateAgda.Auto.Typecheck
CALConcatAgda.Auto.Syntax
Call 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Termination.CallGraph
3 (Data Constructor)Agda.Termination.CallGraph
callGHCAgda.Compiler.MAlonzo.Compiler
CallGraphAgda.Termination.CallGraph
callGraphInvariantAgda.Termination.CallGraph
CallInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInvariantAgda.Termination.CallGraph
CallMatrix 
1 (Type/Class)Agda.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
callMatrixInvariantAgda.Termination.CallGraph
callsAgda.Termination.Lexicographic
CALNilAgda.Auto.Syntax
canonicalNameAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
CantSplitAgda.TypeChecking.Coverage
Case 
1 (Type/Class)Agda.Compiler.JS.Case
2 (Data Constructor)Agda.Compiler.JS.Case
3 (Data Constructor)Agda.Compiler.Epic.AuxAST
4 (Data Constructor)Agda.TypeChecking.CompiledClause
5 (Type/Class)Agda.TypeChecking.CompiledClause
CaseContextAgda.Interaction.MakeCase
caseeAgda.Compiler.Epic.AuxAST
caseOptsAgda.Compiler.Epic.CaseOpts
caseOptsExprAgda.Compiler.Epic.CaseOpts
caseSplitSearchAgda.Auto.CaseSplit
caseSplitSearch'Agda.Auto.CaseSplit
catAgda.Utils.Pretty
catchAllAgda.TypeChecking.CompiledClause
catchAllBranchAgda.TypeChecking.CompiledClause
catchConstraintAgda.TypeChecking.Constraints
catchError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
catchExceptionAgda.TypeChecking.Monad.Exception
catchImpossibleAgda.Utils.Impossible
categorizedeclAgda.Auto.Syntax
catMaybesAgda.Utils.Maybe
cdcontAgda.Auto.Syntax
cddeffreevarsAgda.Auto.Syntax
cdeclAgda.Compiler.MAlonzo.Compiler
cdnameAgda.Auto.Syntax
cdoriginAgda.Auto.Syntax
cdtypeAgda.Auto.Syntax
CExpAgda.Auto.Syntax
chainlAgda.Utils.ReadP
chainl1Agda.Utils.ReadP
chainl1'Agda.Syntax.Concrete.Operators.Parser
chainrAgda.Utils.ReadP
chainr1Agda.Utils.ReadP
chainr1'Agda.Syntax.Concrete.Operators.Parser
CharAgda.Compiler.JS.Syntax
char 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Utils.ReadP
chattyAgda.Utils.QuickCheck
checkAllVarsAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
CheckArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkArgumentsAgda.TypeChecking.Rules.Term
checkArguments'Agda.TypeChecking.Rules.Term
checkArguments_Agda.TypeChecking.Rules.Term
checkAxiomAgda.TypeChecking.Rules.Decl
CheckClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkClauseAgda.TypeChecking.Rules.Def
CheckConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkConstructorAgda.TypeChecking.Rules.Data
checkConstructorApplicationAgda.TypeChecking.Rules.Term
checkConstructorTypeAgda.Compiler.MAlonzo.Compiler
checkCoverAgda.Compiler.MAlonzo.Compiler
checkCoverageAgda.TypeChecking.Coverage
CheckDataDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDataDefAgda.TypeChecking.Rules.Data
checkDeclAgda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
checkDeclsAgda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop
CheckDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDotPatternAgda.TypeChecking.Rules.LHS
checkeliminandAgda.Auto.Typecheck
checkEqualitiesAgda.TypeChecking.Rules.LHS.Unify
checkEqualityAgda.TypeChecking.Rules.LHS.Unify
checkEqualityHHAgda.TypeChecking.Rules.LHS.Unify
CheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkExprAgda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
checkForImportCycleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
CheckFunDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkFunDefAgda.TypeChecking.Rules.Def
checkFunDef'Agda.TypeChecking.Rules.Def
checkHeadApplicationAgda.TypeChecking.Rules.Term
checkImportAgda.TypeChecking.Rules.Decl
checkInjectivityAgda.TypeChecking.Injectivity
CheckIsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLambdaAgda.TypeChecking.Rules.Term
checkLeftHandSideAgda.TypeChecking.Rules.LHS
CheckLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLetBindingAgda.TypeChecking.Rules.Term
checkLetBindingsAgda.TypeChecking.Rules.Term
checkLiteralAgda.TypeChecking.Rules.Term
checkMetaAgda.TypeChecking.Rules.Term
checkModuleArityAgda.TypeChecking.Rules.Decl
checkModuleNameAgda.Interaction.FindFile
checkMutualAgda.TypeChecking.Rules.Decl
checkOptsAgda.Interaction.Options
CheckPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPatternShadowingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPragmaAgda.TypeChecking.Rules.Decl
CheckPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPrimitiveAgda.TypeChecking.Rules.Decl
CheckRecDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkRecDefAgda.TypeChecking.Rules.Record
checkRecordProjectionsAgda.TypeChecking.Rules.Record
checkSectionAgda.TypeChecking.Rules.Decl
CheckSectionApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkSectionApplicationAgda.TypeChecking.Rules.Decl
checkSectionApplication'Agda.TypeChecking.Rules.Decl
checkSizeIndexAgda.TypeChecking.Polarity
checkStrictlyPositiveAgda.TypeChecking.Positivity
checkTelescope_Agda.TypeChecking.Rules.Term
checkTermAgda.TypeChecking.Rules.Term
checkTypedBindingAgda.TypeChecking.Rules.Term
checkTypedBindingsAgda.TypeChecking.Rules.Term
checkTypedBindings_Agda.TypeChecking.Rules.Term
checkTypeOfMainAgda.Compiler.MAlonzo.Primitives
checkTypeSignatureAgda.TypeChecking.Rules.Decl
checkWhereAgda.TypeChecking.Rules.Def
checkWithFunctionAgda.TypeChecking.Rules.Def
CheckWithFunctionTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ChoiceAgda.Auto.NarrowingSearch
choice 
1 (Function)Agda.Utils.ReadP
2 (Function)Agda.TypeChecking.Coverage.Match
3 (Function)Agda.TypeChecking.Quote
choose 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.Auto.NarrowingSearch
choosePrioMetaAgda.Auto.NarrowingSearch
chopAgda.Utils.List
ChrAgda.Utils.Pretty
ClAgda.TypeChecking.CompiledClause.Compile
ClashingDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingFileNamesForAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
classifyAgda.Utils.QuickCheck
Clause 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Abstract
5 (Data Constructor)Agda.Syntax.Abstract
6 (Type/Class)Agda.Syntax.Concrete.Definitions
7 (Data Constructor)Agda.Syntax.Concrete.Definitions
clause 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
ClauseBodyAgda.Syntax.Internal
clauseBodyAgda.Syntax.Internal
clausebodyAgda.Compiler.MAlonzo.Compiler
clausePatsAgda.Syntax.Internal
clausePermAgda.Syntax.Internal
clauseRangeAgda.Syntax.Internal
clauseTelAgda.Syntax.Internal
clearMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
clEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Clos 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
closeBraceAgda.Syntax.Parser.Layout
ClosedLevelAgda.Syntax.Internal
closifyAgda.Auto.Syntax
Closure 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClsAgda.TypeChecking.CompiledClause.Compile
clScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cmAgda.Termination.CallGraph
cmd_autoAgda.Interaction.GhciTop
cmd_compileAgda.Interaction.GhciTop
cmd_computeAgda.Interaction.GhciTop
cmd_compute_toplevelAgda.Interaction.GhciTop
cmd_constraintsAgda.Interaction.GhciTop
cmd_contextAgda.Interaction.GhciTop
cmd_giveAgda.Interaction.GhciTop
cmd_goal_typeAgda.Interaction.GhciTop
cmd_goal_type_contextAgda.Interaction.GhciTop
cmd_goal_type_context_andAgda.Interaction.GhciTop
cmd_goal_type_context_inferAgda.Interaction.GhciTop
cmd_inferAgda.Interaction.GhciTop
cmd_infer_toplevelAgda.Interaction.GhciTop
cmd_introAgda.Interaction.GhciTop
cmd_loadAgda.Interaction.GhciTop
cmd_load'Agda.Interaction.GhciTop
cmd_make_caseAgda.Interaction.GhciTop
cmd_metasAgda.Interaction.GhciTop
cmd_refineAgda.Interaction.GhciTop
cmd_refine_or_introAgda.Interaction.GhciTop
cmd_show_module_contentsAgda.Interaction.GhciTop
cmd_show_module_contents_toplevelAgda.Interaction.GhciTop
cmd_solveAllAgda.Interaction.GhciTop
cmd_write_highlighting_infoAgda.Interaction.GhciTop
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
CmpElimAgda.Interaction.BasicOps
CmpEqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpInTypeAgda.Interaction.BasicOps
CmpLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpLevelsAgda.Interaction.BasicOps
CmpSortsAgda.Interaction.BasicOps
CmpTelesAgda.Interaction.BasicOps
CmpTypesAgda.Interaction.BasicOps
CMRigidAgda.Auto.Typecheck
cnvhAgda.Auto.Convert
CoArbitraryAgda.Utils.QuickCheck
coarbitraryAgda.Utils.QuickCheck
coarbitraryIntegralAgda.Utils.QuickCheck
coarbitraryRealAgda.Utils.QuickCheck
coarbitraryShowAgda.Utils.QuickCheck
CodataAgda.Syntax.Concrete.Definitions
codeAgda.Syntax.Parser.Lexer
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Rules.Builtin.Coinduction
2 (Data Constructor)Agda.TypeChecking.Rules.Builtin.Coinduction
coinductionKitAgda.TypeChecking.Rules.Builtin.Coinduction
CoInductiveAgda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Coverage
col 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
coldescrAgda.Utils.Warshall
collectAgda.Utils.QuickCheck
colonAgda.Utils.Pretty
cols 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Termination.Matrix
ColumnAgda.Termination.Lexicographic
columnsAgda.Termination.Lexicographic
comma 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
CommandAgda.Interaction.CommandLine.CommandLine
commandAgda.Interaction.GhciTop
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Comment 
1 (Type/Class)Agda.Compiler.Epic.AuxAST
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
commutativeAgda.Utils.TestHelpers
commuteMAgda.Utils.Monad
comp'Agda.Auto.Typecheck
compactPAgda.Utils.Permutation
compareArgsAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareElimsAgda.TypeChecking.Conversion
compareLevelAgda.TypeChecking.UniversePolymorphism
compareSizesAgda.TypeChecking.SizedTypes
compareSortAgda.TypeChecking.Conversion
compareTelAgda.TypeChecking.Conversion
compareTermAgda.TypeChecking.Conversion
compareTerm'Agda.TypeChecking.Conversion
compareTypeAgda.TypeChecking.Conversion
ComparisonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompilationErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompileAgda.Compiler.Epic.CompileState
compile 
1 (Function)Agda.TypeChecking.CompiledClause.Compile
2 (Function)Agda.Compiler.MAlonzo.Compiler
3 (Function)Agda.Compiler.JS.Compiler
compileClauses 
1 (Function)Agda.TypeChecking.CompiledClause.Compile
2 (Function)Agda.Compiler.Epic.FromAgda
CompiledClausesAgda.TypeChecking.CompiledClause
CompiledDataPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledEpicAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledEpicPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledHaskellAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
compileDir 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
compiledJSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledJSPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compiledModulesAgda.Compiler.Epic.CompileState
CompiledPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
CompiledRepAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledRepresentationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledTypePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compilerMain 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.Epic.Compiler
3 (Function)Agda.Compiler.JS.Compiler
CompileState 
1 (Type/Class)Agda.Compiler.Epic.CompileState
2 (Data Constructor)Agda.Compiler.Epic.CompileState
completeAgda.Termination.CallGraph
composePAgda.Utils.Permutation
composePolAgda.TypeChecking.Polarity
composeRelevanceAgda.TypeChecking.Irrelevance
compressAgda.Interaction.Highlighting.Precise
CompressedFileAgda.Interaction.Highlighting.Precise
computeEdgeAgda.TypeChecking.Positivity
computeNeighbourhoodAgda.TypeChecking.Coverage
ComputeOccurrencesAgda.TypeChecking.Positivity
computeOccurrencesAgda.TypeChecking.Positivity
computePolarityAgda.TypeChecking.Polarity
computeSizeConstraintAgda.TypeChecking.SizedTypes
Con 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
3 (Data Constructor)Agda.Syntax.Abstract
conAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConArgTypeAgda.TypeChecking.Positivity
conArityAgda.Compiler.Epic.Interface
conArityAndParsAgda.Compiler.MAlonzo.Compiler
conBranchesAgda.TypeChecking.CompiledClause
conCaseAgda.TypeChecking.CompiledClause
concatargsAgda.Auto.CaseSplit
concatMapMAgda.Utils.Monad
concatOccursAgda.TypeChecking.Positivity
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
condeclAgda.Compiler.MAlonzo.Compiler
ConElimAgda.TypeChecking.Eliminators
conFreqAgda.TypeChecking.Test.Generators
ConHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conhqnAgda.Compiler.MAlonzo.Misc
conIndAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conjoinAgda.Utils.QuickCheck
ConMPAgda.TypeChecking.Coverage.Match
ConName 
1 (Data Constructor)Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
2 (Type/Class)Agda.TypeChecking.Test.Generators
3 (Data Constructor)Agda.TypeChecking.Test.Generators
ConnectHandleAgda.Auto.NarrowingSearch
ConP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Abstract
conParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConsAgda.Interaction.EmacsCommand
conSrcConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Const 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
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
Constraint 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Utils.Warshall
constraintProblemAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Constraints 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Utils.Warshall
ConstRefAgda.Auto.Syntax
constrGroupAgda.Compiler.Epic.Injection
constrInScopeAgda.Compiler.Epic.CompileState
constrTagsAgda.Compiler.Epic.Interface
Constructor 
1 (Data Constructor)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Interaction.Highlighting.Precise
5 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructorArityAgda.Compiler.Epic.CompileState
constructorFormAgda.TypeChecking.Primitive
constructorImpossibleAgda.Auto.Typecheck
ConstructorMismatchAgda.TypeChecking.Rules.LHS.Unify
constructorMismatchAgda.TypeChecking.Rules.LHS.Unify
constructorMismatchHHAgda.TypeChecking.Rules.LHS.Unify
ConstructorNameAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
ConstructorPatternInWrongDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructPatsAgda.Auto.Convert
constructsAgda.TypeChecking.Rules.Data
ContAgda.Utils.Monad
containsAbsurdPatternAgda.TypeChecking.Rules.Def
contains_constructorAgda.Auto.Convert
ContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ContextEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
contextOfMetaAgda.Interaction.BasicOps
ContinueAgda.Interaction.CommandLine.CommandLine
continueAfterAgda.Interaction.CommandLine.CommandLine
ContinueInAgda.Interaction.CommandLine.CommandLine
continuousAgda.Syntax.Position, Agda.Interaction.GhciTop
continuousPerLineAgda.Syntax.Position, Agda.Interaction.GhciTop
ContravariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
convertLineEndingsAgda.Utils.Unicode
copyargAgda.Auto.Typecheck
copyScopeAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
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
costUnificationOccursAgda.Auto.SearchControl
countAgda.Utils.ReadP
CovariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cover 
1 (Function)Agda.Utils.QuickCheck
2 (Function)Agda.TypeChecking.Coverage
CoverageCantSplitIrrelevantTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitOnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageFailureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoveringAgda.TypeChecking.Coverage
CoverMAgda.TypeChecking.Coverage
createInterfaceAgda.Interaction.Imports
createMetaInfoAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
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
cthandlesAgda.Auto.NarrowingSearch
ctparentAgda.Auto.NarrowingSearch
ctpriometaAgda.Auto.NarrowingSearch
CTree 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
ctsubAgda.Auto.NarrowingSearch
Ctx 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CtxId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
curDefsAgda.Compiler.MAlonzo.Misc
curFunAgda.Compiler.Epic.CompileState
curHsModAgda.Compiler.MAlonzo.Misc
curIFAgda.Compiler.MAlonzo.Misc
curMNameAgda.Compiler.MAlonzo.Misc
curModule 
1 (Function)Agda.Compiler.Epic.CompileState
2 (Function)Agda.Compiler.JS.Compiler
CurrentDirAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
CurrentInputAgda.Syntax.Parser.Alex
currentModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
currentMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
currentProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
curriedApplyAgda.Compiler.JS.Substitution
curriedLambdaAgda.Compiler.JS.Substitution
curSigAgda.Compiler.MAlonzo.Misc
CyclicModuleDependencyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad