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

Index - C

CAgda.Auto.Options
cacheCurrentLogAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CachedTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cachingStartsAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
callBackendAgda.Compiler.Backend
callByNameAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CallCombAgda.Termination.CallMatrix
callCompilerAgda.Compiler.CallCompiler
callCompiler'Agda.Compiler.CallCompiler
CallGraph 
1 (Type/Class)Agda.Termination.CallGraph
2 (Data Constructor)Agda.Termination.CallGraph
CallInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callInfoCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callInfosAgda.Termination.Monad
callInfoTargetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CandidateKindAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateKindAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateOverlappableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canHaveSuffixTestAgda.Syntax.Scope.Monad
CannotCreateMissingClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotEliminateWithPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotResolveAmbiguousPatternSynonymAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotRewriteByNonEquationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotTranspAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
canonicalizeAbsolutePathAgda.Utils.FileName
canonicalizeSizeConstraintAgda.TypeChecking.SizedTypes.Solve
canonicalNameAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canProjectAgda.TypeChecking.Substitute
CantGeneralizeOverSortsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CantGeneralizeOverSorts_Agda.Interaction.Options.Warnings
CantInvertAgda.TypeChecking.MetaVars
CantResolveOverloadedConstructorsTargetingSameDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitBlockerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConIdxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitFailuresAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitGivenIdxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
caseErasedAgda.Syntax.Treeless, Agda.Compiler.Backend
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.Syntax.Common.Pretty
CatchallAgda.Syntax.Concrete.Definitions.Types
catchAllAgda.TypeChecking.CompiledClause
catchAllBranchAgda.TypeChecking.CompiledClause
CatchallClauseAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
CatchallPragmaAgda.Syntax.Concrete
catchallPragmaAgda.Syntax.Concrete.Definitions.Monad
catchAndPrintImpossibleAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchError_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchIlltypedPatternBlockedOnMetaAgda.TypeChecking.Rules.Term
CatchImpossibleAgda.Utils.Impossible
catchImpossibleAgda.Utils.Impossible
catchImpossibleJustAgda.Utils.Impossible
CatchIOAgda.Utils.IO
catchIOAgda.Utils.IO
catchPatternErrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
categorizedeclAgda.Auto.Syntax
catMaybes 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
3 (Function)Agda.Utils.List1
catMaybesMPAgda.Utils.Monad
CCAgda.TypeChecking.SizedTypes.Solve
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.Syntax.Common.Pretty
chaseDisplayFormsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkAbsurdLambdaAgda.TypeChecking.Rules.Term
checkAliasAgda.TypeChecking.Rules.Def
checkApplicationAgda.TypeChecking.Rules.Application
CheckArgsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckArgumentsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkArgumentsAgda.TypeChecking.Rules.Application
checkArguments_Agda.TypeChecking.Rules.Application
checkAttributesAgda.Syntax.Translation.ConcreteToAbstract
checkAxiomAgda.TypeChecking.Rules.Decl
checkAxiom'Agda.TypeChecking.Rules.Decl
CheckClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkClauseAgda.TypeChecking.Rules.Def
checkClauseLHSAgda.TypeChecking.Rules.Def
checkClauseTelescopeBindingsAgda.Syntax.Translation.ReflectedToAbstract
checkCoinductiveRecordsAgda.TypeChecking.Rules.Decl
checkCompilerPragmasAgda.Compiler.JS.Compiler
CheckConArgFitsInAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckConfluenceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConfluenceOfClausesAgda.TypeChecking.Rewriting.Confluence
checkConfluenceOfRulesAgda.TypeChecking.Rewriting.Confluence
CheckConstraintAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConstructorAgda.TypeChecking.Rules.Data
checkConstructorCountAgda.Compiler.MAlonzo.HaskellTypes
CheckDataDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkDataDefAgda.TypeChecking.Rules.Data
CheckDataSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkeliminandAgda.Auto.Typecheck
checkEmptyTelAgda.TypeChecking.Empty
CheckExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExprAgda.TypeChecking.Rules.Term, Agda.TheTypeChecker
checkExpr'Agda.TypeChecking.Rules.Term
CheckExprCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExtendedLambdaAgda.TypeChecking.Rules.Term
checkForImportCycleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckFunDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDefAgda.TypeChecking.Rules.Def
checkFunDef'Agda.TypeChecking.Rules.Def
CheckFunDefCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDefSAgda.TypeChecking.Rules.Def
checkGeneralizeAgda.TypeChecking.Rules.Decl
checkGeneralizeTelescopeAgda.TypeChecking.Rules.Term
CheckIApplyConfluenceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkIApplyConfluenceAgda.TypeChecking.IApplyConfluence
checkIApplyConfluence_Agda.TypeChecking.IApplyConfluence
checkImportDirectiveAgda.TypeChecking.Rules.Decl
checkIndexSortsAgda.TypeChecking.Rules.Data
checkInjectivityAgda.TypeChecking.Injectivity
checkInjectivity'Agda.TypeChecking.Injectivity
checkInjectivity_Agda.TypeChecking.Rules.Decl
CheckInternalAgda.TypeChecking.CheckInternal
checkInternalAgda.TypeChecking.CheckInternal
checkInternal'Agda.TypeChecking.CheckInternal
CheckIsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckKAgda.Compiler.MAlonzo.Misc
checkKnownArgumentAgda.TypeChecking.Rules.Term
checkKnownArgumentsAgda.TypeChecking.Rules.Term
CheckLambdaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLambdaAgda.TypeChecking.Rules.Term
checkLambda'Agda.TypeChecking.Rules.Term
checkLazyMatchAgda.TypeChecking.CompiledClause
checkLeftHandSideAgda.TypeChecking.Rules.LHS
CheckLetBindingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
checkLibraryFileNotTooFarDownAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLinearityAgda.TypeChecking.MetaVars
checkLiteralAgda.TypeChecking.Rules.Term
CheckLockAgda.Interaction.Base
CheckLockedVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLockedVarsAgda.TypeChecking.Lock
checkLoneSigsAgda.Syntax.Concrete.Definitions.Monad
checkMacroTypeAgda.TypeChecking.Rules.Def
checkMetaAgda.TypeChecking.Rules.Term
CheckMetaInstAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkMetaInstAgda.TypeChecking.MetaVars
CheckMetaSolutionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkModalityAgda.TypeChecking.Modalities
checkModality'Agda.TypeChecking.Modalities
checkModalityArgsAgda.TypeChecking.Modalities
checkModuleArityAgda.TypeChecking.Rules.Decl
checkModuleNameAgda.Interaction.FindFile
CheckModuleParametersAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkMutualAgda.TypeChecking.Rules.Decl
checkNamedArgAgda.TypeChecking.Rules.Term
CheckNamedWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
checkPatternLinearityAgda.Syntax.Abstract.Pattern
CheckPatternLinearityTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckPatternLinearityValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPiDomainAgda.TypeChecking.Rules.Term
checkPiTelescopeAgda.TypeChecking.Rules.Term
checkpointAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckpointId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkpointSubstitutionAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkpointSubstitution'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPositivity_Agda.TypeChecking.Rules.Decl
checkPostponedEquationsAgda.TypeChecking.Rewriting.NonLinMatch
checkPostponedLambdaAgda.TypeChecking.Rules.Term
checkPostponedLambda0Agda.TypeChecking.Rules.Term
CheckPragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPragmaAgda.TypeChecking.Rules.Decl
CheckPrimitiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPrimitiveAgda.TypeChecking.Rules.Decl
CheckProjAppToKnownPrincipalArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjAppToKnownPrincipalArgAgda.TypeChecking.Rules.Application
CheckProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjectionLikeness_Agda.TypeChecking.Rules.Decl
checkQuestionMarkAgda.TypeChecking.Rules.Term
CheckRecDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkRecDefAgda.TypeChecking.Rules.Record
checkRecordExpressionAgda.TypeChecking.Rules.Term
checkRecordProjectionsAgda.TypeChecking.Rules.Record
checkRecordUpdateAgda.TypeChecking.Rules.Term
CheckResult 
1 (Type/Class)Agda.Interaction.Imports, Agda.Compiler.Backend
2 (Data Constructor)Agda.Interaction.Imports, Agda.Compiler.Backend
checkRewriteRuleAgda.TypeChecking.Rewriting
CheckRHSAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkRHSAgda.TypeChecking.Rules.Def
checkSectionAgda.TypeChecking.Rules.Decl
CheckSectionApplicationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSectionApplicationAgda.TypeChecking.Rules.Decl
checkSectionApplication'Agda.TypeChecking.Rules.Decl
checkSigAgda.TypeChecking.Rules.Decl
CheckSizeLtSatAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSizeLtSatAgda.TypeChecking.SizedTypes
checkSizeNeverZeroAgda.TypeChecking.SizedTypes
checkSizeVarNeverZeroAgda.TypeChecking.SizedTypes
checkSolutionForMetaAgda.TypeChecking.MetaVars
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.TypeChecking.Monad, Agda.Compiler.Backend
checkTelePiSortAgda.TypeChecking.Sort
checkTelescopeAgda.TypeChecking.Rules.Term
checkTelescope'Agda.TypeChecking.Rules.Term
checkTermination_Agda.TypeChecking.Rules.Decl
CheckTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkTypeAgda.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.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.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.TypeChecking.Monad, Agda.Compiler.Backend
ClashesViaRenaming_Agda.Interaction.Options.Warnings
ClashingDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingFileNamesForAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModuleImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Internal
3 (Data Constructor)Agda.Syntax.Internal
4 (Type/Class)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Reflected
6 (Type/Class)Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
7 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
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.SplitClause, Agda.TypeChecking.Coverage
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.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearAnonInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearRunningInfoAgda.Interaction.EmacsCommand
clearWarningAgda.Interaction.EmacsCommand
clEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clModuleCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClockTimeAgda.Utils.Time
Clos 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
closedAgda.TypeChecking.Free
ClosedLevelAgda.Syntax.Internal
closedTermToTreelessAgda.Compiler.ToTreeless
ClosedTypeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
closeVerboseBracketAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
closeVerboseBracketExceptionAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
closifyAgda.Auto.Syntax
Closure 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clPatsAgda.TypeChecking.CompiledClause.Compile
ClsAgda.TypeChecking.CompiledClause.Compile
clScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clusterAgda.Utils.Cluster
cluster'Agda.Utils.Cluster
clValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CMaybeAgda.Utils.Singleton
cMaybeAgda.Utils.Singleton
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.TypeChecking.Monad, Agda.Compiler.Backend
CmpInTypeAgda.Interaction.Base
CmpLeqAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
codomainUnivAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
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
cohesionAttributeTableAgda.Syntax.Concrete.Attribute
CoinductionKit 
1 (Type/Class)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKit'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInductiveAgda.Syntax.Common.Aspect, Agda.Syntax.Common
CoinductiveDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoinfectiveAgda.Interaction.Options
CoInfectiveImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty
colsAgda.Termination.SparseMatrix
ColumnAgda.Syntax.Parser.Monad
combineHashesAgda.Utils.Hash
combineSysAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
combineSys'Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
comma 
1 (Function)Agda.Syntax.Common.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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Command'Agda.Interaction.Base
CommandErrorAgda.Interaction.ExitCode
commandLineFlagsAgda.Compiler.Backend
CommandLineOptionsAgda.Interaction.Options
commandLineOptionsAgda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
3 (Data Constructor)Agda.Syntax.Parser.Literate
4 (Type/Class)Agda.Compiler.JS.Syntax
5 (Data Constructor)Agda.Compiler.JS.Syntax
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.TypeChecking.Monad, Agda.Compiler.Backend
compareAsAgda.TypeChecking.Conversion
compareAs'Agda.TypeChecking.Conversion
compareAsDirAgda.TypeChecking.Conversion
compareAtomAgda.TypeChecking.Conversion
compareAtomDirAgda.TypeChecking.Conversion
compareBelowMaxAgda.TypeChecking.SizedTypes
CompareDirectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
CompilationErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
compileDefAgda.Compiler.Backend
compileDirAgda.Compiler.Common
CompiledRepresentationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CompilePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
compilePrimAgda.Compiler.JS.Compiler
CompilerBackendAgda.Interaction.Base
CompilerPragma 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compileTermAgda.Compiler.JS.Compiler
compileWithSplitTreeAgda.TypeChecking.CompiledClause.Compile
CompKit 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
computeDefTypeAgda.TypeChecking.ProjectionLike
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.TypeChecking.Monad, Agda.Compiler.Backend
conAppAgda.TypeChecking.Substitute
conArgsAgda.TypeChecking.MetaVars.Occurs
ConArgTypeAgda.TypeChecking.Positivity.Occurrence
conArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conBranchesAgda.TypeChecking.CompiledClause
conCaseAgda.TypeChecking.CompiledClause
ConcatAgda.TypeChecking.Positivity
concatAgda.Utils.List1
Concat'Agda.TypeChecking.Positivity
concatargsAgda.Auto.CaseSplit
concatListTAgda.Utils.ListT
concatMap1Agda.Utils.List1
concatMapMAgda.Utils.Monad
conCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteDefAgda.Syntax.Common
ConcreteModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
concreteNamesInScopeAgda.Syntax.Scope.Base
concreteToAbstractAgda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_Agda.Syntax.Translation.ConcreteToAbstract
conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conDataRecordAgda.Syntax.Internal
ConDecl 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Utils.Haskell.Syntax
ConditionAgda.TypeChecking.MetaVars
ConEndpointAgda.TypeChecking.Positivity.Occurrence
conErasedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conErasureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conFieldsAgda.Syntax.Internal
configAboveAgda.Interaction.Library.Base, Agda.Interaction.Library
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
conForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conInductiveAgda.Syntax.Internal
ConInfoAgda.Syntax.Internal
conInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConInsteadOfDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
consListTAgda.Utils.ListT
ConsMap0Agda.Utils.TypeLevel
ConsMap1Agda.Utils.TypeLevel
consMListTAgda.Utils.ListT
consOfHITAgda.TypeChecking.Datatypes
conSrcConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraint 
1 (Type/Class)Agda.Utils.Warshall
2 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constraintProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraints 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Type/Class)Agda.Utils.Warshall
3 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstraintStatusAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constraintUnblockerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstRefAgda.Auto.Syntax
Constructor 
1 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Auto.Syntax
3 (Data Constructor)Agda.Syntax.Concrete
4 (Type/Class)Agda.Syntax.Abstract
5 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorBlockAgda.Syntax.Concrete.Definitions.Types
ConstructorData 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorDefnAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorForm 
1 (Function)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.TypeChecking.Reduce.Monad
constructorForm'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorImpossibleAgda.Auto.Typecheck
ConstructorInfoAgda.TypeChecking.Datatypes
ConstructorNameAgda.Syntax.Scope.Base
ConstructorPatternInWrongDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorTagModifierAgda.Interaction.JSON
ConstructorTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructPatsAgda.Auto.Convert
constructsAgda.TypeChecking.Rules.Data
constTranspAxiomAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
containsAgda.Utils.Lens
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.TypeChecking.Monad, Agda.Compiler.Backend
ContextEntryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextLetAgda.Interaction.Base
contextOfMetaAgda.Interaction.BasicOps
contextSizeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextVarAgda.Interaction.Base
ContinuousAgda.Syntax.Common
continuousAgda.Syntax.Position
continuousPerLineAgda.Syntax.Position
ContravariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
copyargAgda.Auto.Typecheck
copyDirContentAgda.Utils.IO.Directory
copyIfChangedAgda.Utils.IO.Directory
copyScopeAgda.Syntax.Scope.Monad
copyTermAgda.Syntax.Internal.Generic
CosplitCatchallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoRecordTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoTargetAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
CoverageIssue_Agda.Interaction.Options.Warnings
CoverageNoExactSplitAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageNoExactSplit_Agda.Interaction.Options.Warnings
CoverageProblemAgda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
Covering 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
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.SplitClause, Agda.TypeChecking.Coverage
covSplitClausesAgda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createMetaInfo'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Interaction.Imports, Agda.Compiler.Backend
crModeAgda.Interaction.Imports, Agda.Compiler.Backend
crModuleInfoAgda.Interaction.Imports
crSourceAgda.Interaction.Imports
crWarningsAgda.Interaction.Imports, Agda.Compiler.Backend
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.Cubical, Agda.TypeChecking.Primitive
Cubical 
1 (Data Constructor)Agda.Syntax.Common
2 (Type/Class)Agda.Syntax.Common
cubicalCompatibleOptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CubicalPrimitiveNotFullyAppliedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
curAgdaModAgda.Compiler.MAlonzo.Misc
curDefsAgda.Compiler.Common
curHsModAgda.Compiler.MAlonzo.Misc
curIFAgda.Compiler.Common
curIsMainModuleAgda.Compiler.MAlonzo.Misc
curMNameAgda.Compiler.Common
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
currentModalityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentModuleAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentModuleNameHashAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentOrFreshMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentTopLevelModuleAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CurrentTypeCheckLogAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend