| CAction | Agda.Auto.Syntax |
| calc | Agda.Auto.NarrowingSearch |
| calcEqRState | Agda.Auto.Typecheck |
| CALConcat | Agda.Auto.Syntax |
| Call | |
| 1 (Type/Class) | Agda.Termination.CallGraph |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CallComb | Agda.Termination.CallMatrix |
| callCompiler | Agda.Compiler.CallCompiler |
| callCompiler' | Agda.Compiler.CallCompiler |
| callGHC | Agda.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 |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| callInfoCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| callInfoRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| callInfos | Agda.Termination.Monad |
| callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CallMatrix | |
| 1 (Type/Class) | Agda.Termination.CallMatrix |
| 2 (Data Constructor) | Agda.Termination.CallMatrix |
| callMatrix | Agda.Termination.CallMatrix |
| CallMatrix' | Agda.Termination.CallMatrix |
| CallMatrixAug | |
| 1 (Type/Class) | Agda.Termination.CallMatrix |
| 2 (Data Constructor) | Agda.Termination.CallMatrix |
| callMatrixSet | Agda.Termination.CallGraph |
| CallPath | |
| 1 (Type/Class) | Agda.Termination.Monad |
| 2 (Data Constructor) | Agda.Termination.Monad |
| CALNil | Agda.Auto.Syntax |
| Candidates | Agda.TypeChecking.InstanceArguments |
| CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| canonicalizeSizeConstraint | |
| 1 (Function) | Agda.TypeChecking.SizedTypes |
| 2 (Function) | Agda.TypeChecking.SizedTypes.Solve |
| canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| canProject | Agda.TypeChecking.Substitute |
| CantInvert | Agda.TypeChecking.MetaVars |
| CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CantSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| CaseContext | Agda.Interaction.MakeCase |
| casee | Agda.Compiler.Epic.AuxAST |
| caseEitherM | Agda.Utils.Either |
| caseMaybe | |
| 1 (Function) | Agda.Utils.Maybe.Strict |
| 2 (Function) | Agda.Utils.Maybe |
| caseMaybeM | |
| 1 (Function) | Agda.Utils.Maybe.Strict |
| 2 (Function) | Agda.Utils.Maybe |
| caseOpts | Agda.Compiler.Epic.CaseOpts |
| caseOptsExpr | Agda.Compiler.Epic.CaseOpts |
| caseSplitSearch | Agda.Auto.CaseSplit |
| caseSplitSearch' | Agda.Auto.CaseSplit |
| cat | Agda.Utils.Pretty |
| catchAll | Agda.TypeChecking.CompiledClause |
| catchAllBranch | Agda.TypeChecking.CompiledClause |
| catchConstraint | Agda.TypeChecking.Constraints |
| catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| catchException | Agda.TypeChecking.Monad.Exception |
| catchImpossible | Agda.Utils.Impossible |
| categorizedecl | Agda.Auto.Syntax |
| catMaybes | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| cdcont | Agda.Auto.Syntax |
| cddeffreevars | 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 |
| Change | Agda.Utils.Update |
| Char | Agda.Compiler.JS.Syntax |
| char | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Utils.ReadP |
| chatty | Agda.Utils.QuickCheck |
| checkAbsurdLambda | Agda.TypeChecking.Rules.Term |
| checkAlias | Agda.TypeChecking.Rules.Def |
| checkApplication | Agda.TypeChecking.Rules.Term |
| CheckArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| checkCandidates | Agda.TypeChecking.InstanceArguments |
| CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkClause | Agda.TypeChecking.Rules.Def |
| checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl |
| CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkConstructor | Agda.TypeChecking.Rules.Data |
| checkConstructorApplication | Agda.TypeChecking.Rules.Term |
| 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 |
| checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker |
| checkDontExpandLast | Agda.TypeChecking.Rules.Term |
| CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkDotPattern | Agda.TypeChecking.Rules.LHS |
| checkeliminand | Agda.Auto.Typecheck |
| checkEqualities | Agda.TypeChecking.Rules.LHS.Unify |
| checkEquality | Agda.TypeChecking.Rules.LHS.Unify |
| checkEqualityHH | Agda.TypeChecking.Rules.LHS.Unify |
| CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker |
| CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkExtendedLambda | Agda.TypeChecking.Rules.Term |
| checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkFunDef | Agda.TypeChecking.Rules.Def |
| checkFunDef' | Agda.TypeChecking.Rules.Def |
| checkHeadApplication | Agda.TypeChecking.Rules.Term |
| checkImport | Agda.TypeChecking.Rules.Decl |
| checkInjectivity | Agda.TypeChecking.Injectivity |
| checkInjectivity_ | Agda.TypeChecking.Rules.Decl |
| checkInternal | Agda.TypeChecking.CheckInternal |
| CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkLambda | Agda.TypeChecking.Rules.Term |
| checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
| CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkLetBinding | Agda.TypeChecking.Rules.Term |
| checkLetBindings | Agda.TypeChecking.Rules.Term |
| checkLinearity | Agda.TypeChecking.MetaVars |
| checkLiteral | Agda.TypeChecking.Rules.Term |
| checkMeta | Agda.TypeChecking.Rules.Term |
| checkModuleArity | Agda.TypeChecking.Rules.Decl |
| checkModuleName | Agda.Interaction.FindFile |
| checkMutual | Agda.TypeChecking.Rules.Decl |
| checkOpts | Agda.Interaction.Options |
| checkOrInferMeta | Agda.TypeChecking.Rules.Term |
| checkParsIfUnambiguous | Agda.TypeChecking.Rules.LHS.Split |
| CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkPositivity_ | Agda.TypeChecking.Rules.Decl |
| 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 |
| checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl |
| CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkRecDef | Agda.TypeChecking.Rules.Record |
| checkRecordExpression | Agda.TypeChecking.Rules.Term |
| checkRecordProjections | Agda.TypeChecking.Rules.Record |
| checkRecordUpdate | Agda.TypeChecking.Rules.Term |
| checkSection | Agda.TypeChecking.Rules.Decl |
| CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkSectionApplication | Agda.TypeChecking.Rules.Decl |
| checkSectionApplication' | Agda.TypeChecking.Rules.Decl |
| checkSizeIndex | Agda.TypeChecking.Polarity |
| checkStrictlyPositive | Agda.TypeChecking.Positivity |
| checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality |
| checkTelescope_ | Agda.TypeChecking.Rules.Term |
| checkTerm | Agda.TypeChecking.Rules.Term |
| checkTermination_ | Agda.TypeChecking.Rules.Decl |
| checkType | Agda.TypeChecking.CheckInternal |
| checkTypeCheckingProblem | Agda.TypeChecking.Constraints |
| checkTypedBinding | Agda.TypeChecking.Rules.Term |
| checkTypedBindings | 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 |
| CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Choice | Agda.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 |
| choosePrioMeta | Agda.Auto.NarrowingSearch |
| chop | Agda.Utils.List |
| Chr | Agda.Utils.Pretty |
| Cl | Agda.TypeChecking.CompiledClause.Compile |
| 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.Abstract |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Type/Class) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Internal |
| 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 |
| Clause' | Agda.Syntax.Abstract |
| clauseArgs | Agda.Syntax.Internal.Pattern |
| ClauseBody | Agda.Syntax.Internal |
| clauseBody | Agda.Syntax.Internal |
| clausebody | Agda.Compiler.MAlonzo.Compiler |
| ClauseBodyF | Agda.Syntax.Internal |
| clauseElims | Agda.Syntax.Internal.Pattern |
| clauseLHS | Agda.Syntax.Abstract |
| clausePats | Agda.Syntax.Internal |
| clausePerm | Agda.Syntax.Internal |
| clauseRange | Agda.Syntax.Internal |
| clauseRHS | Agda.Syntax.Abstract |
| clauseTel | Agda.Syntax.Internal |
| clauseToSplitClause | Agda.TypeChecking.Coverage |
| clauseType | Agda.Syntax.Internal |
| clauseWhereDecls | Agda.Syntax.Abstract |
| clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| clearRunningInfo | Agda.Interaction.EmacsCommand |
| clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClockTime | Agda.Utils.Time |
| Clos | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| closeBrace | Agda.Syntax.Parser.Layout |
| ClosedLevel | Agda.Syntax.Internal |
| closify | Agda.Auto.Syntax |
| Closure | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Cls | Agda.TypeChecking.CompiledClause.Compile |
| clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cluster | Agda.Utils.Cluster |
| cluster' | Agda.Utils.Cluster |
| clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Cmd_auto | Agda.Interaction.InteractionTop |
| Cmd_compile | Agda.Interaction.InteractionTop |
| Cmd_compute | Agda.Interaction.InteractionTop |
| Cmd_compute_toplevel | Agda.Interaction.InteractionTop |
| Cmd_constraints | Agda.Interaction.InteractionTop |
| Cmd_context | Agda.Interaction.InteractionTop |
| Cmd_give | Agda.Interaction.InteractionTop |
| Cmd_goal_type | Agda.Interaction.InteractionTop |
| Cmd_goal_type_context | Agda.Interaction.InteractionTop |
| cmd_goal_type_context_and | Agda.Interaction.InteractionTop |
| Cmd_goal_type_context_infer | Agda.Interaction.InteractionTop |
| Cmd_helper_function | Agda.Interaction.InteractionTop |
| cmd_helper_function | Agda.Interaction.InteractionTop |
| Cmd_highlight | Agda.Interaction.InteractionTop |
| Cmd_infer | Agda.Interaction.InteractionTop |
| Cmd_infer_toplevel | Agda.Interaction.InteractionTop |
| Cmd_intro | Agda.Interaction.InteractionTop |
| Cmd_load | Agda.Interaction.InteractionTop |
| cmd_load' | Agda.Interaction.InteractionTop |
| Cmd_load_highlighting_info | Agda.Interaction.InteractionTop |
| Cmd_make_case | Agda.Interaction.InteractionTop |
| Cmd_metas | Agda.Interaction.InteractionTop |
| Cmd_refine | Agda.Interaction.InteractionTop |
| Cmd_refine_or_intro | Agda.Interaction.InteractionTop |
| Cmd_show_module_contents | Agda.Interaction.InteractionTop |
| Cmd_show_module_contents_toplevel | Agda.Interaction.InteractionTop |
| Cmd_solveAll | Agda.Interaction.InteractionTop |
| Cmd_why_in_scope | Agda.Interaction.InteractionTop |
| Cmd_why_in_scope_toplevel | Agda.Interaction.InteractionTop |
| CMFBlocked | Agda.Auto.Typecheck |
| CMFFlex | Agda.Auto.Typecheck |
| CMFlex | |
| 1 (Type/Class) | Agda.Auto.Typecheck |
| 2 (Data Constructor) | Agda.Auto.Typecheck |
| CMFSemi | Agda.Auto.Typecheck |
| CMode | Agda.Auto.Typecheck |
| Cmp | Agda.TypeChecking.SizedTypes.Syntax |
| cmp | Agda.TypeChecking.SizedTypes.Syntax |
| CmpElim | Agda.Interaction.BasicOps |
| CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpInType | Agda.Interaction.BasicOps |
| CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpLevels | Agda.Interaction.BasicOps |
| CmpSorts | Agda.Interaction.BasicOps |
| CmpTeles | Agda.Interaction.BasicOps |
| CmpTypes | Agda.Interaction.BasicOps |
| CMRigid | Agda.Auto.Typecheck |
| CMSet | |
| 1 (Type/Class) | Agda.Termination.CallMatrix |
| 2 (Data Constructor) | Agda.Termination.CallMatrix |
| cmSet | Agda.Termination.CallMatrix |
| CName | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
| cnvh | Agda.Auto.Convert |
| CoArbitrary | Agda.Utils.QuickCheck |
| coarbitrary | Agda.Utils.QuickCheck |
| coarbitraryEnum | Agda.Utils.QuickCheck |
| coarbitraryIntegral | Agda.Utils.QuickCheck |
| coarbitraryReal | Agda.Utils.QuickCheck |
| coarbitraryShow | Agda.Utils.QuickCheck |
| Codata | Agda.Syntax.Concrete.Definitions |
| code | Agda.Syntax.Parser.Lexer |
| coerce | Agda.TypeChecking.Conversion |
| coerceSize | Agda.TypeChecking.Conversion |
| CoinductionKit | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Builtin |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin |
| coinductionKit | Agda.TypeChecking.Monad.Builtin |
| CoInductive | Agda.Syntax.Common |
| CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| col | Agda.Termination.SparseMatrix |
| coldescr | Agda.Utils.Warshall |
| collapseO | Agda.Termination.Order |
| collect | Agda.Utils.QuickCheck |
| colOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| colon | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Color | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.Syntax.Internal |
| ColoredTypedBinding | Agda.Syntax.Concrete |
| ColorMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cols | Agda.Termination.SparseMatrix |
| combineHashes | Agda.Utils.Hash |
| comma | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Command | Agda.Interaction.CommandLine.CommandLine |
| CommandLineOptions | Agda.Interaction.Options |
| commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| CommandM | Agda.Interaction.InteractionTop |
| commandMToIO | Agda.Interaction.InteractionTop |
| CommandState | |
| 1 (Type/Class) | Agda.Interaction.InteractionTop |
| 2 (Data Constructor) | Agda.Interaction.InteractionTop |
| Comment | |
| 1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| commutative | Agda.Utils.TestHelpers |
| comp' | Agda.Auto.Typecheck |
| compactP | Agda.Utils.Permutation |
| Comparable | Agda.Utils.PartialOrd |
| comparable | Agda.Utils.PartialOrd |
| comparableOrd | Agda.Utils.PartialOrd |
| Compare | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| compareArgs | Agda.TypeChecking.Conversion |
| compareAtom | Agda.TypeChecking.Conversion |
| compareAtomDir | Agda.TypeChecking.Conversion |
| compareBelowMax | Agda.TypeChecking.SizedTypes |
| CompareDirection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| compareElims | Agda.TypeChecking.Conversion |
| compareFavorites | Agda.Utils.Favorites |
| compareIrrelevant | Agda.TypeChecking.Conversion |
| compareLevel | Agda.TypeChecking.Conversion |
| compareMaxViews | Agda.TypeChecking.SizedTypes |
| compareOffset | Agda.TypeChecking.SizedTypes.Syntax |
| compareRelevance | Agda.TypeChecking.Conversion |
| CompareResult | Agda.Utils.Favorites |
| compareSizes | Agda.TypeChecking.SizedTypes |
| compareSizeViews | Agda.TypeChecking.SizedTypes |
| compareSort | Agda.TypeChecking.Conversion |
| compareTel | Agda.TypeChecking.Conversion |
| compareTerm | Agda.TypeChecking.Conversion |
| compareTerm' | Agda.TypeChecking.Conversion |
| compareTermDir | Agda.TypeChecking.Conversion |
| compareType | Agda.TypeChecking.Conversion |
| compareWithFavorites | Agda.Utils.Favorites |
| compareWithPol | Agda.TypeChecking.Conversion |
| Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Compile | Agda.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 |
| CompiledClauses | Agda.TypeChecking.CompiledClause |
| CompiledDataPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compiledEpic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CompiledEpicPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledExportPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compiledHaskell | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| compileDir | |
| 1 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| compiledJS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CompiledJSPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compiledModules | Agda.Compiler.Epic.CompileState |
| CompiledPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CompiledRepresentation | Agda.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 |
| compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile |
| complete | Agda.Termination.CallGraph |
| completionStep | Agda.Termination.CallGraph |
| compose | Agda.TypeChecking.SizedTypes.Utils |
| composeP | Agda.Utils.Permutation |
| composePol | Agda.TypeChecking.Polarity |
| composeRelevance | Agda.TypeChecking.Irrelevance |
| composeS | Agda.TypeChecking.Substitute |
| composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| compress | Agda.Interaction.Highlighting.Precise |
| CompressedFile | |
| 1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| compressedFileInvariant | Agda.Interaction.Highlighting.Precise |
| compressPointerChain | Agda.Syntax.Internal |
| computeEdge | Agda.TypeChecking.Positivity |
| computeNeighbourhood | Agda.TypeChecking.Coverage |
| computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| ComputeOccurrences | Agda.TypeChecking.Positivity |
| computeOccurrences | Agda.TypeChecking.Positivity |
| computePolarity | Agda.TypeChecking.Polarity |
| computeSizeConstraint | |
| 1 (Function) | Agda.TypeChecking.SizedTypes |
| 2 (Function) | Agda.TypeChecking.SizedTypes.Solve |
| computeSizeConstraints | Agda.TypeChecking.SizedTypes |
| computeUnsolvedConstraints | Agda.Interaction.Highlighting.Generate |
| computeUnsolvedMetaWarnings | Agda.Interaction.Highlighting.Generate |
| Con | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conApp | Agda.TypeChecking.Substitute |
| ConArgType | Agda.TypeChecking.Positivity |
| conArity | Agda.Compiler.Epic.Interface |
| conArityAndPars | Agda.Compiler.MAlonzo.Compiler |
| conBranches | Agda.TypeChecking.CompiledClause |
| conCase | Agda.TypeChecking.CompiledClause |
| concatargs | Agda.Auto.CaseSplit |
| concatOccurs | Agda.TypeChecking.Positivity |
| ConcreteDef | Agda.Syntax.Common |
| ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
| concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract |
| conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConDBP | Agda.Termination.Monad |
| condecl | Agda.Compiler.MAlonzo.Compiler |
| Condition | Agda.TypeChecking.MetaVars |
| conFields | Agda.Syntax.Internal |
| conFreq | Agda.TypeChecking.Test.Generators |
| ConGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ConGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ConHead | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| conhqn | Agda.Compiler.MAlonzo.Misc |
| conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conjoin | Agda.Utils.QuickCheck |
| ConMP | Agda.TypeChecking.Coverage.Match |
| ConName | |
| 1 (Data Constructor) | Agda.Syntax.Scope.Base |
| 2 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| conName | Agda.Syntax.Internal |
| ConnectHandle | Agda.Auto.NarrowingSearch |
| connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| ConP | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConPatInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| ConPatternInfo | Agda.Syntax.Internal |
| Cons | Agda.Interaction.EmacsCommand |
| ConsHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Const | |
| 1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 3 (Data Constructor) | 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 |
| 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 |
| Constraint' | Agda.TypeChecking.SizedTypes.Syntax |
| constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
| constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| constraintProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Constraints | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConstRef | Agda.Auto.Syntax |
| constrGroup | Agda.Compiler.Epic.Injection |
| constrInScope | Agda.Compiler.Epic.CompileState |
| constrTags | Agda.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 |
| constructorArity | Agda.Compiler.Epic.CompileState |
| constructorForm | |
| 1 (Function) | Agda.TypeChecking.Monad.Builtin |
| 2 (Function) | Agda.TypeChecking.Reduce.Monad |
| constructorForm' | Agda.TypeChecking.Monad.Builtin |
| constructorImpossible | Agda.Auto.Typecheck |
| ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| constructorMismatchHH | Agda.TypeChecking.Rules.LHS.Unify |
| ConstructorName | Agda.Syntax.Scope.Monad |
| ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| constructPats | Agda.Auto.Convert |
| constructs | Agda.TypeChecking.Rules.Data |
| Cont | Agda.Utils.Monad |
| containsAbsurdPattern | Agda.TypeChecking.Rules.Def |
| contains_constructor | Agda.Auto.Convert |
| content | Agda.TypeChecking.CompiledClause |
| 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 |
| continuousPerLine | Agda.Syntax.Position |
| Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conUseSizeLt | Agda.Termination.Monad |
| ConvColor | Agda.TypeChecking.Rules.Term |
| convColor | Agda.TypeChecking.Rules.Term |
| convError | Agda.TypeChecking.Conversion |
| convertLineEndings | Agda.Utils.Unicode |
| copatternsNotImplemented | Agda.Auto.Convert |
| copyarg | Agda.Auto.Typecheck |
| copyScope | Agda.Syntax.Scope.Monad |
| copyTerm | Agda.Syntax.Internal.Generic |
| costAbsurdLam | Agda.Auto.SearchControl |
| costAddVarDepth | Agda.Auto.CaseSplit |
| costAppConstructor | Agda.Auto.SearchControl |
| costAppConstructorSingle | Agda.Auto.SearchControl |
| costAppExtraRef | Agda.Auto.SearchControl |
| costAppHint | Agda.Auto.SearchControl |
| costAppHintUsed | Agda.Auto.SearchControl |
| costAppRecCall | Agda.Auto.SearchControl |
| costAppRecCallUsed | Agda.Auto.SearchControl |
| costAppVar | Agda.Auto.SearchControl |
| costAppVarUsed | Agda.Auto.SearchControl |
| costCaseSplitHigh | Agda.Auto.CaseSplit |
| costCaseSplitLow | Agda.Auto.CaseSplit |
| costCaseSplitVeryHigh | Agda.Auto.CaseSplit |
| costEqCong | Agda.Auto.SearchControl |
| costEqEnd | Agda.Auto.SearchControl |
| costEqStep | Agda.Auto.SearchControl |
| costEqSym | Agda.Auto.SearchControl |
| costIncrease | Agda.Auto.SearchControl |
| costInferredTypeUnkown | Agda.Auto.SearchControl |
| costIotaStep | Agda.Auto.SearchControl |
| costLam | Agda.Auto.SearchControl |
| costLamUnfold | Agda.Auto.SearchControl |
| costPi | Agda.Auto.SearchControl |
| costSort | Agda.Auto.SearchControl |
| costUnification | Agda.Auto.SearchControl |
| costUnificationOccurs | Agda.Auto.SearchControl |
| count | Agda.Utils.ReadP |
| counterexample | Agda.Utils.QuickCheck |
| Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cover | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.TypeChecking.Coverage |
| Coverage | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| CoverageCantSplitIrrelevantType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| coverageCheck | Agda.TypeChecking.Coverage |
| CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Covering | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage |
| CoverM | Agda.TypeChecking.Coverage |
| covSplitArg | Agda.TypeChecking.Coverage |
| covSplitClauses | Agda.TypeChecking.Coverage |
| CPUTime | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| createInterface | Agda.Interaction.Imports |
| createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| createModule | Agda.Syntax.Scope.Monad |
| CSAbsurd | Agda.Auto.CaseSplit |
| CSCtx | Agda.Auto.CaseSplit |
| CSOmittedArg | Agda.Auto.CaseSplit |
| CSPat | Agda.Auto.CaseSplit |
| CSPatConApp | Agda.Auto.CaseSplit |
| CSPatExp | Agda.Auto.CaseSplit |
| CSPatI | Agda.Auto.CaseSplit |
| CSPatVar | Agda.Auto.CaseSplit |
| CSWith | Agda.Auto.CaseSplit |
| cthandles | Agda.Auto.NarrowingSearch |
| ctparent | Agda.Auto.NarrowingSearch |
| ctpriometa | Agda.Auto.NarrowingSearch |
| CTrans | Agda.TypeChecking.SizedTypes.Syntax |
| 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 |
| curFun | Agda.Compiler.Epic.CompileState |
| curHsMod | Agda.Compiler.MAlonzo.Misc |
| curIF | Agda.Compiler.MAlonzo.Misc |
| curMName | Agda.Compiler.MAlonzo.Misc |
| curModule | |
| 1 (Function) | Agda.Compiler.Epic.CompileState |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| CurrentInput | Agda.Syntax.Parser.Alex |
| currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| currentProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| curriedApply | Agda.Compiler.JS.Substitution |
| curriedLambda | Agda.Compiler.JS.Substitution |
| curryAt | Agda.TypeChecking.Records |
| curSig | Agda.Compiler.MAlonzo.Misc |
| CutOff | |
| 1 (Type/Class) | Agda.Termination.CutOff |
| 2 (Data Constructor) | Agda.Termination.CutOff |
| CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |