| C | |
| 1 (Data Constructor) | Agda.Auto.Options |
| 2 (Type/Class) | Agda.Utils.Cluster |
| cacheCurrentLog | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching |
| CachedTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cachingStarts | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| callBackend | Agda.Compiler.Backend |
| callByName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| callInfoCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| callInfoRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| callInfos | Agda.Termination.Monad |
| callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| callMain | Agda.Compiler.JS.Syntax |
| 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 |
| callMatrixSet | Agda.Termination.CallGraph |
| CallPath | |
| 1 (Type/Class) | Agda.Termination.Monad |
| 2 (Data Constructor) | Agda.Termination.Monad |
| CallSite | Agda.Utils.CallStack |
| CallSiteFilter | Agda.Utils.CallStack |
| CallStack | Agda.Utils.CallStack |
| callStack | Agda.Utils.CallStack |
| CALNil | Agda.Auto.Syntax |
| camelTo2 | Agda.Interaction.JSON |
| Candidate | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CandidateKind | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| candidateKind | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| candidateOverlappable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| candidateTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| candidateType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| canHaveSuffixTest | Agda.Syntax.Scope.Monad |
| CannotCreateMissingClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CannotResolveAmbiguousPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| canonicalizeAbsolutePath | Agda.Utils.FileName |
| canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
| canonicalName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| canProject | Agda.TypeChecking.Substitute |
| CantGeneralizeOverSorts | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CantGeneralizeOverSorts_ | Agda.Interaction.Options.Warnings |
| CantInvert | Agda.TypeChecking.MetaVars |
| CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitBlocker | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitConIdx | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitConName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitFailures | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitGivenIdx | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cantSplitTel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Carrier | Agda.Utils.Zipper |
| Case | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| 3 (Type/Class) | Agda.TypeChecking.CompiledClause |
| CaseContext | Agda.Interaction.MakeCase |
| caseEitherM | Agda.Utils.Either |
| CaseInfo | |
| 1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| caseLazy | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| caseList | Agda.Utils.List |
| caseListM | Agda.Utils.List |
| caseListT | Agda.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 |
| CaseSplit | Agda.Syntax.Common |
| caseSplitSearch | Agda.Auto.CaseSplit |
| caseSplitSearch' | Agda.Auto.CaseSplit |
| caseToSeq | Agda.Compiler.Treeless.Uncase |
| CaseType | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| caseType | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve |
| castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve |
| cat | Agda.Utils.Pretty |
| Catchall | Agda.Syntax.Concrete.Definitions.Types |
| catchAll | Agda.TypeChecking.CompiledClause |
| catchAllBranch | Agda.TypeChecking.CompiledClause |
| CatchallClause | Agda.Interaction.Highlighting.Precise |
| CatchallPragma | Agda.Syntax.Concrete |
| catchallPragma | Agda.Syntax.Concrete.Definitions.Monad |
| catchAndPrintImpossible | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| catchConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| catchError_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term |
| CatchImpossible | Agda.Utils.Impossible |
| catchImpossible | Agda.Utils.Impossible |
| catchImpossibleJust | Agda.Utils.Impossible |
| CatchIO | Agda.Utils.IO |
| catchIO | Agda.Utils.IO |
| catchPatternErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| categorizedecl | Agda.Auto.Syntax |
| catMaybes | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| 3 (Function) | Agda.Utils.List1 |
| catMaybesMP | Agda.Utils.Monad |
| CC | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
| 2 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| CCContext | Agda.Compiler.MAlonzo.Compiler |
| ccContext | Agda.Compiler.MAlonzo.Compiler |
| CCEnv | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| ccNameSupply | Agda.Compiler.MAlonzo.Compiler |
| CCT | Agda.Compiler.MAlonzo.Compiler |
| cdcont | Agda.Auto.Syntax |
| cddeffreevars | Agda.Auto.Syntax |
| cdname | Agda.Auto.Syntax |
| cdorigin | Agda.Auto.Syntax |
| cdtype | Agda.Auto.Syntax |
| CErased | Agda.Syntax.Common |
| CExp | Agda.Auto.Syntax |
| CFull | Agda.Syntax.Common |
| Change | Agda.Utils.Update |
| ChangeT | Agda.Utils.Update |
| Char | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| char | Agda.Utils.Pretty |
| chaseDisplayForms | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| checkAbsurdLambda | Agda.TypeChecking.Rules.Term |
| checkAlias | Agda.TypeChecking.Rules.Def |
| checkApplication | Agda.TypeChecking.Rules.Application |
| CheckArgs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CheckArguments | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkArguments | Agda.TypeChecking.Rules.Application |
| checkArguments_ | Agda.TypeChecking.Rules.Application |
| checkAxiom | Agda.TypeChecking.Rules.Decl |
| checkAxiom' | Agda.TypeChecking.Rules.Decl |
| CheckClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkClause | Agda.TypeChecking.Rules.Def |
| checkClauseLHS | Agda.TypeChecking.Rules.Def |
| checkClauseTelescopeBindings | Agda.Syntax.Translation.ReflectedToAbstract |
| checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl |
| checkCompilerPragmas | Agda.Compiler.JS.Compiler |
| CheckConfluence | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkConfluenceOfClauses | Agda.TypeChecking.Rewriting.Confluence |
| checkConfluenceOfRules | Agda.TypeChecking.Rewriting.Confluence |
| CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkConstructor | Agda.TypeChecking.Rules.Data |
| checkConstructorCount | Agda.Compiler.MAlonzo.HaskellTypes |
| CheckConstructorFitsIn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkConstructorType | Agda.Compiler.MAlonzo.Compiler |
| checkCover | Agda.Compiler.MAlonzo.Compiler |
| CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkDataDef | Agda.TypeChecking.Rules.Data |
| checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
| checkDeclCached | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
| checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
| checkDisplayPragma | Agda.TypeChecking.Rules.Display |
| checkDomain | Agda.TypeChecking.Rules.Term |
| checkDontExpandLast | Agda.TypeChecking.Rules.Term |
| CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkEarlierThan | Agda.TypeChecking.Lock |
| checkedMainDecl | Agda.Compiler.MAlonzo.Primitives |
| checkedMainDef | Agda.Compiler.MAlonzo.Primitives |
| CheckedMainFunctionDef | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives |
| CheckedTarget | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkeliminand | Agda.Auto.Typecheck |
| checkEmptyTel | Agda.TypeChecking.Empty |
| CheckExpr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
| checkExpr' | Agda.TypeChecking.Rules.Term |
| CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkExtendedLambda | Agda.TypeChecking.Rules.Term |
| checkForImportCycle | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkFunDef | Agda.TypeChecking.Rules.Def |
| checkFunDef' | Agda.TypeChecking.Rules.Def |
| CheckFunDefCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkFunDefS | Agda.TypeChecking.Rules.Def |
| checkGeneralize | Agda.TypeChecking.Rules.Decl |
| checkGeneralizeTelescope | Agda.TypeChecking.Rules.Term |
| checkIApplyConfluence | Agda.TypeChecking.IApplyConfluence |
| checkIApplyConfluence_ | Agda.TypeChecking.IApplyConfluence |
| checkImport | Agda.TypeChecking.Rules.Decl |
| checkIndexSorts | Agda.TypeChecking.Rules.Data |
| checkInjectivity | Agda.TypeChecking.Injectivity |
| checkInjectivity' | Agda.TypeChecking.Injectivity |
| checkInjectivity_ | Agda.TypeChecking.Rules.Decl |
| checkInternal | Agda.TypeChecking.CheckInternal |
| checkInternal' | Agda.TypeChecking.CheckInternal |
| checkInternalType' | Agda.TypeChecking.CheckInternal |
| CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CheckK | Agda.Compiler.MAlonzo.Misc |
| checkKnownArgument | Agda.TypeChecking.Rules.Term |
| checkKnownArguments | Agda.TypeChecking.Rules.Term |
| CheckLambda | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkLambda | Agda.TypeChecking.Rules.Term |
| checkLambda' | Agda.TypeChecking.Rules.Term |
| checkLazyMatch | Agda.TypeChecking.CompiledClause |
| checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
| CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkLetBinding | Agda.TypeChecking.Rules.Term |
| checkLetBindings | Agda.TypeChecking.Rules.Term |
| checkLevel | Agda.TypeChecking.Rules.Term |
| CheckLHS | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkLinearity | Agda.TypeChecking.MetaVars |
| checkLiteral | Agda.TypeChecking.Rules.Term |
| CheckLock | Agda.Interaction.Base |
| CheckLockedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkLockedVars | Agda.TypeChecking.Lock |
| checkLoneSigs | Agda.Syntax.Concrete.Definitions.Monad |
| checkMacroType | Agda.TypeChecking.Rules.Def |
| checkMeta | Agda.TypeChecking.Rules.Term |
| CheckMetaInst | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkMetaInst | Agda.TypeChecking.MetaVars |
| CheckMetaSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkModuleArity | Agda.TypeChecking.Rules.Decl |
| checkModuleName | Agda.Interaction.FindFile |
| checkMutual | Agda.TypeChecking.Rules.Decl |
| checkNamedArg | Agda.TypeChecking.Rules.Term |
| CheckNamedWhere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkNoFixityInRenamingModule | Agda.Syntax.Scope.Monad |
| checkNoShadowing | Agda.Syntax.Scope.Monad |
| checkOpts | Agda.Interaction.Options |
| checkOrInferMeta | Agda.TypeChecking.Rules.Term |
| checkOverapplication | Agda.TypeChecking.Injectivity |
| checkPath | Agda.TypeChecking.Rules.Term |
| CheckPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkPatternLinearity | Agda.Syntax.Abstract.Pattern |
| CheckPatternLinearityType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CheckPatternLinearityValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkPiDomain | Agda.TypeChecking.Rules.Term |
| checkPiTelescope | Agda.TypeChecking.Rules.Term |
| checkpoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| CheckpointId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkpointSubstitution | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| checkpointSubstitution' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| checkPositivity_ | Agda.TypeChecking.Rules.Decl |
| checkPostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch |
| checkPostponedLambda | Agda.TypeChecking.Rules.Term |
| checkPostponedLambda0 | Agda.TypeChecking.Rules.Term |
| CheckPragma | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkPragma | Agda.TypeChecking.Rules.Decl |
| CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkPrimitive | Agda.TypeChecking.Rules.Decl |
| CheckProjAppToKnownPrincipalArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkProjAppToKnownPrincipalArg | Agda.TypeChecking.Rules.Application |
| CheckProjection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl |
| checkQuestionMark | Agda.TypeChecking.Rules.Term |
| CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkRecDef | Agda.TypeChecking.Rules.Record |
| checkRecordExpression | Agda.TypeChecking.Rules.Term |
| checkRecordProjections | Agda.TypeChecking.Rules.Record |
| checkRecordUpdate | Agda.TypeChecking.Rules.Term |
| CheckResult | |
| 1 (Type/Class) | Agda.Compiler.Backend, Agda.Interaction.Imports |
| 2 (Data Constructor) | Agda.Compiler.Backend, Agda.Interaction.Imports |
| checkRewriteRule | Agda.TypeChecking.Rewriting |
| CheckRHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| checkRHS | Agda.TypeChecking.Rules.Def |
| checkSection | Agda.TypeChecking.Rules.Decl |
| CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkSectionApplication | Agda.TypeChecking.Rules.Decl |
| checkSectionApplication' | Agda.TypeChecking.Rules.Decl |
| CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkSizeLtSat | Agda.TypeChecking.SizedTypes |
| checkSizeNeverZero | Agda.TypeChecking.SizedTypes |
| checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes |
| checkSolutionForMeta | Agda.TypeChecking.MetaVars |
| checkSort | Agda.TypeChecking.CheckInternal |
| checkSortOfSplitVar | Agda.TypeChecking.Rules.LHS |
| checkStrictlyPositive | Agda.TypeChecking.Positivity |
| checkSubtypeIsEqual | Agda.TypeChecking.MetaVars |
| checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality |
| checkSystemCoverage | Agda.TypeChecking.Rules.Def |
| checkTacticAttribute | Agda.TypeChecking.Rules.Term |
| CheckTargetType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkTelePiSort | Agda.TypeChecking.Sort |
| checkTelescope | Agda.TypeChecking.Rules.Term |
| checkTelescope' | Agda.TypeChecking.Rules.Term |
| checkTermination_ | Agda.TypeChecking.Rules.Decl |
| checkType | Agda.TypeChecking.CheckInternal |
| checkType' | Agda.TypeChecking.CheckInternal |
| checkTypeCheckingProblem | Agda.TypeChecking.Constraints |
| checkTypedBindings | Agda.TypeChecking.Rules.Term |
| checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
| checkTypeOfMain' | Agda.Compiler.MAlonzo.Primitives |
| checkTypeSignature | Agda.TypeChecking.Rules.Decl |
| checkTypeSignature' | Agda.TypeChecking.Rules.Decl |
| checkUnderscore | Agda.TypeChecking.Rules.Term |
| checkUnquoteDecl | Agda.TypeChecking.Rules.Decl |
| checkUnquoteDef | Agda.TypeChecking.Rules.Decl |
| checkWhere | Agda.TypeChecking.Rules.Def |
| checkWithFunction | Agda.TypeChecking.Rules.Def |
| CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| checkWithRHS | Agda.TypeChecking.Rules.Def |
| Choice | Agda.Auto.NarrowingSearch |
| choice | Agda.TypeChecking.Unquote |
| choiceP | Agda.Utils.Parser.MemoisedCPS |
| choose | Agda.Auto.NarrowingSearch |
| ChooseEither | Agda.TypeChecking.Rules.LHS.Problem |
| ChooseFlex | Agda.TypeChecking.Rules.LHS.Problem |
| chooseFlex | Agda.TypeChecking.Rules.LHS.Problem |
| chooseHighlightingMethod | Agda.Interaction.Highlighting.Common |
| ChooseLeft | Agda.TypeChecking.Rules.LHS.Problem |
| choosePrioMeta | Agda.Auto.NarrowingSearch |
| ChooseRight | Agda.TypeChecking.Rules.LHS.Problem |
| chop | Agda.Utils.List |
| chopWhen | Agda.Utils.List |
| Chr | Agda.Utils.Pretty |
| Cl | |
| 1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile |
| 2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile |
| cl | Agda.TypeChecking.Names |
| cl' | Agda.TypeChecking.Names |
| ClashesViaRenaming | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClashesViaRenaming_ | Agda.Interaction.Options.Warnings |
| ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClashingImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClashingModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| classifyForeign | Agda.Compiler.MAlonzo.Pragmas |
| classifyPragma | Agda.Compiler.MAlonzo.Pragmas |
| classifyWarning | Agda.TypeChecking.Warnings |
| classifyWarnings | Agda.TypeChecking.Warnings |
| Clause | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| 3 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
| 4 (Type/Class) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Internal |
| 6 (Type/Class) | Agda.Syntax.Reflected |
| 7 (Data Constructor) | Agda.Syntax.Reflected |
| 8 (Type/Class) | Agda.Syntax.Abstract |
| 9 (Data Constructor) | Agda.Syntax.Abstract |
| Clause' | Agda.Syntax.Abstract |
| clauseArgs | Agda.Syntax.Internal.Pattern |
| clauseBody | Agda.Syntax.Internal |
| clauseCatchall | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.Syntax.Abstract |
| clauseElims | Agda.Syntax.Internal.Pattern |
| clauseEllipsis | Agda.Syntax.Internal |
| clauseExact | Agda.Syntax.Internal |
| clauseFullRange | Agda.Syntax.Internal |
| clauseLHS | Agda.Syntax.Abstract |
| clauseLHSRange | Agda.Syntax.Internal |
| clausePats | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.Syntax.Reflected |
| clausePerm | Agda.Syntax.Internal.Pattern |
| clauseQName | Agda.TypeChecking.Rewriting.Clause |
| clauseRecursive | Agda.Syntax.Internal |
| clauseRHS | |
| 1 (Function) | Agda.Syntax.Reflected |
| 2 (Function) | Agda.Syntax.Abstract |
| ClausesPostChecks | Agda.TypeChecking.Rules.Def |
| clauseStrippedPats | Agda.Syntax.Abstract |
| clauseTel | |
| 1 (Function) | Agda.Syntax.Internal |
| 2 (Function) | Agda.Syntax.Reflected |
| clauseToRewriteRule | Agda.TypeChecking.Rewriting.Clause |
| clauseToSplitClause | Agda.TypeChecking.Coverage |
| clauseType | Agda.Syntax.Internal |
| clauseUnreachable | Agda.Syntax.Internal |
| clauseWhereDecls | Agda.Syntax.Abstract |
| ClauseZipper | Agda.Interaction.MakeCase |
| clBody | Agda.TypeChecking.CompiledClause.Compile |
| Clean | Agda.TypeChecking.Unquote |
| clean | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| cleanCachedLog | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching |
| clearAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| clearMetaListeners | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| clearRunningInfo | Agda.Interaction.EmacsCommand |
| clearWarning | Agda.Interaction.EmacsCommand |
| clEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| clModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ClockTime | Agda.Utils.Time |
| Clos | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| closed | Agda.TypeChecking.Free |
| ClosedLevel | Agda.Syntax.Internal |
| closedTerm | Agda.Compiler.MAlonzo.Compiler |
| closedTermToTreeless | Agda.Compiler.ToTreeless |
| closedTerm_ | Agda.Compiler.MAlonzo.Compiler |
| ClosedType | Agda.TypeChecking.Rules.Data |
| closeVerboseBracket | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| closeVerboseBracketException | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| closify | Agda.Auto.Syntax |
| Closure | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| clPats | Agda.TypeChecking.CompiledClause.Compile |
| Cls | Agda.TypeChecking.CompiledClause.Compile |
| clScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| clSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cluster | Agda.Utils.Cluster |
| cluster' | Agda.Utils.Cluster |
| clValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| cmdToName | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| Cmd_abort | Agda.Interaction.Base |
| Cmd_autoAll | Agda.Interaction.Base |
| Cmd_autoOne | Agda.Interaction.Base |
| Cmd_compile | Agda.Interaction.Base |
| Cmd_compute | Agda.Interaction.Base |
| Cmd_compute_toplevel | Agda.Interaction.Base |
| Cmd_constraints | Agda.Interaction.Base |
| Cmd_context | Agda.Interaction.Base |
| Cmd_elaborate_give | Agda.Interaction.Base |
| Cmd_exit | Agda.Interaction.Base |
| Cmd_give | Agda.Interaction.Base |
| Cmd_goal_type | Agda.Interaction.Base |
| Cmd_goal_type_context | Agda.Interaction.Base |
| cmd_goal_type_context_and | Agda.Interaction.InteractionTop |
| Cmd_goal_type_context_check | Agda.Interaction.Base |
| Cmd_goal_type_context_infer | Agda.Interaction.Base |
| Cmd_helper_function | Agda.Interaction.Base |
| Cmd_highlight | Agda.Interaction.Base |
| Cmd_infer | Agda.Interaction.Base |
| Cmd_infer_toplevel | Agda.Interaction.Base |
| Cmd_intro | Agda.Interaction.Base |
| Cmd_load | Agda.Interaction.Base |
| cmd_load' | Agda.Interaction.InteractionTop |
| Cmd_load_highlighting_info | Agda.Interaction.Base |
| Cmd_make_case | Agda.Interaction.Base |
| Cmd_metas | Agda.Interaction.Base |
| Cmd_refine | Agda.Interaction.Base |
| Cmd_refine_or_intro | Agda.Interaction.Base |
| Cmd_search_about_toplevel | Agda.Interaction.Base |
| Cmd_show_module_contents | Agda.Interaction.Base |
| Cmd_show_module_contents_toplevel | Agda.Interaction.Base |
| Cmd_show_version | Agda.Interaction.Base |
| Cmd_solveAll | Agda.Interaction.Base |
| Cmd_solveOne | Agda.Interaction.Base |
| Cmd_tokenHighlighting | Agda.Interaction.Base |
| Cmd_why_in_scope | Agda.Interaction.Base |
| Cmd_why_in_scope_toplevel | Agda.Interaction.Base |
| 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.Base |
| CmpEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CmpInType | Agda.Interaction.Base |
| CmpLeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CmpLevels | Agda.Interaction.Base |
| CmpSorts | Agda.Interaction.Base |
| CmpTeles | Agda.Interaction.Base |
| CmpTypes | Agda.Interaction.Base |
| CMRigid | Agda.Auto.Typecheck |
| CMSet | |
| 1 (Type/Class) | Agda.Termination.CallMatrix |
| 2 (Data Constructor) | Agda.Termination.CallMatrix |
| cmSet | Agda.Termination.CallMatrix |
| CoConName | Agda.Syntax.Scope.Base |
| Code | Agda.Syntax.Parser.Literate |
| code | Agda.Syntax.Parser.Lexer |
| CoDomain | Agda.Utils.TypeLevel |
| CoDomain' | Agda.Utils.TypeLevel |
| coerce | Agda.TypeChecking.Conversion |
| coerceAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| coerceSize | Agda.TypeChecking.Conversion |
| coerceView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Cohesion | Agda.Syntax.Common |
| CohesionAttribute | Agda.Syntax.Concrete.Attribute |
| cohesionAttributeTable | Agda.Syntax.Concrete.Attribute |
| CoinductionKit | |
| 1 (Type/Class) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| 2 (Data Constructor) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| coinductionKit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| coinductionKit' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| CoInductive | Agda.Syntax.Common |
| CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CoInfectiveImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CoInfectiveImport_ | Agda.Interaction.Options.Warnings |
| coinfectiveOptions | Agda.Interaction.Options |
| col | Agda.Termination.SparseMatrix |
| coldescr | Agda.Utils.Warshall |
| collapseDefault | Agda.Utils.WithDefault |
| collapseO | Agda.Termination.Order |
| Collection | Agda.Utils.Singleton |
| collectStats | Agda.TypeChecking.Serialise.Base |
| colon | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| cols | Agda.Termination.SparseMatrix |
| Column | Agda.Syntax.Parser.Monad |
| combineHashes | Agda.Utils.Hash |
| comma | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Command | |
| 1 (Type/Class) | Agda.Interaction.Base |
| 2 (Data Constructor) | Agda.Interaction.Base |
| Command' | Agda.Interaction.Base |
| commandLineFlags | Agda.Compiler.Backend |
| CommandLineOptions | Agda.Interaction.Options |
| commandLineOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CommandM | Agda.Interaction.Base |
| commandMToIO | Agda.Interaction.InteractionTop |
| CommandQueue | |
| 1 (Type/Class) | Agda.Interaction.Base |
| 2 (Data Constructor) | Agda.Interaction.Base |
| commandQueue | Agda.Interaction.Base |
| commands | Agda.Interaction.Base |
| CommandState | |
| 1 (Type/Class) | Agda.Interaction.Base |
| 2 (Data Constructor) | Agda.Interaction.Base |
| Comment | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Type/Class) | Agda.Compiler.JS.Syntax |
| 3 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 4 (Data Constructor) | Agda.Syntax.Parser.Literate |
| 5 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| commitInfo | Agda.VersionCommit |
| commonParentModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| commonPrefix | Agda.Utils.List |
| commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| commonSuffix | Agda.Utils.List |
| comp' | Agda.Auto.Typecheck |
| Compaction | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| compactP | Agda.Utils.Permutation |
| compactS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| Comparable | Agda.Utils.PartialOrd |
| comparable | Agda.Utils.PartialOrd |
| comparableOrd | Agda.Utils.PartialOrd |
| Compare | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| compareArgs | Agda.TypeChecking.Conversion |
| CompareAs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compareAs | Agda.TypeChecking.Conversion |
| compareAs' | Agda.TypeChecking.Conversion |
| compareAsDir | Agda.TypeChecking.Conversion |
| compareAtom | Agda.TypeChecking.Conversion |
| compareAtomDir | Agda.TypeChecking.Conversion |
| compareBelowMax | Agda.TypeChecking.SizedTypes |
| compareCohesion | Agda.TypeChecking.Conversion |
| CompareDirection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compareDom | Agda.TypeChecking.Conversion |
| compareElims | Agda.TypeChecking.Conversion |
| compareFavorites | Agda.Utils.Favorites |
| compareInterval | Agda.TypeChecking.Conversion |
| compareIrrelevant | Agda.TypeChecking.Conversion |
| compareLevel | Agda.TypeChecking.Conversion |
| compareMaxViews | Agda.TypeChecking.SizedTypes |
| compareOffset | Agda.TypeChecking.SizedTypes.Syntax |
| compareQuantity | Agda.TypeChecking.Conversion |
| compareRelevance | Agda.TypeChecking.Conversion |
| CompareResult | Agda.Utils.Favorites |
| compareSizes | Agda.TypeChecking.SizedTypes |
| compareSizeViews | Agda.TypeChecking.SizedTypes |
| compareSort | Agda.TypeChecking.Conversion |
| compareTerm | Agda.TypeChecking.Conversion |
| compareTerm' | Agda.TypeChecking.Conversion |
| compareTermOnFace | Agda.TypeChecking.Conversion |
| compareTermOnFace' | Agda.TypeChecking.Conversion |
| compareType | Agda.TypeChecking.Conversion |
| compareWithFavorites | Agda.Utils.Favorites |
| compareWithPol | Agda.TypeChecking.Conversion |
| Comparison | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compGlue | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| compHCompU | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| CompilationError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compile | Agda.TypeChecking.CompiledClause.Compile |
| compileAlt | Agda.Compiler.JS.Compiler |
| compileClauses | Agda.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 |
| compiledClauseBody | Agda.TypeChecking.Substitute |
| CompiledClauses | Agda.TypeChecking.CompiledClause |
| CompiledClauses' | Agda.TypeChecking.CompiledClause |
| compiledcondecl | Agda.Compiler.MAlonzo.Compiler |
| compileDef | Agda.Compiler.Backend |
| compileDir | Agda.Compiler.Common |
| CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compiledTypeSynonym | Agda.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 |
| CompilerBackend | Agda.Interaction.Base |
| CompilerPragma | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| compileTerm | Agda.Compiler.JS.Compiler |
| compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile |
| CompKit | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| complement | Agda.Utils.SmallSet |
| complete | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.Termination.CallGraph |
| completeIter | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| completionStep | Agda.Termination.CallGraph |
| compose | Agda.TypeChecking.SizedTypes.Utils |
| composeCohesion | Agda.Syntax.Common |
| composeErased | Agda.Syntax.Common |
| composeFlexRig | Agda.TypeChecking.Free.Lazy |
| composeModality | Agda.Syntax.Common |
| composeP | Agda.Utils.Permutation |
| composePol | Agda.TypeChecking.Polarity |
| composeQuantity | Agda.Syntax.Common |
| composeRelevance | Agda.Syntax.Common |
| composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| composeVarOcc | Agda.TypeChecking.Free.Lazy |
| composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| ComposeZip | Agda.Utils.Zipper |
| ComposeZipper | Agda.Utils.Zipper |
| Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| computeEdges | Agda.TypeChecking.Positivity |
| computeElimHeadType | Agda.TypeChecking.Conversion |
| computeErasedConstructorArgs | Agda.Compiler.Treeless.Erase |
| computeFixitiesAndPolarities | Agda.Syntax.Scope.Monad |
| computeForcingAnnotations | Agda.TypeChecking.Forcing |
| computeIgnoreAbstract | Agda.Interaction.BasicOps |
| ComputeMode | Agda.Interaction.Base |
| computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| ComputeOccurrences | Agda.TypeChecking.Positivity |
| computeOccurrences | Agda.TypeChecking.Positivity |
| computeOccurrences' | Agda.TypeChecking.Positivity |
| computePolarity | Agda.TypeChecking.Polarity |
| computeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
| computeUnsolvedInfo | Agda.Interaction.Highlighting.Generate |
| computeWrapInput | Agda.Interaction.BasicOps |
| Con | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Reflected |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| conAbstr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conApp | Agda.TypeChecking.Substitute |
| conArgs | Agda.TypeChecking.MetaVars.Occurs |
| ConArgType | Agda.TypeChecking.Positivity.Occurrence |
| conArity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conBranches | Agda.TypeChecking.CompiledClause |
| conCase | Agda.TypeChecking.CompiledClause |
| Concat | Agda.TypeChecking.Positivity |
| concat | Agda.Utils.List1 |
| Concat' | Agda.TypeChecking.Positivity |
| concatargs | Agda.Auto.CaseSplit |
| concatListT | Agda.Utils.ListT |
| conComp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConcreteDef | Agda.Syntax.Common |
| ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| concreteNamesInScope | Agda.Syntax.Scope.Base |
| concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
| concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract |
| conData | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conDataRecord | Agda.Syntax.Internal |
| ConDecl | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| condecl | Agda.Compiler.MAlonzo.Compiler |
| Condition | Agda.TypeChecking.MetaVars |
| conErased | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conFields | Agda.Syntax.Internal |
| configAgdaLibFiles | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| configRoot | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| Confirmed | Agda.Syntax.Parser.Monad |
| confirmLayout | Agda.Syntax.Parser.Layout |
| ConfluenceCheck | Agda.Interaction.Options |
| ConfluenceProblem | Agda.Interaction.Highlighting.Precise |
| conForced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| conInductive | Agda.Syntax.Internal |
| ConInfo | Agda.Syntax.Internal |
| ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Conj | Agda.TypeChecking.Conversion |
| ConK | Agda.Compiler.MAlonzo.Misc |
| conKindOfName | Agda.Syntax.Scope.Base |
| conKindOfName' | Agda.Syntax.Scope.Base |
| ConName | Agda.Syntax.Scope.Base |
| conName | Agda.Syntax.Internal |
| ConnectHandle | Agda.Auto.NarrowingSearch |
| connectInteractionPoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| ConOCon | Agda.Syntax.Common |
| ConOfAbs | Agda.Syntax.Translation.AbstractToConcrete |
| ConORec | Agda.Syntax.Common |
| ConOrigin | Agda.Syntax.Common |
| ConOSplit | Agda.Syntax.Common |
| ConOSystem | Agda.Syntax.Common |
| ConP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Reflected |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| conPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConPatEager | Agda.Syntax.Info |
| ConPatInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| conPatInfo | Agda.Syntax.Info |
| ConPatLazy | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| conPatLazy | Agda.Syntax.Info |
| conPatOrigin | Agda.Syntax.Info |
| ConPatternInfo | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| conPFallThrough | Agda.Syntax.Internal |
| conPInfo | Agda.Syntax.Internal |
| conPLazy | Agda.Syntax.Internal |
| conPRecord | Agda.Syntax.Internal |
| conProj | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conPType | Agda.Syntax.Internal |
| Cons | |
| 1 (Data Constructor) | Agda.Utils.IndexedList |
| 2 (Data Constructor) | Agda.Interaction.EmacsCommand |
| cons | Agda.Utils.List1 |
| consecutiveAndSeparated | Agda.Syntax.Position |
| ConsHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| consListT | Agda.Utils.ListT |
| ConsMap0 | Agda.Utils.TypeLevel |
| ConsMap1 | Agda.Utils.TypeLevel |
| consMListT | Agda.Utils.ListT |
| consOfHIT | Agda.TypeChecking.Datatypes |
| conSrcCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| consS | Agda.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 |
| Constant | Agda.Utils.TypeLevel |
| Constant0 | Agda.Utils.TypeLevel |
| Constant1 | Agda.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 |
| constrainedPrims | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.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.Compiler.Backend, Agda.TypeChecking.Monad |
| Constraint' | Agda.TypeChecking.SizedTypes.Syntax |
| constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
| constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| constraintMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| constraintProblems | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Constraints | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConstraintStatus | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| constraintUnblocker | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConstRef | Agda.Auto.Syntax |
| Constructor | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ConstructorBlock | Agda.Syntax.Concrete.Definitions.Types |
| constructorCoverageCode | Agda.Compiler.MAlonzo.Compiler |
| constructorForm | |
| 1 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| 2 (Function) | Agda.TypeChecking.Reduce.Monad |
| constructorForm' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| constructorImpossible | Agda.Auto.Typecheck |
| ConstructorInfo | Agda.TypeChecking.Datatypes |
| ConstructorName | Agda.Syntax.Scope.Base |
| ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| constructorTagModifier | Agda.Interaction.JSON |
| constructPats | Agda.Auto.Convert |
| constructs | Agda.TypeChecking.Rules.Data |
| constTranspAxiom | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| containsAbsurdPattern | Agda.Syntax.Abstract.Pattern |
| containsAPattern | Agda.Syntax.Abstract.Pattern |
| containsAsPattern | Agda.Syntax.Abstract.Pattern |
| contains_constructor | Agda.Auto.Convert |
| content | Agda.TypeChecking.CompiledClause |
| contentsFieldName | Agda.Interaction.JSON |
| Context | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ContextEntry | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ContextLet | Agda.Interaction.Base |
| contextOfMeta | Agda.Interaction.BasicOps |
| contextSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| ContextVar | Agda.Interaction.Base |
| Continuous | Agda.Syntax.Common |
| continuous | Agda.Syntax.Position |
| continuousPerLine | Agda.Syntax.Position |
| Contravariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| conUseSizeLt | Agda.Termination.Monad |
| convError | Agda.TypeChecking.Conversion |
| Conversion | Agda.Auto.Convert |
| Convert | Agda.Interaction.Highlighting.Precise |
| convert | |
| 1 (Function) | Agda.Interaction.Highlighting.Precise |
| 2 (Function) | Agda.Auto.Convert |
| convertGuards | Agda.Compiler.Treeless.GuardsToPrims |
| CopatternMatching | Agda.Syntax.Common |
| CopatternMatchingAllowed | Agda.Syntax.Common |
| copatternMatchingAllowed | Agda.Syntax.Common |
| CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| copatternsNotImplemented | Agda.Auto.Convert |
| copyarg | Agda.Auto.Typecheck |
| copyDirContent | Agda.Utils.IO.Directory |
| copyRTEModules | Agda.Compiler.MAlonzo.Compiler |
| copyScope | Agda.Syntax.Scope.Monad |
| copyTerm | Agda.Syntax.Internal.Generic |
| CosplitCatchall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CosplitNoRecordType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CosplitNoTarget | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Cost | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 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 |
| costUnificationIf | Agda.Auto.SearchControl |
| costUnificationOccurs | Agda.Auto.SearchControl |
| count | Agda.Utils.Bag |
| CountPatternVars | Agda.Syntax.Internal.Pattern |
| countPatternVars | Agda.Syntax.Internal.Pattern |
| countWithArgs | Agda.TypeChecking.With |
| Covariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| CoverageCheck | Agda.Syntax.Common |
| coverageCheck | |
| 1 (Function) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Function) | Agda.TypeChecking.Coverage |
| coverageCheckPragma | Agda.Syntax.Concrete.Definitions.Monad |
| CoverageIssue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CoverageIssue_ | Agda.Interaction.Options.Warnings |
| CoverageNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| CoverageNoExactSplit_ | Agda.Interaction.Options.Warnings |
| CoverageProblem | Agda.Interaction.Highlighting.Precise |
| Covering | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage |
| 2 (Data Constructor) | Agda.TypeChecking.Coverage |
| coveringRange | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| CoverK | Agda.Compiler.MAlonzo.Misc |
| covSplitArg | Agda.TypeChecking.Coverage |
| covSplitClauses | Agda.TypeChecking.Coverage |
| CPatternLike | Agda.Syntax.Concrete.Pattern |
| CPC | Agda.TypeChecking.Rules.Def |
| cpcPartialSplits | Agda.TypeChecking.Rules.Def |
| CPUTime | |
| 1 (Type/Class) | Agda.Utils.Time |
| 2 (Data Constructor) | Agda.Utils.Time |
| createMetaInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| createMetaInfo' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| createModule | Agda.Syntax.Scope.Monad |
| crInterface | Agda.Compiler.Backend, Agda.Interaction.Imports |
| crMode | Agda.Compiler.Backend, Agda.Interaction.Imports |
| crModuleInfo | Agda.Interaction.Imports |
| crSource | Agda.Interaction.Imports |
| crWarnings | Agda.Compiler.Backend, Agda.Interaction.Imports |
| 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 |
| CTChar | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| CTData | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| CTFloat | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| cthandles | Agda.Auto.NarrowingSearch |
| CTInt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| CTNat | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| ctparent | Agda.Auto.NarrowingSearch |
| ctpriometa | Agda.Auto.NarrowingSearch |
| CTQName | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| CTrans | Agda.TypeChecking.SizedTypes.Syntax |
| CTree | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| cTreeless | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| CTString | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| ctsub | Agda.Auto.NarrowingSearch |
| Ctx | Agda.Auto.Syntax |
| CType | Agda.TypeChecking.Rules.Data |
| Cubical | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Common |
| curAgdaMod | Agda.Compiler.MAlonzo.Misc |
| curDefs | Agda.Compiler.Common |
| curHsMod | Agda.Compiler.MAlonzo.Misc |
| curIF | Agda.Compiler.Common |
| curIsMainModule | Agda.Compiler.MAlonzo.Misc |
| curMName | Agda.Compiler.Common |
| curOutFile | Agda.Compiler.MAlonzo.Compiler |
| curOutFileAndDir | Agda.Compiler.MAlonzo.Compiler |
| CurrentAccount | Agda.Utils.Benchmark |
| currentAccount | Agda.Utils.Benchmark |
| currentCxt | Agda.TypeChecking.Names |
| CurrentFile | |
| 1 (Type/Class) | Agda.Interaction.Base |
| 2 (Data Constructor) | Agda.Interaction.Base |
| currentFileArgs | Agda.Interaction.Base |
| currentFilePath | Agda.Interaction.Base |
| currentFileStamp | Agda.Interaction.Base |
| CurrentInput | Agda.Syntax.Parser.Alex |
| currentModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| currentModuleNameHash | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| currentOrFreshMutualBlock | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual |
| CurrentTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| curriedApply | Agda.Compiler.JS.Substitution |
| curriedLambda | Agda.Compiler.JS.Substitution |
| curryAt | Agda.TypeChecking.Records |
| Currying | Agda.Utils.TypeLevel |
| currys | Agda.Utils.TypeLevel |
| CutOff | |
| 1 (Type/Class) | Agda.Termination.CutOff |
| 2 (Data Constructor) | Agda.Termination.CutOff |
| cxtSubst | Agda.TypeChecking.Names |
| cycle | Agda.Utils.List1 |
| CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |