| CAction | Agda.Auto.Syntax |
| calc | Agda.Auto.NarrowingSearch |
| CALConcat | Agda.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 |
| callGHC | Agda.Compiler.MAlonzo.Compiler |
| CallGraph | Agda.Termination.CallGraph |
| callGraphInvariant | Agda.Termination.CallGraph |
| callInvariant | Agda.Termination.CallGraph |
| CallMatrix | |
| 1 (Type/Class) | Agda.Termination.CallGraph |
| 2 (Data Constructor) | Agda.Termination.CallGraph |
| callMatrixInvariant | Agda.Termination.CallGraph |
| calls | Agda.Termination.Lexicographic |
| CallTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CALNil | Agda.Auto.Syntax |
| canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| CantSplit | Agda.TypeChecking.Coverage |
| CArgList | Agda.Auto.Syntax |
| cat | Agda.Utils.Pretty |
| catchConstraint | Agda.TypeChecking.Constraints |
| catchException | Agda.TypeChecking.Monad.Exception |
| catchImpossible | Agda.Utils.Impossible |
| catMaybes | Agda.Utils.Maybe |
| cdcont | Agda.Auto.Syntax |
| cdecl | Agda.Compiler.MAlonzo.Compiler |
| cdname | Agda.Auto.Syntax |
| cdorigin | Agda.Auto.Syntax |
| cdtype | Agda.Auto.Syntax |
| CExp | Agda.Auto.Syntax |
| chainl | Agda.Utils.ReadP |
| chainl1 | Agda.Utils.ReadP |
| chainr | Agda.Utils.ReadP |
| chainr1 | Agda.Utils.ReadP |
| char | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Utils.ReadP |
| checkArgs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkArguments | Agda.TypeChecking.Rules.Term |
| checkArguments' | Agda.TypeChecking.Rules.Term |
| checkArguments_ | Agda.TypeChecking.Rules.Term |
| checkAxiom | Agda.TypeChecking.Rules.Decl |
| CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkClause | Agda.TypeChecking.Rules.Def |
| CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkConstructor | Agda.TypeChecking.Rules.Data |
| checkConstructorType | Agda.Compiler.MAlonzo.Compiler |
| checkCover | Agda.Compiler.MAlonzo.Compiler |
| checkCoverage | Agda.TypeChecking.Coverage |
| CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkDataDef | Agda.TypeChecking.Rules.Data |
| checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkDefinition | Agda.TypeChecking.Rules.Decl |
| CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkDotPattern | Agda.TypeChecking.Rules.LHS |
| checkEqualities | Agda.TypeChecking.Rules.LHS.Unify |
| CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkFunDef | Agda.TypeChecking.Rules.Def |
| checkHeadApplication | Agda.TypeChecking.Rules.Term |
| checkImport | Agda.TypeChecking.Rules.Decl |
| checkInjectivity | Agda.TypeChecking.Injectivity |
| checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
| CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkLetBinding | Agda.TypeChecking.Rules.Term |
| checkLetBindings | Agda.TypeChecking.Rules.Term |
| checkLiteral | Agda.TypeChecking.Rules.Term |
| checkModuleArity | Agda.TypeChecking.Rules.Decl |
| checkModuleName | Agda.Interaction.FindFile |
| checkMutual | Agda.TypeChecking.Rules.Decl |
| checkOpts | Agda.Interaction.Options |
| CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkPragma | Agda.TypeChecking.Rules.Decl |
| CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkPrimitive | Agda.TypeChecking.Rules.Decl |
| CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkRecDef | Agda.TypeChecking.Rules.Record |
| checkRecordProjections | Agda.TypeChecking.Rules.Record |
| checkSection | Agda.TypeChecking.Rules.Decl |
| CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkSectionApplication | Agda.TypeChecking.Rules.Decl |
| checkSizeIndex | Agda.TypeChecking.Polarity |
| checkStrictlyPositive | Agda.TypeChecking.Positivity |
| checkTelescope | Agda.TypeChecking.Rules.Term |
| checkTypedBinding | Agda.TypeChecking.Rules.Term |
| checkTypedBindings | Agda.TypeChecking.Rules.Term |
| checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
| checkTypeSignature | Agda.TypeChecking.Rules.Decl |
| checkWhere | Agda.TypeChecking.Rules.Def |
| checkWithFunction | Agda.TypeChecking.Rules.Def |
| Child | Agda.Utils.Trace |
| ChildCall | Agda.Utils.Trace |
| Choice | Agda.Auto.NarrowingSearch |
| choice | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.TypeChecking.Coverage.Match |
| choose | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.Auto.NarrowingSearch |
| choosePrioMeta | Agda.Auto.NarrowingSearch |
| chop | Agda.Utils.List |
| Chr | Agda.Utils.Pretty |
| ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| classify | Agda.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.Alonzo.PatternMonad |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| clauseBod | Agda.Compiler.Alonzo.Main |
| ClauseBody | Agda.Syntax.Internal |
| clauseBody | Agda.Syntax.Internal |
| clausebody | Agda.Compiler.MAlonzo.Compiler |
| clausePats | Agda.Syntax.Internal |
| clausePerm | Agda.Syntax.Internal |
| clauseRange | Agda.Syntax.Internal |
| clauseTel | Agda.Syntax.Internal |
| clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Clos | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| closeBrace | Agda.Syntax.Parser.Layout |
| ClosedLevel | Agda.TypeChecking.Level |
| closify | Agda.Auto.Typecheck |
| Closure | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clTrace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cm | Agda.Termination.CallGraph |
| cmd_auto | Agda.Interaction.GhciTop |
| cmd_compile | Agda.Interaction.GhciTop |
| cmd_compute | Agda.Interaction.GhciTop |
| cmd_compute_toplevel | Agda.Interaction.GhciTop |
| cmd_constraints | Agda.Interaction.GhciTop |
| cmd_context | Agda.Interaction.GhciTop |
| cmd_give | Agda.Interaction.GhciTop |
| cmd_goals | Agda.Interaction.GhciTop |
| cmd_goal_type | Agda.Interaction.GhciTop |
| cmd_goal_type_context | Agda.Interaction.GhciTop |
| cmd_goal_type_context_and | Agda.Interaction.GhciTop |
| cmd_goal_type_context_infer | Agda.Interaction.GhciTop |
| cmd_infer | Agda.Interaction.GhciTop |
| cmd_infer_toplevel | Agda.Interaction.GhciTop |
| cmd_intro | Agda.Interaction.GhciTop |
| cmd_load | Agda.Interaction.GhciTop |
| cmd_load' | Agda.Interaction.GhciTop |
| cmd_make_case | Agda.Interaction.GhciTop |
| cmd_metas | Agda.Interaction.GhciTop |
| cmd_refine | Agda.Interaction.GhciTop |
| cmd_refine_or_intro | Agda.Interaction.GhciTop |
| cmd_reset | Agda.Interaction.GhciTop |
| cmd_solveAll | Agda.Interaction.GhciTop |
| cmd_write_highlighting_info | Agda.Interaction.GhciTop |
| CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpInType | Agda.Interaction.BasicOps |
| CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpSorts | Agda.Interaction.BasicOps |
| CmpTeles | Agda.Interaction.BasicOps |
| CmpTypes | Agda.Interaction.BasicOps |
| cnt | Agda.Compiler.Alonzo.PatternMonad |
| cnvh | Agda.Auto.Convert |
| CoArbitrary | Agda.Utils.QuickCheck |
| coarbitrary | Agda.Utils.QuickCheck |
| coarbitraryIntegral | Agda.Utils.QuickCheck |
| coarbitraryReal | Agda.Utils.QuickCheck |
| coarbitraryShow | Agda.Utils.QuickCheck |
| code | Agda.Syntax.Parser.Lexer |
| CoInductive | Agda.Syntax.Common |
| col | Agda.Termination.Matrix |
| coldescr | Agda.Utils.Warshall |
| collect | Agda.Utils.QuickCheck |
| colon | Agda.Utils.Pretty |
| cols | Agda.Termination.Matrix |
| Column | Agda.Termination.Lexicographic |
| columns | Agda.Termination.Lexicographic |
| comma | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Command | Agda.Interaction.CommandLine.CommandLine |
| command | Agda.Interaction.GhciTop |
| CommandLineOptions | Agda.Interaction.Options |
| commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Comment | Agda.Interaction.Highlighting.Precise |
| commutative | Agda.Utils.TestHelpers |
| commuteM | Agda.Utils.Monad |
| comp | Agda.Auto.Typecheck |
| comp' | Agda.Auto.Typecheck |
| compactP | Agda.Utils.Permutation |
| compareArgs | Agda.TypeChecking.Conversion |
| compareAtom | Agda.TypeChecking.Conversion |
| compareSizes | Agda.TypeChecking.SizedTypes |
| compareSort | Agda.TypeChecking.Conversion |
| compareTel | Agda.TypeChecking.Conversion |
| compareTerm | Agda.TypeChecking.Conversion |
| compareType | Agda.TypeChecking.Conversion |
| compargs | Agda.Auto.Typecheck |
| Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| comphn' | Agda.Auto.Typecheck |
| CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| compile | Agda.Compiler.MAlonzo.Compiler |
| CompiledDataPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledTypePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compilerMain | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.Agate.Main |
| 3 (Function) | Agda.Compiler.Alonzo.Main |
| complete | Agda.Termination.CallGraph |
| composeP | Agda.Utils.Permutation |
| composePol | Agda.TypeChecking.Polarity |
| compress | Agda.Interaction.Highlighting.Precise |
| CompressedFile | Agda.Interaction.Highlighting.Precise |
| computeEdge | Agda.TypeChecking.Positivity |
| computeGreatestFixedPoint | Agda.Compiler.Agate.Classify |
| computeLeastFixedPoint | Agda.Compiler.Agate.Classify |
| computeMaxArity | Agda.Compiler.Agate.Main |
| computeNeighbourhood | Agda.TypeChecking.Coverage |
| ComputeOccurrences | Agda.TypeChecking.Positivity |
| computeOccurrences | Agda.TypeChecking.Positivity |
| computePolarity | Agda.TypeChecking.Polarity |
| computeSizeConstraint | Agda.TypeChecking.SizedTypes |
| Con | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConArgType | Agda.TypeChecking.Positivity |
| concatMapM | Agda.Utils.Monad |
| concatOccurs | Agda.TypeChecking.Positivity |
| ConcreteDef | Agda.Syntax.Common |
| ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| condecl | Agda.Compiler.MAlonzo.Compiler |
| conFreq | Agda.TypeChecking.Test.Generators |
| ConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conhqn | Agda.Compiler.MAlonzo.Misc |
| conHsCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConMP | Agda.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 |
| conName | Agda.Compiler.Alonzo.Names |
| ConP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConPos | Agda.TypeChecking.With |
| conQName | Agda.Compiler.Alonzo.Names |
| conQStr | Agda.Compiler.Alonzo.Names |
| consDefs | Agda.Compiler.Alonzo.Main |
| consForName | Agda.Compiler.Alonzo.Main |
| conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Const | Agda.Auto.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 |
| conStr | Agda.Compiler.Alonzo.Names |
| Constraint | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.Utils.Warshall |
| ConstraintClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Constraints | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.Utils.Warshall |
| ConstRef | Agda.Auto.Syntax |
| 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 |
| constructorArity | Agda.Compiler.MAlonzo.Compiler |
| constructorForm | Agda.TypeChecking.Primitive |
| ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| ConstructorName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| constructorsInClause | Agda.TypeChecking.With |
| constructorsInClauses | Agda.TypeChecking.With |
| constructs | Agda.TypeChecking.Rules.Data |
| Cont | Agda.Utils.Monad |
| containsAbsurdPattern | Agda.TypeChecking.Rules.Def |
| contClause | Agda.Compiler.Alonzo.Main |
| Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| contextOfMeta | Agda.Interaction.BasicOps |
| Continue | Agda.Interaction.CommandLine.CommandLine |
| continueAfter | Agda.Interaction.CommandLine.CommandLine |
| ContinueIn | Agda.Interaction.CommandLine.CommandLine |
| continuous | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| continuousPerLine | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| convertLineEndings | Agda.Utils.Unicode |
| copyScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| count | Agda.Utils.ReadP |
| Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cover | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.TypeChecking.Coverage |
| CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Covering | Agda.TypeChecking.Coverage |
| CoverM | Agda.TypeChecking.Coverage |
| createInterface | Agda.Interaction.Imports |
| createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| createModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| ctparent | Agda.Auto.NarrowingSearch |
| ctpriometa | Agda.Auto.NarrowingSearch |
| CTree | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| ctsub | Agda.Auto.NarrowingSearch |
| Ctx | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ctxEntry | Agda.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 |
| ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| curDefs | Agda.Compiler.MAlonzo.Misc |
| curHsMod | Agda.Compiler.MAlonzo.Misc |
| curIF | Agda.Compiler.MAlonzo.Misc |
| curMName | Agda.Compiler.MAlonzo.Misc |
| Current | Agda.Utils.Trace |
| CurrentCall | Agda.Utils.Trace |
| CurrentDir | Agda.Interaction.Imports |
| CurrentInput | Agda.Syntax.Parser.Alex |
| currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| currentMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| curSig | Agda.Compiler.MAlonzo.Misc |
| CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |