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

Index - C

CAgda.Auto.Options
cacheCurrentLogAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
CachedTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cachingStartsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
CActionAgda.Auto.Syntax
calcAgda.Auto.NarrowingSearch
calcEqRStateAgda.Auto.Typecheck
CALConcatAgda.Auto.Syntax
Call 
1 (Type/Class)Agda.Termination.CallGraph
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callBackendAgda.Compiler.Backend
callByNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
CallCombAgda.Termination.CallMatrix
callCompilerAgda.Compiler.CallCompiler
callCompiler'Agda.Compiler.CallCompiler
callGHCAgda.Compiler.MAlonzo.Compiler
CallGraph 
1 (Type/Class)Agda.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
CallInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callInfoCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callInfosAgda.Termination.Monad
callInfoTargetAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callMainAgda.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
callMatrixSetAgda.Termination.CallGraph
CallPath 
1 (Type/Class)Agda.Termination.Monad
2 (Data Constructor)Agda.Termination.Monad
CallSiteAgda.Utils.CallStack
CallSiteFilterAgda.Utils.CallStack
CallStackAgda.Utils.CallStack
callStackAgda.Utils.CallStack
CALNilAgda.Auto.Syntax
camelTo2Agda.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
CandidateKindAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateKindAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateOverlappableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateTermAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
canHaveSuffixTestAgda.Syntax.Scope.Monad
CannotCreateMissingClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CannotEliminateWithPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CannotResolveAmbiguousPatternSynonymAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CannotTranspAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
canonicalizeAbsolutePathAgda.Utils.FileName
canonicalizeSizeConstraintAgda.TypeChecking.SizedTypes.Solve
canonicalNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
canProjectAgda.TypeChecking.Substitute
CantGeneralizeOverSortsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CantGeneralizeOverSorts_Agda.Interaction.Options.Warnings
CantInvertAgda.TypeChecking.MetaVars
CantResolveOverloadedConstructorsTargetingSameDatatypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitBlockerAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitConIdxAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitConNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitFailuresAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitGivenIdxAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitTelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cArgUsageAgda.Syntax.Treeless, Agda.Compiler.Backend
CarrierAgda.Utils.Zipper
Case 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.TypeChecking.CompiledClause
3 (Type/Class)Agda.TypeChecking.CompiledClause
CaseContextAgda.Interaction.MakeCase
caseEitherMAgda.Utils.Either
CaseInfo 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
caseLazyAgda.Syntax.Treeless, Agda.Compiler.Backend
caseListAgda.Utils.List
caseListMAgda.Utils.List
caseListTAgda.Utils.ListT
caseMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
caseMaybeM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
CaseSplitAgda.Syntax.Common
caseSplitSearchAgda.Auto.CaseSplit
caseSplitSearch'Agda.Auto.CaseSplit
caseToSeqAgda.Compiler.Treeless.Uncase
CaseTypeAgda.Syntax.Treeless, Agda.Compiler.Backend
caseTypeAgda.Syntax.Treeless, Agda.Compiler.Backend
castConstraintToCurrentContextAgda.TypeChecking.SizedTypes.Solve
castConstraintToCurrentContext'Agda.TypeChecking.SizedTypes.Solve
catAgda.Utils.Pretty
CatchallAgda.Syntax.Concrete.Definitions.Types
catchAllAgda.TypeChecking.CompiledClause
catchAllBranchAgda.TypeChecking.CompiledClause
CatchallClauseAgda.Interaction.Highlighting.Precise
CatchallPragmaAgda.Syntax.Concrete
catchallPragmaAgda.Syntax.Concrete.Definitions.Monad
catchAndPrintImpossibleAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
catchConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
catchError_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
catchIlltypedPatternBlockedOnMetaAgda.TypeChecking.Rules.Term
CatchImpossibleAgda.Utils.Impossible
catchImpossibleAgda.Utils.Impossible
catchImpossibleJustAgda.Utils.Impossible
CatchIOAgda.Utils.IO
catchIOAgda.Utils.IO
catchPatternErrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
categorizedeclAgda.Auto.Syntax
catMaybes 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
3 (Function)Agda.Utils.List1
catMaybesMPAgda.Utils.Monad
CC 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Type/Class)Agda.Compiler.MAlonzo.Compiler
CCContextAgda.Compiler.MAlonzo.Compiler
ccContextAgda.Compiler.MAlonzo.Compiler
CCEnv 
1 (Type/Class)Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor)Agda.Compiler.MAlonzo.Compiler
ccNameSupplyAgda.Compiler.MAlonzo.Compiler
CCTAgda.Compiler.MAlonzo.Compiler
cdcontAgda.Auto.Syntax
cddeffreevarsAgda.Auto.Syntax
cdnameAgda.Auto.Syntax
cdoriginAgda.Auto.Syntax
cdtypeAgda.Auto.Syntax
CErasedAgda.Syntax.Common
CExpAgda.Auto.Syntax
CFullAgda.Syntax.Common
ChangeAgda.Utils.Update
ChangeTAgda.Utils.Update
Char 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
charAgda.Utils.Pretty
chaseDisplayFormsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
checkAbsurdLambdaAgda.TypeChecking.Rules.Term
checkAliasAgda.TypeChecking.Rules.Def
checkApplicationAgda.TypeChecking.Rules.Application
CheckArgsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckArgumentsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkArgumentsAgda.TypeChecking.Rules.Application
checkArguments_Agda.TypeChecking.Rules.Application
checkAxiomAgda.TypeChecking.Rules.Decl
checkAxiom'Agda.TypeChecking.Rules.Decl
CheckClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkClauseAgda.TypeChecking.Rules.Def
checkClauseLHSAgda.TypeChecking.Rules.Def
checkClauseTelescopeBindingsAgda.Syntax.Translation.ReflectedToAbstract
checkCohesionAttributesAgda.Syntax.Translation.ConcreteToAbstract
checkCoinductiveRecordsAgda.TypeChecking.Rules.Decl
checkCompilerPragmasAgda.Compiler.JS.Compiler
CheckConfluenceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConfluenceOfClausesAgda.TypeChecking.Rewriting.Confluence
checkConfluenceOfRulesAgda.TypeChecking.Rewriting.Confluence
CheckConstraintAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckConstructorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConstructorAgda.TypeChecking.Rules.Data
checkConstructorCountAgda.Compiler.MAlonzo.HaskellTypes
CheckConstructorFitsInAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConstructorTypeAgda.Compiler.MAlonzo.Compiler
checkCoverAgda.Compiler.MAlonzo.Compiler
CheckDataDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkDataDefAgda.TypeChecking.Rules.Data
CheckDataSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkDataSortAgda.TypeChecking.Rules.Data
checkDeclAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclCachedAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclsAgda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDisplayPragmaAgda.TypeChecking.Rules.Display
checkDomainAgda.TypeChecking.Rules.Term
checkDontExpandLastAgda.TypeChecking.Rules.Term
CheckDotPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkEarlierThanAgda.TypeChecking.Lock
checkedMainDeclAgda.Compiler.MAlonzo.Primitives
checkedMainDefAgda.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
checkeliminandAgda.Auto.Typecheck
checkEmptyTelAgda.TypeChecking.Empty
CheckExprAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkExprAgda.TypeChecking.Rules.Term, Agda.TheTypeChecker
checkExpr'Agda.TypeChecking.Rules.Term
CheckExprCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkExtendedLambdaAgda.TypeChecking.Rules.Term
checkForImportCycleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
CheckFunDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkFunDefAgda.TypeChecking.Rules.Def
checkFunDef'Agda.TypeChecking.Rules.Def
CheckFunDefCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkFunDefSAgda.TypeChecking.Rules.Def
checkGeneralizeAgda.TypeChecking.Rules.Decl
checkGeneralizeTelescopeAgda.TypeChecking.Rules.Term
CheckIApplyConfluenceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkIApplyConfluenceAgda.TypeChecking.IApplyConfluence
checkIApplyConfluence_Agda.TypeChecking.IApplyConfluence
checkImportAgda.TypeChecking.Rules.Decl
checkIndexSortsAgda.TypeChecking.Rules.Data
checkInjectivityAgda.TypeChecking.Injectivity
checkInjectivity'Agda.TypeChecking.Injectivity
checkInjectivity_Agda.TypeChecking.Rules.Decl
checkInternalAgda.TypeChecking.CheckInternal
checkInternal'Agda.TypeChecking.CheckInternal
checkInternalType'Agda.TypeChecking.CheckInternal
CheckIsEmptyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckKAgda.Compiler.MAlonzo.Misc
checkKnownArgumentAgda.TypeChecking.Rules.Term
checkKnownArgumentsAgda.TypeChecking.Rules.Term
CheckLambdaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLambdaAgda.TypeChecking.Rules.Term
checkLambda'Agda.TypeChecking.Rules.Term
checkLazyMatchAgda.TypeChecking.CompiledClause
checkLeftHandSideAgda.TypeChecking.Rules.LHS
CheckLetBindingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLetBindingAgda.TypeChecking.Rules.Term
checkLetBindingsAgda.TypeChecking.Rules.Term
checkLevelAgda.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
checkLinearityAgda.TypeChecking.MetaVars
checkLiteralAgda.TypeChecking.Rules.Term
CheckLockAgda.Interaction.Base
CheckLockedVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLockedVarsAgda.TypeChecking.Lock
checkLoneSigsAgda.Syntax.Concrete.Definitions.Monad
checkMacroTypeAgda.TypeChecking.Rules.Def
checkMetaAgda.TypeChecking.Rules.Term
CheckMetaInstAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkMetaInstAgda.TypeChecking.MetaVars
CheckMetaSolutionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkModuleArityAgda.TypeChecking.Rules.Decl
checkModuleNameAgda.Interaction.FindFile
checkMutualAgda.TypeChecking.Rules.Decl
checkNamedArgAgda.TypeChecking.Rules.Term
CheckNamedWhereAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkNoFixityInRenamingModuleAgda.Syntax.Scope.Monad
checkNoShadowingAgda.Syntax.Scope.Monad
checkOptsAgda.Interaction.Options
checkOrInferMetaAgda.TypeChecking.Rules.Term
checkOverapplicationAgda.TypeChecking.Injectivity
checkPathAgda.TypeChecking.Rules.Term
CheckPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPatternLinearityAgda.Syntax.Abstract.Pattern
CheckPatternLinearityTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckPatternLinearityValueAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPiDomainAgda.TypeChecking.Rules.Term
checkPiTelescopeAgda.TypeChecking.Rules.Term
checkpointAgda.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
checkpointSubstitutionAgda.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
checkPostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
checkPostponedLambdaAgda.TypeChecking.Rules.Term
checkPostponedLambda0Agda.TypeChecking.Rules.Term
CheckPragmaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPragmaAgda.TypeChecking.Rules.Decl
CheckPrimitiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPrimitiveAgda.TypeChecking.Rules.Decl
CheckProjAppToKnownPrincipalArgAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkProjAppToKnownPrincipalArgAgda.TypeChecking.Rules.Application
CheckProjectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkProjectionLikeness_Agda.TypeChecking.Rules.Decl
checkQuestionMarkAgda.TypeChecking.Rules.Term
CheckRecDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkRecDefAgda.TypeChecking.Rules.Record
checkRecordExpressionAgda.TypeChecking.Rules.Term
checkRecordProjectionsAgda.TypeChecking.Rules.Record
checkRecordUpdateAgda.TypeChecking.Rules.Term
CheckResult 
1 (Type/Class)Agda.Compiler.Backend, Agda.Interaction.Imports
2 (Data Constructor)Agda.Compiler.Backend, Agda.Interaction.Imports
checkRewriteRuleAgda.TypeChecking.Rewriting
CheckRHSAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkRHSAgda.TypeChecking.Rules.Def
checkSectionAgda.TypeChecking.Rules.Decl
CheckSectionApplicationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkSectionApplicationAgda.TypeChecking.Rules.Decl
checkSectionApplication'Agda.TypeChecking.Rules.Decl
checkSigAgda.TypeChecking.Rules.Decl
CheckSizeLtSatAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkSizeLtSatAgda.TypeChecking.SizedTypes
checkSizeNeverZeroAgda.TypeChecking.SizedTypes
checkSizeVarNeverZeroAgda.TypeChecking.SizedTypes
checkSolutionForMetaAgda.TypeChecking.MetaVars
checkSortAgda.TypeChecking.CheckInternal
checkSortOfSplitVarAgda.TypeChecking.Rules.LHS
checkStrictlyPositiveAgda.TypeChecking.Positivity
checkSubtypeIsEqualAgda.TypeChecking.MetaVars
checkSyntacticEqualityAgda.TypeChecking.SyntacticEquality
checkSyntacticEquality'Agda.TypeChecking.SyntacticEquality
checkSystemCoverageAgda.TypeChecking.Rules.Def
checkTacticAttributeAgda.TypeChecking.Rules.Term
CheckTargetTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkTelePiSortAgda.TypeChecking.Sort
checkTelescopeAgda.TypeChecking.Rules.Term
checkTelescope'Agda.TypeChecking.Rules.Term
checkTermination_Agda.TypeChecking.Rules.Decl
CheckTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkTypeAgda.TypeChecking.CheckInternal
checkType'Agda.TypeChecking.CheckInternal
checkTypeCheckingProblemAgda.TypeChecking.Constraints
checkTypedBindingsAgda.TypeChecking.Rules.Term
checkTypeOfMainAgda.Compiler.MAlonzo.Primitives
checkTypeOfMain'Agda.Compiler.MAlonzo.Primitives
checkTypeSignatureAgda.TypeChecking.Rules.Decl
checkTypeSignature'Agda.TypeChecking.Rules.Decl
checkUnderscoreAgda.TypeChecking.Rules.Term
checkUnquoteDeclAgda.TypeChecking.Rules.Decl
checkUnquoteDefAgda.TypeChecking.Rules.Decl
checkWhereAgda.TypeChecking.Rules.Def
checkWithFunctionAgda.TypeChecking.Rules.Def
CheckWithFunctionTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkWithRHSAgda.TypeChecking.Rules.Def
ChoiceAgda.Auto.NarrowingSearch
choiceAgda.TypeChecking.Unquote
choicePAgda.Utils.Parser.MemoisedCPS
chooseAgda.Auto.NarrowingSearch
ChooseEitherAgda.TypeChecking.Rules.LHS.Problem
ChooseFlexAgda.TypeChecking.Rules.LHS.Problem
chooseFlexAgda.TypeChecking.Rules.LHS.Problem
chooseHighlightingMethodAgda.Interaction.Highlighting.Common
ChooseLeftAgda.TypeChecking.Rules.LHS.Problem
choosePrioMetaAgda.Auto.NarrowingSearch
ChooseRightAgda.TypeChecking.Rules.LHS.Problem
chopAgda.Utils.List
chopWhenAgda.Utils.List
ChrAgda.Utils.Pretty
Cl 
1 (Type/Class)Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor)Agda.TypeChecking.CompiledClause.Compile
clAgda.TypeChecking.Names
cl'Agda.TypeChecking.Names
ClashesViaRenamingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashesViaRenaming_Agda.Interaction.Options.Warnings
ClashingDefinitionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingFileNamesForAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingModuleImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
classifyForeignAgda.Compiler.MAlonzo.Pragmas
classifyPragmaAgda.Compiler.MAlonzo.Pragmas
classifyWarningAgda.TypeChecking.Warnings
classifyWarningsAgda.TypeChecking.Warnings
Clause 
1 (Type/Class)Agda.Auto.Syntax
2 (Type/Class)Agda.Syntax.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
clauseArgsAgda.Syntax.Internal.Pattern
clauseBodyAgda.Syntax.Internal
clauseCatchall 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Abstract
clauseElimsAgda.Syntax.Internal.Pattern
clauseEllipsisAgda.Syntax.Internal
clauseExactAgda.Syntax.Internal
clauseFullRangeAgda.Syntax.Internal
clauseLHSAgda.Syntax.Abstract
clauseLHSRangeAgda.Syntax.Internal
clausePats 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Reflected
clausePermAgda.Syntax.Internal.Pattern
clauseQNameAgda.TypeChecking.Rewriting.Clause
clauseRecursiveAgda.Syntax.Internal
clauseRHS 
1 (Function)Agda.Syntax.Reflected
2 (Function)Agda.Syntax.Abstract
ClauseSAgda.Syntax.Abstract
ClauseSpineAgda.Syntax.Abstract
clauseSpineAgda.Syntax.Abstract
ClausesPostChecksAgda.TypeChecking.Rules.Def
clauseStrippedPatsAgda.Syntax.Abstract
clauseTel 
1 (Function)Agda.Syntax.Internal
2 (Function)Agda.Syntax.Reflected
clauseToRewriteRuleAgda.TypeChecking.Rewriting.Clause
clauseToSplitClauseAgda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause
clauseTypeAgda.Syntax.Internal
clauseUnreachableAgda.Syntax.Internal
clauseWhereDeclsAgda.Syntax.Abstract
clauseWhereModuleAgda.Syntax.Internal
ClauseZipperAgda.Interaction.MakeCase
clBodyAgda.TypeChecking.CompiledClause.Compile
CleanAgda.TypeChecking.Unquote
cleanAgda.Utils.Graph.AdjacencyMap.Unidirectional
cleanCachedLogAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
clearAnonInstanceDefsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clearMetaListenersAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
clearRunningInfoAgda.Interaction.EmacsCommand
clearWarningAgda.Interaction.EmacsCommand
clEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClockTimeAgda.Utils.Time
Clos 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
closedAgda.TypeChecking.Free
ClosedLevelAgda.Syntax.Internal
closedTermAgda.Compiler.MAlonzo.Compiler
closedTermToTreelessAgda.Compiler.ToTreeless
closedTerm_Agda.Compiler.MAlonzo.Compiler
ClosedTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
closeVerboseBracketAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
closeVerboseBracketExceptionAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
closifyAgda.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
clPatsAgda.TypeChecking.CompiledClause.Compile
ClsAgda.TypeChecking.CompiledClause.Compile
clScopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clSignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clusterAgda.Utils.Cluster
cluster'Agda.Utils.Cluster
clValueAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Cmd_abortAgda.Interaction.Base
Cmd_autoAllAgda.Interaction.Base
Cmd_autoOneAgda.Interaction.Base
Cmd_compileAgda.Interaction.Base
Cmd_computeAgda.Interaction.Base
Cmd_compute_toplevelAgda.Interaction.Base
Cmd_constraintsAgda.Interaction.Base
Cmd_contextAgda.Interaction.Base
Cmd_elaborate_giveAgda.Interaction.Base
Cmd_exitAgda.Interaction.Base
Cmd_giveAgda.Interaction.Base
Cmd_goal_typeAgda.Interaction.Base
Cmd_goal_type_contextAgda.Interaction.Base
cmd_goal_type_context_andAgda.Interaction.InteractionTop
Cmd_goal_type_context_checkAgda.Interaction.Base
Cmd_goal_type_context_inferAgda.Interaction.Base
Cmd_helper_functionAgda.Interaction.Base
Cmd_highlightAgda.Interaction.Base
Cmd_inferAgda.Interaction.Base
Cmd_infer_toplevelAgda.Interaction.Base
Cmd_introAgda.Interaction.Base
Cmd_loadAgda.Interaction.Base
cmd_load'Agda.Interaction.InteractionTop
Cmd_load_highlighting_infoAgda.Interaction.Base
Cmd_make_caseAgda.Interaction.Base
Cmd_metasAgda.Interaction.Base
Cmd_no_metasAgda.Interaction.Base
Cmd_refineAgda.Interaction.Base
Cmd_refine_or_introAgda.Interaction.Base
Cmd_search_about_toplevelAgda.Interaction.Base
Cmd_show_module_contentsAgda.Interaction.Base
Cmd_show_module_contents_toplevelAgda.Interaction.Base
Cmd_show_versionAgda.Interaction.Base
Cmd_solveAllAgda.Interaction.Base
Cmd_solveOneAgda.Interaction.Base
Cmd_tokenHighlightingAgda.Interaction.Base
Cmd_why_in_scopeAgda.Interaction.Base
Cmd_why_in_scope_toplevelAgda.Interaction.Base
CMFBlockedAgda.Auto.Typecheck
CMFFlexAgda.Auto.Typecheck
CMFlex 
1 (Type/Class)Agda.Auto.Typecheck
2 (Data Constructor)Agda.Auto.Typecheck
CMFSemiAgda.Auto.Typecheck
CModeAgda.Auto.Typecheck
CmpAgda.TypeChecking.SizedTypes.Syntax
cmpAgda.TypeChecking.SizedTypes.Syntax
CmpElimAgda.Interaction.Base
CmpEqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CmpInTypeAgda.Interaction.Base
CmpLeqAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CmpLevelsAgda.Interaction.Base
CmpSortsAgda.Interaction.Base
CmpTelesAgda.Interaction.Base
CmpTypesAgda.Interaction.Base
CMRigidAgda.Auto.Typecheck
CMSet 
1 (Type/Class)Agda.Termination.CallMatrix
2 (Data Constructor)Agda.Termination.CallMatrix
cmSetAgda.Termination.CallMatrix
CoConNameAgda.Syntax.Scope.Base
CodeAgda.Syntax.Parser.Literate
codeAgda.Syntax.Parser.Lexer
CoDomainAgda.Utils.TypeLevel
CoDomain'Agda.Utils.TypeLevel
coerceAgda.TypeChecking.Conversion
coerceAppViewAgda.Syntax.Treeless, Agda.Compiler.Backend
coerceSizeAgda.TypeChecking.Conversion
coerceViewAgda.Syntax.Treeless, Agda.Compiler.Backend
CohesionAgda.Syntax.Common
CohesionAttributeAgda.Syntax.Concrete.Attribute
CohesionAttributesAgda.Syntax.Concrete.Attribute
cohesionAttributeTableAgda.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
coinductionKitAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
coinductionKit'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
CoInductiveAgda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoinfectiveAgda.Interaction.Options
CoInfectiveImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoInfectiveImport_Agda.Interaction.Options.Warnings
colAgda.Termination.SparseMatrix
coldescrAgda.Utils.Warshall
collapseDefaultAgda.Utils.WithDefault
collapseOAgda.Termination.Order
CollectionAgda.Utils.Singleton
collectStatsAgda.TypeChecking.Serialise.Base
colon 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
colsAgda.Termination.SparseMatrix
ColumnAgda.Syntax.Parser.Monad
combineHashesAgda.Utils.Hash
combineSysAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
combineSys'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
comma 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
Command 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
3 (Type/Class)Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
Command'Agda.Interaction.Base
CommandErrorAgda.Interaction.ExitCode
commandLineFlagsAgda.Compiler.Backend
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CommandMAgda.Interaction.Base
commandMToIOAgda.Interaction.InteractionTop
CommandQueue 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
commandQueueAgda.Interaction.Base
commandsAgda.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
commitInfoAgda.VersionCommit
commonParentModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
commonPredsAgda.TypeChecking.SizedTypes.WarshallSolver
commonPrefixAgda.Utils.List
commonSuccsAgda.TypeChecking.SizedTypes.WarshallSolver
commonSuffixAgda.Utils.List
comp'Agda.Auto.Typecheck
CompactionAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compactPAgda.Utils.Permutation
ComparableAgda.Utils.PartialOrd
comparableAgda.Utils.PartialOrd
comparableOrdAgda.Utils.PartialOrd
CompareAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compareArgsAgda.TypeChecking.Conversion
CompareAsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compareAsAgda.TypeChecking.Conversion
compareAs'Agda.TypeChecking.Conversion
compareAsDirAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareAtomDirAgda.TypeChecking.Conversion
compareBelowMaxAgda.TypeChecking.SizedTypes
CompareDirectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compareDomAgda.TypeChecking.Conversion
compareElimsAgda.TypeChecking.Conversion
compareFavoritesAgda.Utils.Favorites
compareIntervalAgda.TypeChecking.Conversion
compareIrrelevantAgda.TypeChecking.Conversion
compareLevelAgda.TypeChecking.Conversion
compareMaxViewsAgda.TypeChecking.SizedTypes
compareMetasAgda.TypeChecking.Conversion
compareOffsetAgda.TypeChecking.SizedTypes.Syntax
CompareResultAgda.Utils.Favorites
compareSizesAgda.TypeChecking.SizedTypes
compareSizeViewsAgda.TypeChecking.SizedTypes
compareSortAgda.TypeChecking.Conversion
compareTermAgda.TypeChecking.Conversion
compareTerm'Agda.TypeChecking.Conversion
compareTermOnFaceAgda.TypeChecking.Conversion
compareTermOnFace'Agda.TypeChecking.Conversion
compareTypeAgda.TypeChecking.Conversion
compareWithFavoritesAgda.Utils.Favorites
compareWithPolAgda.TypeChecking.Conversion
ComparisonAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CompilationErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compileAgda.TypeChecking.CompiledClause.Compile
compileAltAgda.Compiler.JS.Compiler
compileClausesAgda.TypeChecking.CompiledClause.Compile
compileClauses'Agda.TypeChecking.CompiledClause.Compile
Compiled 
1 (Type/Class)Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor)Agda.Syntax.Treeless, Agda.Compiler.Backend
compiledClauseBodyAgda.TypeChecking.Substitute
CompiledClausesAgda.TypeChecking.CompiledClause
CompiledClauses'Agda.TypeChecking.CompiledClause
compiledcondeclAgda.Compiler.MAlonzo.Compiler
compileDefAgda.Compiler.Backend
compileDirAgda.Compiler.Common
CompiledRepresentationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compiledTypeSynonymAgda.Compiler.MAlonzo.Compiler
CompilePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compilePrim 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
CompilerBackendAgda.Interaction.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
compileTermAgda.Compiler.JS.Compiler
compileWithSplitTreeAgda.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 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.SmallSet
complete 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.Termination.CallGraph
completeIterAgda.Utils.Graph.AdjacencyMap.Unidirectional
completionStepAgda.Termination.CallGraph
composeAgda.TypeChecking.SizedTypes.Utils
composeCohesionAgda.Syntax.Common
composeErasedAgda.Syntax.Common
composeFlexRigAgda.TypeChecking.Free.Lazy
composeModalityAgda.Syntax.Common
composePAgda.Utils.Permutation
composePolAgda.TypeChecking.Polarity
composeQuantityAgda.Syntax.Common
composeRelevanceAgda.Syntax.Common
composeRetractAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
composeSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
composeVarOccAgda.TypeChecking.Free.Lazy
composeWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
ComposeZipAgda.Utils.Zipper
ComposeZipperAgda.Utils.Zipper
CompressAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
computeEdgesAgda.TypeChecking.Positivity
computeElimHeadTypeAgda.TypeChecking.Conversion
computeErasedConstructorArgsAgda.Compiler.Treeless.Erase
computeFixitiesAndPolaritiesAgda.Syntax.Scope.Monad
computeForcingAnnotationsAgda.TypeChecking.Forcing
computeIgnoreAbstractAgda.Interaction.BasicOps
ComputeModeAgda.Interaction.Base
computeNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
ComputeOccurrencesAgda.TypeChecking.Positivity
computeOccurrencesAgda.TypeChecking.Positivity
computeOccurrences'Agda.TypeChecking.Positivity
computePolarityAgda.TypeChecking.Polarity
computeSizeConstraintAgda.TypeChecking.SizedTypes.Solve
computeUnsolvedInfoAgda.Interaction.Highlighting.Generate
computeWrapInputAgda.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
conAbstrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conAppAgda.TypeChecking.Substitute
conArgsAgda.TypeChecking.MetaVars.Occurs
ConArgTypeAgda.TypeChecking.Positivity.Occurrence
conArityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conBranchesAgda.TypeChecking.CompiledClause
conCaseAgda.TypeChecking.CompiledClause
ConcatAgda.TypeChecking.Positivity
concatAgda.Utils.List1
Concat'Agda.TypeChecking.Positivity
concatargsAgda.Auto.CaseSplit
concatListTAgda.Utils.ListT
conCompAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConcreteNamesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
concreteNamesInScopeAgda.Syntax.Scope.Base
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract
conDataAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conDataRecordAgda.Syntax.Internal
ConDecl 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Utils.Haskell.Syntax
condeclAgda.Compiler.MAlonzo.Compiler
ConditionAgda.TypeChecking.MetaVars
conErasedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conFieldsAgda.Syntax.Internal
configAgdaLibFilesAgda.Interaction.Library.Base, Agda.Interaction.Library
configRootAgda.Interaction.Library.Base, Agda.Interaction.Library
ConfirmedAgda.Syntax.Parser.Monad
confirmLayoutAgda.Syntax.Parser.Layout
ConflictAgda.TypeChecking.Rules.LHS.Unify.Types
conflictAtAgda.TypeChecking.Rules.LHS.Unify.Types
conflictDatatypeAgda.TypeChecking.Rules.LHS.Unify.Types
conflictLeftAgda.TypeChecking.Rules.LHS.Unify.Types
conflictParametersAgda.TypeChecking.Rules.LHS.Unify.Types
conflictRightAgda.TypeChecking.Rules.LHS.Unify.Types
conflictTypeAgda.TypeChecking.Rules.LHS.Unify.Types
ConfluenceCheckAgda.Interaction.Options
ConfluenceProblemAgda.Interaction.Highlighting.Precise
conForcedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConGraphAgda.TypeChecking.SizedTypes.WarshallSolver
ConGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
ConHead 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
conhqnAgda.Compiler.MAlonzo.Misc
conidView'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
conIndAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conInductiveAgda.Syntax.Internal
ConInfoAgda.Syntax.Internal
ConInsteadOfDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConjAgda.TypeChecking.Conversion
ConKAgda.Compiler.MAlonzo.Misc
conKindOfNameAgda.Syntax.Scope.Base
conKindOfName'Agda.Syntax.Scope.Base
ConNameAgda.Syntax.Scope.Base
conNameAgda.Syntax.Internal
ConnectHandleAgda.Auto.NarrowingSearch
connectInteractionPointAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
ConOConAgda.Syntax.Common
ConOfAbsAgda.Syntax.Translation.AbstractToConcrete
ConORecAgda.Syntax.Common
ConOriginAgda.Syntax.Common
ConOSplitAgda.Syntax.Common
ConOSystemAgda.Syntax.Common
ConP 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Reflected
3 (Data Constructor)Agda.Syntax.Abstract
conParsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConPatEagerAgda.Syntax.Info
ConPatInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
conPatInfoAgda.Syntax.Info
ConPatLazy 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
conPatLazyAgda.Syntax.Info
conPatOriginAgda.Syntax.Info
ConPatternInfo 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
conPFallThroughAgda.Syntax.Internal
conPInfoAgda.Syntax.Internal
conPLazyAgda.Syntax.Internal
conPRecordAgda.Syntax.Internal
conProjAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conPTypeAgda.Syntax.Internal
Cons 
1 (Data Constructor)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Interaction.EmacsCommand
cons 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
consecutiveAndSeparatedAgda.Syntax.Position
ConsHeadAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
consListTAgda.Utils.ListT
ConsMap0Agda.Utils.TypeLevel
ConsMap1Agda.Utils.TypeLevel
consMListTAgda.Utils.ListT
consOfHITAgda.TypeChecking.Datatypes
conSrcConAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
consSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Const 
1 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
ConstantAgda.Utils.TypeLevel
Constant0Agda.Utils.TypeLevel
Constant1Agda.Utils.TypeLevel
ConstDef 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
Constr 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
constrainedPrimsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
Constraint 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
3 (Type/Class)Agda.TypeChecking.SizedTypes.Syntax
4 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax
Constraint'Agda.TypeChecking.SizedTypes.Syntax
constraintGraphAgda.TypeChecking.SizedTypes.WarshallSolver
constraintGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
constraintMetasAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
constraintProblemsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Constraints 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Type/Class)Agda.Utils.Warshall
3 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConstraintStatusAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
constraintUnblockerAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConstRefAgda.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
ConstructorBlockAgda.Syntax.Concrete.Definitions.Types
constructorCoverageCodeAgda.Compiler.MAlonzo.Compiler
ConstructorData 
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
ConstructorDefnAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
constructorImpossibleAgda.Auto.Typecheck
ConstructorInfoAgda.TypeChecking.Datatypes
ConstructorNameAgda.Syntax.Scope.Base
ConstructorPatternInWrongDatatypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
constructorTagModifierAgda.Interaction.JSON
ConstructorTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
constructPatsAgda.Auto.Convert
constructsAgda.TypeChecking.Rules.Data
constTranspAxiomAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
containsAbsurdPatternAgda.Syntax.Abstract.Pattern
containsAPatternAgda.Syntax.Abstract.Pattern
containsAsPatternAgda.Syntax.Abstract.Pattern
containsProfileOptionAgda.Utils.ProfileOptions
contains_constructorAgda.Auto.Convert
contentAgda.TypeChecking.CompiledClause
contentsFieldNameAgda.Interaction.JSON
ContentWithoutFieldAgda.Interaction.Library.Base
ContextAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ContextEntryAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ContextLetAgda.Interaction.Base
contextOfMetaAgda.Interaction.BasicOps
contextSizeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
ContextVarAgda.Interaction.Base
ContinuousAgda.Syntax.Common
continuousAgda.Syntax.Position
continuousPerLineAgda.Syntax.Position
ContravariantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conUseSizeLtAgda.Termination.Monad
convErrorAgda.TypeChecking.Conversion
Conversion 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Type/Class)Agda.Auto.Convert
ConvertAgda.Interaction.Highlighting.Precise
convert 
1 (Function)Agda.Interaction.Highlighting.Precise
2 (Function)Agda.Auto.Convert
convertGuardsAgda.Compiler.Treeless.GuardsToPrims
CopatternMatchingAgda.Syntax.Common
CopatternMatchingAllowedAgda.Syntax.Common
copatternMatchingAllowedAgda.Syntax.Common
CopatternReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
copyargAgda.Auto.Typecheck
copyDirContentAgda.Utils.IO.Directory
copyRTEModulesAgda.Compiler.MAlonzo.Compiler
copyScopeAgda.Syntax.Scope.Monad
copyTermAgda.Syntax.Internal.Generic
CosplitCatchallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CosplitNoRecordTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CosplitNoTargetAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Cost 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
costAbsurdLamAgda.Auto.SearchControl
costAddVarDepthAgda.Auto.CaseSplit
costAppConstructorAgda.Auto.SearchControl
costAppConstructorSingleAgda.Auto.SearchControl
costAppExtraRefAgda.Auto.SearchControl
costAppHintAgda.Auto.SearchControl
costAppHintUsedAgda.Auto.SearchControl
costAppRecCallAgda.Auto.SearchControl
costAppRecCallUsedAgda.Auto.SearchControl
costAppVarAgda.Auto.SearchControl
costAppVarUsedAgda.Auto.SearchControl
costCaseSplitHighAgda.Auto.CaseSplit
costCaseSplitLowAgda.Auto.CaseSplit
costCaseSplitVeryHighAgda.Auto.CaseSplit
costEqCongAgda.Auto.SearchControl
costEqEndAgda.Auto.SearchControl
costEqStepAgda.Auto.SearchControl
costEqSymAgda.Auto.SearchControl
costIncreaseAgda.Auto.SearchControl
costInferredTypeUnkownAgda.Auto.SearchControl
costIotaStepAgda.Auto.SearchControl
costLamAgda.Auto.SearchControl
costLamUnfoldAgda.Auto.SearchControl
costPiAgda.Auto.SearchControl
costSortAgda.Auto.SearchControl
costUnificationAgda.Auto.SearchControl
costUnificationIfAgda.Auto.SearchControl
costUnificationOccursAgda.Auto.SearchControl
countAgda.Utils.Bag
CountPatternVarsAgda.Syntax.Internal.Pattern
countPatternVarsAgda.Syntax.Internal.Pattern
countWithArgsAgda.TypeChecking.With
CovariantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoverageAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
CoverageCheckAgda.Syntax.Common
coverageCheck 
1 (Function)Agda.Syntax.Concrete.Definitions.Types
2 (Function)Agda.TypeChecking.Coverage
coverageCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
CoverageIssueAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoverageIssue_Agda.Interaction.Options.Warnings
CoverageNoExactSplitAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoverageNoExactSplit_Agda.Interaction.Options.Warnings
CoverageProblemAgda.Interaction.Highlighting.Precise
Covering 
1 (Type/Class)Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause
2 (Data Constructor)Agda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause
coveringRangeAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
CoverKAgda.Compiler.MAlonzo.Misc
coverMissingClausesAgda.TypeChecking.Coverage.SplitClause
coverNoExactClausesAgda.TypeChecking.Coverage.SplitClause
coverPatternsAgda.TypeChecking.Coverage.SplitClause
CoverResult 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitClause
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitClause
coverSplitTreeAgda.TypeChecking.Coverage.SplitClause
coverUsedClausesAgda.TypeChecking.Coverage.SplitClause
covFillTeleAgda.TypeChecking.Coverage.Cubical
covSplitArgAgda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause
covSplitClausesAgda.TypeChecking.Coverage, Agda.TypeChecking.Coverage.SplitClause
CPatternLikeAgda.Syntax.Concrete.Pattern
CPCAgda.TypeChecking.Rules.Def
cpcPartialSplitsAgda.TypeChecking.Rules.Def
CPUTime 
1 (Type/Class)Agda.Utils.Time
2 (Data Constructor)Agda.Utils.Time
createMetaInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
createMetaInfo'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
createMissingConIdClauseAgda.TypeChecking.Coverage.Cubical
createMissingHCompClauseAgda.TypeChecking.Coverage.Cubical
createMissingIndexedClausesAgda.TypeChecking.Coverage.Cubical
createMissingTrXConClauseAgda.TypeChecking.Coverage.Cubical
createMissingTrXHCompClauseAgda.TypeChecking.Coverage.Cubical
createMissingTrXTrXClauseAgda.TypeChecking.Coverage.Cubical
createModuleAgda.Syntax.Scope.Monad
crInterfaceAgda.Compiler.Backend, Agda.Interaction.Imports
crModeAgda.Compiler.Backend, Agda.Interaction.Imports
crModuleInfoAgda.Interaction.Imports
crSourceAgda.Interaction.Imports
crWarningsAgda.Compiler.Backend, Agda.Interaction.Imports
CSAbsurdAgda.Auto.CaseSplit
CSCtxAgda.Auto.CaseSplit
CSOmittedArgAgda.Auto.CaseSplit
CSPatAgda.Auto.CaseSplit
CSPatConAppAgda.Auto.CaseSplit
CSPatExpAgda.Auto.CaseSplit
CSPatIAgda.Auto.CaseSplit
CSPatProjAgda.Auto.CaseSplit
CSPatVarAgda.Auto.CaseSplit
CSWithAgda.Auto.CaseSplit
CTCharAgda.Syntax.Treeless, Agda.Compiler.Backend
CTDataAgda.Syntax.Treeless, Agda.Compiler.Backend
CTFloatAgda.Syntax.Treeless, Agda.Compiler.Backend
cthandlesAgda.Auto.NarrowingSearch
CTIntAgda.Syntax.Treeless, Agda.Compiler.Backend
CTNatAgda.Syntax.Treeless, Agda.Compiler.Backend
ctparentAgda.Auto.NarrowingSearch
ctpriometaAgda.Auto.NarrowingSearch
CTQNameAgda.Syntax.Treeless, Agda.Compiler.Backend
CTransAgda.TypeChecking.SizedTypes.Syntax
CTree 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Auto.NarrowingSearch
cTreelessAgda.Syntax.Treeless, Agda.Compiler.Backend
CTStringAgda.Syntax.Treeless, Agda.Compiler.Backend
ctsubAgda.Auto.NarrowingSearch
CtxAgda.Auto.Syntax
CTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
Cubical 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Common
cubicalCompatibleOptionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
curAgdaModAgda.Compiler.MAlonzo.Misc
curDefsAgda.Compiler.Common
curHsModAgda.Compiler.MAlonzo.Misc
curIFAgda.Compiler.Common
curIsMainModuleAgda.Compiler.MAlonzo.Misc
curMNameAgda.Compiler.Common
curOutFileAgda.Compiler.MAlonzo.Compiler
curOutFileAndDirAgda.Compiler.MAlonzo.Compiler
CurrentAccountAgda.Utils.Benchmark
currentAccountAgda.Utils.Benchmark
currentCxtAgda.TypeChecking.Names
CurrentFile 
1 (Type/Class)Agda.Interaction.Base
2 (Data Constructor)Agda.Interaction.Base
currentFileArgsAgda.Interaction.Base
currentFileModuleAgda.Interaction.Base
currentFilePathAgda.Interaction.Base
currentFileStampAgda.Interaction.Base
CurrentInputAgda.Syntax.Parser.Alex
currentModuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
currentModuleNameHashAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
currentOrFreshMutualBlockAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
currentTopLevelModuleAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CurrentTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
curriedApplyAgda.Compiler.JS.Substitution
curriedLambdaAgda.Compiler.JS.Substitution
curryAtAgda.TypeChecking.Records
CurryingAgda.Utils.TypeLevel
currysAgda.Utils.TypeLevel
CutOff 
1 (Type/Class)Agda.Termination.CutOff
2 (Data Constructor)Agda.Termination.CutOff
cxtSubstAgda.TypeChecking.Names
CycleAgda.TypeChecking.Rules.LHS.Unify.Types
cycleAgda.Utils.List1
cycleAtAgda.TypeChecking.Rules.LHS.Unify.Types
cycleDatatypeAgda.TypeChecking.Rules.LHS.Unify.Types
cycleOccursInAgda.TypeChecking.Rules.LHS.Unify.Types
cycleParametersAgda.TypeChecking.Rules.LHS.Unify.Types
cycleTypeAgda.TypeChecking.Rules.LHS.Unify.Types
cycleVarAgda.TypeChecking.Rules.LHS.Unify.Types
CyclicModuleDependencyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad