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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - C

C | Agda.Mimer.Options
cacheCurrentLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CachedTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cachingStarts | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
caConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
caElim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Call |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callBackend | Agda.Compiler.Backend
callBackendInteractHole | Agda.Compiler.Backend
callBackendInteractTop | Agda.Compiler.Backend
callByName | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CallComb | Agda.Termination.CallMatrix
callCompiler | Agda.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
callInfoCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callInfos | Agda.Termination.Monad
callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callMain | Agda.Compiler.JS.Syntax
CallMatrix |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
CallMatrix' | Agda.Termination.CallMatrix
CallMatrixAug |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
callMatrixSet | Agda.Termination.CallGraph
CallPath |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
CallSite |
1 (Type/Class) | Agda.Utils.CallStack
2 (Data Constructor) | Agda.Utils.CallStack
CallSiteFilter | Agda.Utils.CallStack
CallStack | Agda.Utils.CallStack
callStack | Agda.Utils.CallStack
camelTo2 | Agda.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
CandidateKind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateKind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateOverlap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
candidateType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canDropRecursiveInstance | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canHaveSuffixTest | Agda.Syntax.Scope.Monad
CannotApply | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotApply_ | Agda.Interaction.Options.Errors
CannotCreateMissingClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotCreateMissingClause_ | Agda.Interaction.Options.Errors
CannotDeclareHiddenFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotDeclareHiddenFunction_ | Agda.Interaction.Options.Errors
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotEliminateWithPattern_ | Agda.Interaction.Options.Errors
CannotEliminateWithProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotEliminateWithProjection_ | Agda.Interaction.Options.Errors
CannotGenerateHCompClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotGenerateHCompClause_ | Agda.Interaction.Options.Errors
CannotGenerateTransportClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotGenerateTransportClause_ | Agda.Interaction.Options.Errors
CannotGive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotGive_ | Agda.Interaction.Options.Errors
CannotQuote |
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
CannotQuoteAmbiguous | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteAmbiguous_ | Agda.Interaction.Options.Errors
CannotQuoteExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteExpression_ | Agda.Interaction.Options.Errors
CannotQuoteHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteHidden_ | Agda.Interaction.Options.Errors
cannotQuoteNameString | Agda.Interaction.Options.Errors
CannotQuoteNothing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteNothing_ | Agda.Interaction.Options.Errors
CannotQuotePattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuotePattern_ | Agda.Interaction.Options.Errors
CannotQuoteTerm |
1 (Type/Class) | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteTermHidden | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cannotQuoteTermNameString | Agda.Interaction.Options.Errors
CannotQuoteTermNothing | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotQuoteTerm_ | Agda.Interaction.Options.Errors
CannotQuote_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
CannotRefine | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotRefine_ | Agda.Interaction.Options.Errors
CannotResolveAmbiguousPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotResolveAmbiguousPatternSynonym_ | Agda.Interaction.Options.Errors
CannotRewriteByNonEquation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotRewriteByNonEquation_ | Agda.Interaction.Options.Errors
CannotSolveSizeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotSolveSizeConstraints_ | Agda.Interaction.Options.Errors
CannotTransp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
canonicalizeAbsolutePath | Agda.Utils.FileName
canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
canProject | Agda.TypeChecking.Substitute
CantGeneralizeOverSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CantGeneralizeOverSorts_ | Agda.Interaction.Options.Warnings
CantInvert | Agda.TypeChecking.MetaVars
CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CantResolveOverloadedConstructorsTargetingSameDatatype_ | Agda.Interaction.Options.Errors
cantSplitBlocker | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitConName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitFailures | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitGivenIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cantSplitTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
caRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend
Carrier | Agda.Utils.Zipper
cartesianProduct | Agda.Utils.Set1
Case |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.TypeChecking.CompiledClause
3 (Type/Class) | Agda.TypeChecking.CompiledClause
CaseContext | Agda.Interaction.MakeCase
CaseDT | Agda.TypeChecking.DiscrimTree.Types
caseEitherM | Agda.Utils.Either
caseErased | Agda.Syntax.Treeless, Agda.Compiler.Backend
CaseInfo |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseLazy | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseList | Agda.Utils.List
caseListM | Agda.Utils.List
caseListT | Agda.Utils.ListT
caseMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
caseMaybeM |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
CaseSplit | Agda.Syntax.Common
CaseSplitError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CaseSplitError_ | Agda.Interaction.Options.Errors
caseToSeq | Agda.Compiler.Treeless.Uncase
CaseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve
castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve
cat | Agda.Syntax.Common.Pretty
Catchall | Agda.Syntax.Common
catchall | Agda.TypeChecking.CompiledClause
catchallBranch | Agda.TypeChecking.CompiledClause
CatchallClause | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
CatchallPragma | Agda.Syntax.Concrete
catchallPragma | Agda.Syntax.Concrete.Definitions.Monad
catchAndPrintImpossible | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term
CatchImpossible | Agda.Utils.Impossible
catchImpossible | Agda.Utils.Impossible
catchImpossibleJust | Agda.Utils.Impossible
CatchIO | Agda.Utils.IO
catchIO | Agda.Utils.IO
catchNull | Agda.Utils.Null
catchPatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catMaybes |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
3 (Function) | Agda.Utils.List1
catMaybesMP | Agda.Utils.Monad
CCConfig | Agda.Compiler.ToTreeless
CCSubst | Agda.Compiler.ToTreeless
ceName | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CErased | Agda.Syntax.Common
ceType | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CFull | Agda.Syntax.Common
Change | Agda.Utils.Update
ChangeT | Agda.Utils.Update
Char |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
char | Agda.Syntax.Common.Pretty
ChaseDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
chaseDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkAbsurdLambda | Agda.TypeChecking.Rules.Term
checkAlias | Agda.TypeChecking.Rules.Def
checkAndSetOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkApplication | Agda.TypeChecking.Rules.Application
CheckArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkArguments | Agda.TypeChecking.Rules.Application
checkArguments_ | Agda.TypeChecking.Rules.Application
checkAttributes | Agda.Syntax.Translation.ConcreteToAbstract
checkAxiom | Agda.TypeChecking.Rules.Decl
checkAxiom' | Agda.TypeChecking.Rules.Decl
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkClause | Agda.TypeChecking.Rules.Def
checkClauseLHS | Agda.TypeChecking.Rules.Def
checkClauseTelescopeBindings | Agda.Syntax.Translation.ReflectedToAbstract
checkCompilerPragmas | Agda.Compiler.JS.Compiler
CheckConArgFitsIn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckConfluence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConfluenceOfClauses | Agda.TypeChecking.Rewriting.Confluence
checkConfluenceOfRules | Agda.TypeChecking.Rewriting.Confluence
CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConstructor | Agda.TypeChecking.Rules.Data
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkDataDef | Agda.TypeChecking.Rules.Data
CheckDataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkDataSort | Agda.TypeChecking.Rules.Data
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclCached | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDisplayPragma | Agda.TypeChecking.Rules.Display
checkDomain | Agda.TypeChecking.Rules.Term
checkDontExpandLast | Agda.TypeChecking.Rules.Term
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkEarlierThan | Agda.TypeChecking.Lock
CheckedArg |
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
checkedMainDecl | Agda.Compiler.MAlonzo.Primitives
checkedMainDef | Agda.Compiler.MAlonzo.Primitives
CheckedMainFunctionDef |
1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives
2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives
CheckedTarget |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkEmptyTel | Agda.TypeChecking.Empty
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker
checkExpr' | Agda.TypeChecking.Rules.Term
CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkExtendedLambda | Agda.TypeChecking.Rules.Term
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkForUniqueAttribute | Agda.Syntax.Parser.Helpers
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDef | Agda.TypeChecking.Rules.Def
checkFunDef' | Agda.TypeChecking.Rules.Def
CheckFunDefCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkFunDefS | Agda.TypeChecking.Rules.Def
checkGeneralize | Agda.TypeChecking.Rules.Decl
checkGeneralizeTelescope | Agda.TypeChecking.Rules.Term
CheckIApplyConfluence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkIApplyConfluence | Agda.TypeChecking.IApplyConfluence
checkIApplyConfluence_ | Agda.TypeChecking.IApplyConfluence
checkImportDirective | Agda.TypeChecking.Rules.Decl
checkIndexSorts | Agda.TypeChecking.Rules.Data
checkingWhere | Agda.Syntax.Concrete.Definitions.Monad, Agda.Syntax.Concrete.Definitions
checkInjectivity | Agda.TypeChecking.Injectivity
checkInjectivity' | Agda.TypeChecking.Injectivity
checkInjectivity_ | Agda.TypeChecking.Rules.Decl
CheckInternal | Agda.TypeChecking.CheckInternal
checkInternal | Agda.TypeChecking.CheckInternal
checkInternal' | Agda.TypeChecking.CheckInternal
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckK | Agda.Compiler.MAlonzo.Misc
checkKnownArgument | Agda.TypeChecking.Rules.Term
checkKnownArguments | Agda.TypeChecking.Rules.Term
CheckLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLambda | Agda.TypeChecking.Rules.Term
checkLambda' | Agda.TypeChecking.Rules.Term
checkLazyMatch | Agda.TypeChecking.CompiledClause
checkLeftHandSide | Agda.TypeChecking.Rules.LHS
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLetBinding | Agda.TypeChecking.Rules.Term
checkLetBinding' | Agda.TypeChecking.Rules.Term
checkLetBindings | Agda.TypeChecking.Rules.Term
checkLetBindings' | Agda.TypeChecking.Rules.Term
checkLevel | Agda.TypeChecking.Rules.Term
CheckLHS |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLibraryFileNotTooFarDown | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLinearity | Agda.TypeChecking.MetaVars
checkLiteral | Agda.TypeChecking.Rules.Term
CheckLock | Agda.Interaction.Base
CheckLockedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkLockedVars | Agda.TypeChecking.Lock
checkLoneSigs | Agda.Syntax.Concrete.Definitions.Monad
checkMacroType | Agda.TypeChecking.Rules.Def
checkMeta | Agda.TypeChecking.Rules.Term
CheckMetaInst | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkMetaInst | Agda.TypeChecking.MetaVars
CheckMetaSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkModality | Agda.TypeChecking.Modalities
checkModality' | Agda.TypeChecking.Modalities
checkModalityArgs | Agda.TypeChecking.Modalities
checkModuleArity | Agda.TypeChecking.Rules.Decl
checkModuleName | Agda.Interaction.FindFile
CheckModuleParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkMutual | Agda.TypeChecking.Rules.Decl
checkNamedArg | Agda.TypeChecking.Rules.Term
CheckNamedWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkNoFixityInRenamingModule | Agda.Syntax.Scope.Monad
checkNoShadowing | Agda.Syntax.Scope.Monad
checkOpts | Agda.Interaction.Options
checkOrInferMeta | Agda.TypeChecking.Rules.Term
checkOverapplication | Agda.TypeChecking.Injectivity
CheckOverlap | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkPath | Agda.TypeChecking.Rules.Term
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPatternLinearity | Agda.Syntax.Abstract.Pattern
CheckPatternLinearityType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckPatternLinearityValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPiDomain | Agda.TypeChecking.Rules.Term
checkPiTelescope | Agda.TypeChecking.Rules.Term
checkpoint | Agda.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
checkpointSubstitution | Agda.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
checkPostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch
checkPostponedLambda | Agda.TypeChecking.Rules.Term
checkPostponedLambda0 | Agda.TypeChecking.Rules.Term
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPragma | Agda.TypeChecking.Rules.Decl
checkPragmaOptionConsistency | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPrimitive | Agda.TypeChecking.Rules.Decl
CheckProjAppToKnownPrincipalArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjAppToKnownPrincipalArg | Agda.TypeChecking.Rules.Application
CheckProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl
checkQuestionMark | Agda.TypeChecking.Rules.Term
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkRecDef | Agda.TypeChecking.Rules.Record
checkRecordExpression | Agda.TypeChecking.Rules.Term
checkRecordProjections | Agda.TypeChecking.Rules.Record
checkRecordUpdate | Agda.TypeChecking.Rules.Term
CheckResult |
1 (Type/Class) | Agda.Interaction.Imports, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Interaction.Imports, Agda.Compiler.Backend
checkRewriteRule | Agda.TypeChecking.Rewriting
CheckRHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkRHS | Agda.TypeChecking.Rules.Def
checkSection | Agda.TypeChecking.Rules.Decl
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSectionApplication | Agda.TypeChecking.Rules.Decl
checkSectionApplication' | Agda.TypeChecking.Rules.Decl
checkSig | Agda.TypeChecking.Rules.Decl
CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSizeLtSat | Agda.TypeChecking.SizedTypes
checkSizeNeverZero | Agda.TypeChecking.SizedTypes
checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes
checkSolutionForMeta | Agda.TypeChecking.MetaVars
checkSortOfSplitVar | Agda.TypeChecking.Rules.LHS
checkStrictlyPositive | Agda.TypeChecking.Positivity
checkSubtypeIsEqual | Agda.TypeChecking.MetaVars
checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality
checkSyntacticEquality' | Agda.TypeChecking.SyntacticEquality
checkSystemCoverage | Agda.TypeChecking.Rules.Def
checkTacticAttribute | Agda.TypeChecking.Rules.Term
CheckTargetType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkTelePiSort | Agda.TypeChecking.Sort
checkTelescope | Agda.TypeChecking.Rules.Term
checkTelescope' | Agda.TypeChecking.Rules.Term
checkTermination_ | Agda.TypeChecking.Rules.Decl
CheckType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkType | Agda.TypeChecking.CheckInternal
checkTypeCheckingProblem | Agda.TypeChecking.Constraints
checkTypedBindings | Agda.TypeChecking.Rules.Term
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives
checkTypeOfMain' | Agda.Compiler.MAlonzo.Primitives
checkTypeSignature | Agda.TypeChecking.Rules.Decl
checkTypeSignature' | Agda.TypeChecking.Rules.Decl
checkUnderscore | Agda.TypeChecking.Rules.Term
checkUnquoteDecl | Agda.TypeChecking.Rules.Decl
checkUnquoteDef | Agda.TypeChecking.Rules.Decl
checkWhere | Agda.TypeChecking.Rules.Def
checkWithFunction | Agda.TypeChecking.Rules.Def
CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkWithRHS | Agda.TypeChecking.Rules.Def
choice | Agda.TypeChecking.Unquote
choiceP | Agda.Utils.Parser.MemoisedCPS
ChooseEither | Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseHighlightingMethod | Agda.Interaction.Highlighting.Common
ChooseLeft | Agda.TypeChecking.Rules.LHS.Problem
ChooseRight | Agda.TypeChecking.Rules.LHS.Problem
chop | Agda.Utils.List
chopWhen | Agda.Utils.List
Chr | Agda.Syntax.Common.Pretty
Cl |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile
cl | Agda.TypeChecking.Names
cl' | Agda.TypeChecking.Names
ClashesViaRenaming | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashesViaRenaming_ | Agda.Interaction.Options.Warnings
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingDefinition_ | Agda.Interaction.Options.Errors
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModule_ | Agda.Interaction.Options.Errors
classifyBuiltinModule_ | Agda.Interaction.Library
classifyForeign | Agda.Compiler.MAlonzo.Pragmas
classifyPragma | Agda.Compiler.MAlonzo.Pragmas
classifyWarning | Agda.TypeChecking.Warnings
classifyWarnings | Agda.TypeChecking.Warnings
Clause |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Reflected
5 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
6 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
7 (Type/Class) | Agda.Syntax.Abstract
8 (Data Constructor) | Agda.Syntax.Abstract
Clause' | Agda.Syntax.Abstract
clauseArgs | Agda.Syntax.Internal.Pattern
clauseBody | Agda.Syntax.Internal
clauseCatchall |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Abstract
clauseElims | Agda.Syntax.Internal.Pattern
clauseEllipsis | Agda.Syntax.Internal
clauseFullRange | Agda.Syntax.Internal
clauseLHS | Agda.Syntax.Abstract
clauseLHSRange | Agda.Syntax.Internal
clausePats |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Reflected
clausePerm | Agda.Syntax.Internal.Pattern
clauseQName | Agda.TypeChecking.Rewriting.Clause
clauseRecursive | Agda.Syntax.Internal
clauseRHS |
1 (Function) | Agda.Syntax.Reflected
2 (Function) | Agda.Syntax.Abstract
ClauseS | Agda.Syntax.Abstract
ClauseSpine | Agda.Syntax.Abstract
clauseSpine | Agda.Syntax.Abstract
ClausesPostChecks | Agda.TypeChecking.Rules.Def
clauseStrippedPats | Agda.Syntax.Abstract
clauseTel |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Reflected
clauseToRewriteRule | Agda.TypeChecking.Rewriting.Clause
clauseToSplitClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
clauseType | Agda.Syntax.Internal
clauseUnreachable | Agda.Syntax.Internal
clauseWhereDecls | Agda.Syntax.Abstract
clauseWhereModule | Agda.Syntax.Internal
ClauseZipper | Agda.Interaction.MakeCase
clBody | Agda.TypeChecking.CompiledClause.Compile
Clean | Agda.TypeChecking.Unquote
clean | Agda.Utils.Graph.AdjacencyMap.Unidirectional
cleanCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearRunningInfo | Agda.Interaction.EmacsCommand
clearUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearWarning | Agda.Interaction.EmacsCommand
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClockTime | Agda.Utils.Time
closed | Agda.TypeChecking.Free
ClosedLevel | Agda.Syntax.Internal
closedTermToTreeless | Agda.Compiler.ToTreeless
ClosedType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
closeVerboseBracket | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
closeVerboseBracketException | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
clPats | Agda.TypeChecking.CompiledClause.Compile
Cls | Agda.TypeChecking.CompiledClause.Compile
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cluster | Agda.Utils.Cluster
cluster' | Agda.Utils.Cluster
cluster1 | Agda.Utils.Cluster
cluster1' | Agda.Utils.Cluster
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CMaybe | Agda.Utils.Singleton
cMaybe | Agda.Utils.Singleton
Cmd_abort | Agda.Interaction.Base
Cmd_autoAll | Agda.Interaction.Base
Cmd_autoOne | Agda.Interaction.Base
Cmd_backend_hole | Agda.Interaction.Base
Cmd_backend_top | Agda.Interaction.Base
Cmd_compile | Agda.Interaction.Base
Cmd_compute | Agda.Interaction.Base
Cmd_compute_toplevel | Agda.Interaction.Base
Cmd_constraints | Agda.Interaction.Base
Cmd_context | Agda.Interaction.Base
Cmd_elaborate_give | Agda.Interaction.Base
Cmd_exit | Agda.Interaction.Base
Cmd_give | Agda.Interaction.Base
Cmd_goal_type | Agda.Interaction.Base
Cmd_goal_type_context | Agda.Interaction.Base
cmd_goal_type_context_and | Agda.Interaction.InteractionTop
Cmd_goal_type_context_check | Agda.Interaction.Base
Cmd_goal_type_context_infer | Agda.Interaction.Base
Cmd_helper_function | Agda.Interaction.Base
Cmd_highlight | Agda.Interaction.Base
Cmd_infer | Agda.Interaction.Base
Cmd_infer_toplevel | Agda.Interaction.Base
Cmd_intro | Agda.Interaction.Base
Cmd_load | Agda.Interaction.Base
cmd_load' | Agda.Interaction.InteractionTop
Cmd_load_highlighting_info | Agda.Interaction.Base
Cmd_load_no_metas | Agda.Interaction.Base
Cmd_make_case | Agda.Interaction.Base
Cmd_metas | Agda.Interaction.Base
Cmd_refine | Agda.Interaction.Base
Cmd_refine_or_intro | Agda.Interaction.Base
Cmd_search_about_toplevel | Agda.Interaction.Base
Cmd_show_module_contents | Agda.Interaction.Base
Cmd_show_module_contents_toplevel | Agda.Interaction.Base
Cmd_show_version | Agda.Interaction.Base
Cmd_solveAll | Agda.Interaction.Base
Cmd_solveOne | Agda.Interaction.Base
Cmd_tokenHighlighting | Agda.Interaction.Base
Cmd_why_in_scope | Agda.Interaction.Base
Cmd_why_in_scope_toplevel | Agda.Interaction.Base
Cmp | Agda.TypeChecking.SizedTypes.Syntax
cmp | Agda.TypeChecking.SizedTypes.Syntax
CmpElim | Agda.Interaction.Base
CmpEq | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpInType | Agda.Interaction.Base
CmpLeq | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpLevels | Agda.Interaction.Base
CmpSorts | Agda.Interaction.Base
CmpTeles | Agda.Interaction.Base
CmpTypes | Agda.Interaction.Base
CMSet |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
cmSet | Agda.Termination.CallMatrix
CoConName | Agda.Syntax.Scope.Base
Code | Agda.Syntax.Parser.Literate
code | Agda.Syntax.Parser.Lexer
CoDomain | Agda.Utils.TypeLevel
CoDomain' | Agda.Utils.TypeLevel
codomainUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
coerce | Agda.TypeChecking.Conversion
coerceAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend
coerceSize | Agda.TypeChecking.Conversion
coerceView | Agda.Syntax.Treeless, Agda.Compiler.Backend
Cohesion | Agda.Syntax.Common
CohesionAttribute | Agda.Syntax.Concrete.Attribute
cohesionAttributeTable | Agda.Syntax.Concrete.Attribute
CoinductionKit |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
coinductionKit' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInductive | Agda.Syntax.Common.Aspect, Agda.Syntax.Common
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoinductiveDatatype_ | Agda.Interaction.Options.Errors
CoinductiveEtaRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoinductiveEtaRecord_ | Agda.Interaction.Options.Warnings
Coinfective | Agda.Interaction.Options
CoInfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInfectiveImport_ | Agda.Interaction.Options.Warnings
col | Agda.Termination.SparseMatrix
collapseDefault | Agda.Utils.WithDefault
collapseO | Agda.Termination.Order
Collection | Agda.Utils.Singleton
collectStats | Agda.TypeChecking.Serialise.Base
colon |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
cols | Agda.Termination.SparseMatrix
Column | Agda.Syntax.Parser.Monad
ComatchingDisabledForRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ComatchingDisabledForRecord_ | Agda.Interaction.Options.Errors
combineHashes | Agda.Utils.Hash
combineSys | Agda.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
CommandError | Agda.Interaction.ExitCode
commandLineFlags | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
CommandLineOptions | Agda.Interaction.Options
commandLineOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CommandM | Agda.Interaction.Command
CommandM' | Agda.Interaction.Base
commandMToIO | Agda.Interaction.InteractionTop
CommandPayload | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
CommandQueue |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
commandQueue | Agda.Interaction.Base
commands | Agda.Interaction.Base
CommandState |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
Comment |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (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
CommitAfterDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CommitAfterDef_ | Agda.Interaction.Options.Errors
commitInfo | Agda.VersionCommit
commonParentModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver
commonPrefix | Agda.Utils.List
commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver
commonSuffix | Agda.Utils.List
Compaction | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compactP | Agda.Utils.Permutation
Comparable | Agda.Utils.PartialOrd
comparable | Agda.Utils.PartialOrd
comparableOrd | Agda.Utils.PartialOrd
Compare | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compareArgs | Agda.TypeChecking.Conversion
CompareAs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compareAs | Agda.TypeChecking.Conversion
compareAs' | Agda.TypeChecking.Conversion
compareAsDir | Agda.TypeChecking.Conversion
compareAtom | Agda.TypeChecking.Conversion
compareAtomDir | Agda.TypeChecking.Conversion
compareBelowMax | Agda.TypeChecking.SizedTypes
CompareDirection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compareDom | Agda.TypeChecking.Conversion
compareElims | Agda.TypeChecking.Conversion
compareFavorites | Agda.Utils.Favorites
compareInterval | Agda.TypeChecking.Conversion
compareIrrelevant | Agda.TypeChecking.Conversion
compareLevel | Agda.TypeChecking.Conversion
compareMaxViews | Agda.TypeChecking.SizedTypes
compareMetas | Agda.TypeChecking.Conversion
compareOffset | Agda.TypeChecking.SizedTypes.Syntax
CompareResult | Agda.Utils.Favorites
compareSizes | Agda.TypeChecking.SizedTypes
compareSizeViews | Agda.TypeChecking.SizedTypes
compareSort | Agda.TypeChecking.Conversion
compareTerm | Agda.TypeChecking.Conversion
compareTerm' | Agda.TypeChecking.Conversion
compareTermOnFace | Agda.TypeChecking.Conversion
compareTermOnFace' | Agda.TypeChecking.Conversion
compareType | Agda.TypeChecking.Conversion
compareWithFavorites | Agda.Utils.Favorites
compareWithPol | Agda.TypeChecking.Conversion
Comparison | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CompilationError_ | Agda.Interaction.Options.Errors
compile | Agda.TypeChecking.CompiledClause.Compile
compileAlt | Agda.Compiler.JS.Compiler
compileClauses | Agda.TypeChecking.CompiledClause.Compile
compileClauses' | Agda.TypeChecking.CompiledClause.Compile
Compiled |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
compiledClauseBody | Agda.TypeChecking.Substitute
CompiledClauses | Agda.TypeChecking.CompiledClause
CompiledClauses' | Agda.TypeChecking.CompiledClause
compileDef | Agda.Compiler.Backend.Base, Agda.Compiler.Backend
compileDir | Agda.Compiler.Common
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compileElispFiles | Agda.Setup.EmacsMode
compileFlag | Agda.Setup.EmacsMode
CompilePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compilePrim | Agda.Compiler.JS.Compiler
CompilerBackend | Agda.Interaction.Base
CompilerPass |
1 (Type/Class) | Agda.Compiler.ToTreeless
2 (Data Constructor) | Agda.Compiler.ToTreeless
compilerPass | Agda.Compiler.ToTreeless
compilerPipeline | Agda.Compiler.ToTreeless
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
compileTerm | Agda.Compiler.JS.Compiler
compileWithSplitTree | Agda.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
completeIter | Agda.Utils.Graph.AdjacencyMap.Unidirectional
completionStep | Agda.Termination.CallGraph
compose | Agda.TypeChecking.SizedTypes.Utils
composeCohesion | Agda.Syntax.Common
composeErased | Agda.Syntax.Common
composeFlexRig | Agda.TypeChecking.Free.Lazy
composeModality | Agda.Syntax.Common
composeP | Agda.Utils.Permutation
composePol | Agda.TypeChecking.Polarity
composePolarity | Agda.Syntax.Common
composePolarity' | Agda.Syntax.Common
composeQuantity | Agda.Syntax.Common
composeRelevance | Agda.Syntax.Common
composeRetract | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
composeVarOcc | Agda.TypeChecking.Free.Lazy
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
ComposeZip | Agda.Utils.Zipper
ComposeZipper | Agda.Utils.Zipper
Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
computeDefType | Agda.TypeChecking.ProjectionLike
computeEdges | Agda.TypeChecking.Positivity
computeElimHeadType | Agda.TypeChecking.Conversion
computeErasedConstructorArgs | Agda.Compiler.Treeless.Erase
computeFixitiesAndPolarities | Agda.Syntax.Scope.Monad
computeForcingAnnotations | Agda.TypeChecking.Forcing
computeIgnoreAbstract | Agda.Interaction.BasicOps
ComputeMode | Agda.Interaction.Base
computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
ComputeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences' | Agda.TypeChecking.Positivity
computePolarity | Agda.TypeChecking.Polarity
computeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve
computeUnsolvedInfo | Agda.Interaction.Highlighting.Generate
computeWrapInput | Agda.Interaction.BasicOps
Con |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Abstract
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conApp | Agda.TypeChecking.Substitute
conArgs | Agda.TypeChecking.MetaVars.Occurs
ConArgType | Agda.TypeChecking.Positivity.Occurrence
conArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conBranches | Agda.TypeChecking.CompiledClause
conCase | Agda.TypeChecking.CompiledClause
Concat | Agda.TypeChecking.Positivity
concat | Agda.Utils.List1
Concat' | Agda.TypeChecking.Positivity
concat21 | Agda.Utils.List2
concatListT | Agda.Utils.ListT
concatMap1 | Agda.Utils.List1
concatMapM | Agda.Utils.Monad
conComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteDef | Agda.Syntax.Common
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
concreteNamesInScope | Agda.Syntax.Scope.Base
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conDataRecord | Agda.Syntax.Internal
ConDecl |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
Condition | Agda.TypeChecking.MetaVars
ConEndpoint | Agda.TypeChecking.Positivity.Occurrence
conErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conFields | Agda.Syntax.Internal
configAbove | Agda.Interaction.Library.Base, Agda.Interaction.Library
configAgdaLibFile | Agda.Interaction.Library.Base, Agda.Interaction.Library
configRoot | Agda.Interaction.Library.Base, Agda.Interaction.Library
Confirmed | Agda.Syntax.Parser.Monad
confirmLayout | Agda.Syntax.Parser.Layout
Conflict | Agda.TypeChecking.Rules.LHS.Unify.Types
conflictAt | Agda.TypeChecking.Rules.LHS.Unify.Types
conflictDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types
ConflictingPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConflictingPragmaOptions_ | Agda.Interaction.Options.Warnings
conflictLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
conflictParameters | Agda.TypeChecking.Rules.LHS.Unify.Types
conflictRight | Agda.TypeChecking.Rules.LHS.Unify.Types
conflictType | Agda.TypeChecking.Rules.LHS.Unify.Types
ConfluenceCheck | Agda.Interaction.Options
ConfluenceCheckingIncompleteBecauseOfMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConfluenceCheckingIncompleteBecauseOfMeta_ | Agda.Interaction.Options.Warnings
ConfluenceForCubicalNotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConfluenceForCubicalNotSupported_ | Agda.Interaction.Options.Warnings
ConfluenceProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
conForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConGraph | Agda.TypeChecking.SizedTypes.WarshallSolver
ConGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
ConHead |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
conhqn | Agda.Compiler.MAlonzo.Misc
conInductive | Agda.Syntax.Internal
ConInfo | Agda.Syntax.Internal
conInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConInsteadOfDef_ | Agda.Interaction.Options.Errors
Conj | Agda.TypeChecking.Conversion
ConK | Agda.Compiler.MAlonzo.Misc
conKindOfName | Agda.Syntax.Scope.Base
conKindOfName' | Agda.Syntax.Scope.Base
conLikeNameKinds | Agda.Syntax.Scope.Base
ConName | Agda.Syntax.Scope.Base
conName | Agda.Syntax.Internal
connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConOCon | Agda.Syntax.Common
ConOfAbs | Agda.Syntax.Translation.AbstractToConcrete
ConORec | Agda.Syntax.Common
ConOrigin | Agda.Syntax.Common
ConOSplit | Agda.Syntax.Common
ConOSystem | Agda.Syntax.Common
ConP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Abstract
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConPatEager | Agda.Syntax.Info
ConPatInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
conPatInfo | Agda.Syntax.Info
ConPatLazy |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
conPatLazy | Agda.Syntax.Info
conPatOrigin | Agda.Syntax.Info
ConPatternInfo |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
conPFallThrough | Agda.Syntax.Internal
conPInfo | Agda.Syntax.Internal
conPLazy | Agda.Syntax.Internal
conPRecord | Agda.Syntax.Internal
conProj | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conPType | Agda.Syntax.Internal
Cons |
1 (Data Constructor) | Agda.Utils.IndexedList
2 (Data Constructor) | Agda.Interaction.EmacsCommand
3 (Data Constructor) | Agda.TypeChecking.Serialise.Base
cons |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.List2
consecutiveAndSeparated | Agda.Syntax.Position
ConsHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
consListT | Agda.Utils.ListT
ConsMap0 | Agda.Utils.TypeLevel
ConsMap1 | Agda.Utils.TypeLevel
consMListT | Agda.Utils.ListT
consOfHIT | Agda.TypeChecking.Datatypes
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
consS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Const |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
Constant | Agda.Utils.TypeLevel
Constant0 | Agda.Utils.TypeLevel
Constant1 | Agda.Utils.TypeLevel
ConstK | Agda.TypeChecking.DiscrimTree.Types
Constr |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
constrainedPrims | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraint |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraint' | Agda.TypeChecking.SizedTypes.Syntax
constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver
constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
constraintMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constraintProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Constraints |
1 (Data Constructor) | Agda.Utils.ProfileOptions
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstraintStatus | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constraintUnblocker | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstrOfNonRecord | Agda.Syntax.Scope.Base
Constructor |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorBlock | Agda.Syntax.Concrete.Definitions.Types
ConstructorCountMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorCountMismatch_ | Agda.Interaction.Options.Errors
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
ConstructorDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorDisambiguationData |
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
ConstructorDoesNotFitInData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorDoesNotFitInData_ | Agda.Interaction.Options.Warnings
ConstructorDoesNotTargetGivenType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorDoesNotTargetGivenType_ | Agda.Interaction.Options.Errors
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
ConstructorInfo | Agda.TypeChecking.Datatypes
ConstructorName | Agda.Syntax.Scope.Base
ConstructorNameOfNonRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorNameOfNonRecord_ | Agda.Interaction.Options.Errors
ConstructorOrPatternSynonym | Agda.Syntax.Common
constructorOrPatternSynonymNameString | Agda.Interaction.Options.Errors
ConstructorParametersNotGeneral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstructorPatternInWrongDatatype_ | Agda.Interaction.Options.Errors
constructorTagModifier | Agda.Interaction.JSON
ConstructorType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructs | Agda.TypeChecking.Rules.Data
constTranspAxiom | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contains | Agda.Utils.Lens
containsAbsurdPattern | Agda.Syntax.Abstract.Pattern
containsAPattern | Agda.Syntax.Abstract.Pattern
containsAsPattern | Agda.Syntax.Abstract.Pattern
containsProfileOption | Agda.Utils.ProfileOptions
ContainsUnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
content | Agda.TypeChecking.CompiledClause
contentsFieldName | Agda.Interaction.JSON
ContentWithoutField | Agda.Interaction.Library.Base
Context | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextArgs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextEntry | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextLet | Agda.Interaction.Base
contextNames | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextNames' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextOfMeta | Agda.Interaction.BasicOps
contextSize | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextTerms | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextToTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextVar | Agda.Interaction.Base
contextVars | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextVars' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Continuous | Agda.Syntax.Common
continuous | Agda.Syntax.Position
continuousPerLine | Agda.Syntax.Position
ContradictorySizeConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContradictorySizeConstraint_ | Agda.Interaction.Options.Errors
Contravariant | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conUseSizeLt | Agda.Termination.Monad
convError | Agda.TypeChecking.Conversion
Conversion | Agda.Utils.ProfileOptions
Convert | Agda.Interaction.Highlighting.Precise
convert | Agda.Interaction.Highlighting.Precise
convertGuards | Agda.Compiler.Treeless.GuardsToPrims
CopatternHeadNotProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CopatternHeadNotProjection_ | Agda.Interaction.Options.Errors
CopatternMatching | Agda.Syntax.Common
CopatternMatchingAllowed | Agda.Syntax.Common
copatternMatchingAllowed | Agda.Syntax.Common
CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
copyDirContent | Agda.Utils.IO.Directory
copyIfChanged | Agda.Utils.IO.Directory
copyName | Agda.Syntax.Scope.Monad
copyScope | Agda.Syntax.Scope.Monad
copyTerm | Agda.Syntax.Internal.Generic
CosmeticProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
CosplitCatchall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitCatchall_ | Agda.Interaction.Options.Errors
CosplitNoRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoRecordType_ | Agda.Interaction.Options.Errors
CosplitNoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoTarget_ | Agda.Interaction.Options.Errors
count | Agda.Utils.Bag
CountPatternVars | Agda.Syntax.Internal.Pattern
countPatternVars | Agda.Syntax.Internal.Pattern
countWithArgs | Agda.TypeChecking.With
countWithPats | Agda.TypeChecking.With
Covariant | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
CoverageCheck | Agda.Syntax.Common
coverageCheck |
1 (Function) | Agda.Syntax.Concrete.Definitions.Types
2 (Function) | Agda.TypeChecking.Coverage
coverageCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
CoverageIssue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageIssue_ | Agda.Interaction.Options.Warnings
CoverageNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoverageNoExactSplit_ | Agda.Interaction.Options.Warnings
CoverageProblem | Agda.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
coveringRange | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
CoverK | Agda.Compiler.MAlonzo.Misc
coverMissingClauses | Agda.TypeChecking.Coverage.SplitClause
coverNoExactClauses | Agda.TypeChecking.Coverage.SplitClause
coverPatterns | Agda.TypeChecking.Coverage.SplitClause
CoverResult |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitClause
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitClause
coverSplitTree | Agda.TypeChecking.Coverage.SplitClause
coverUsedClauses | Agda.TypeChecking.Coverage.SplitClause
covFillTele | Agda.TypeChecking.Coverage.Cubical
covSplitArg | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
covSplitClauses | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage
CPatternLike | Agda.Syntax.Concrete.Pattern
CPC | Agda.TypeChecking.Rules.Def
cpcPartialSplits | Agda.TypeChecking.Rules.Def
CPUTime |
1 (Type/Class) | Agda.Utils.Time
2 (Data Constructor) | Agda.Utils.Time
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createMissingHCompClause | Agda.TypeChecking.Coverage.Cubical
createMissingIndexedClauses | Agda.TypeChecking.Coverage.Cubical
createMissingTrXConClause | Agda.TypeChecking.Coverage.Cubical
createMissingTrXHCompClause | Agda.TypeChecking.Coverage.Cubical
createMissingTrXTrXClause | Agda.TypeChecking.Coverage.Cubical
createModule | Agda.Syntax.Scope.Monad
crInterface | Agda.Interaction.Imports, Agda.Compiler.Backend
crMode | Agda.Interaction.Imports, Agda.Compiler.Backend
crModuleInfo | Agda.Interaction.Imports
crSource | Agda.Interaction.Imports
crWarnings | Agda.Interaction.Imports, Agda.Compiler.Backend
CTChar | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTData | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTFloat | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTInt | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTNat | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTQName | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTrans |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver
cTreeless | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTString | Agda.Syntax.Treeless, Agda.Compiler.Backend
ctxEntryDom | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ctxEntryName | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ctxEntryType | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CtxVar | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Cubical |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Common
cubicalCompatibleOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CubicalCompilationNotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CubicalCompilationNotSupported_ | Agda.Interaction.Options.Errors
CubicalNotErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CubicalNotErasure_ | Agda.Interaction.Options.Errors
cubicalOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cubicalOptionString | Agda.Syntax.Common
CubicalPrimitiveNotFullyApplied | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CubicalPrimitiveNotFullyApplied_ | Agda.Interaction.Options.Errors
curAgdaMod | Agda.Compiler.MAlonzo.Misc
curDefs | Agda.Compiler.Common
curHsMod | Agda.Compiler.MAlonzo.Misc
curIF | Agda.Compiler.Common
curIsMainModule | Agda.Compiler.MAlonzo.Misc
curMName | Agda.Compiler.Common
CurrentAccount | Agda.Utils.Benchmark
currentAccount | Agda.Utils.Benchmark
currentCxt | Agda.TypeChecking.Names
CurrentFile |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
currentFileArgs | Agda.Interaction.Base
currentFileModule | Agda.Interaction.Base
currentFilePath | Agda.Interaction.Base
currentFileStamp | Agda.Interaction.Base
CurrentInput | Agda.Syntax.Parser.Alex
currentModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentModuleNameHash | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CurrentTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
curriedApply | Agda.Compiler.JS.Substitution
curriedLambda | Agda.Compiler.JS.Substitution
curryAt | Agda.TypeChecking.Records
Currying | Agda.Utils.TypeLevel
currys | Agda.Utils.TypeLevel
CustomBackendError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CustomBackendError_ | Agda.Interaction.Options.Errors
CustomBackendWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CustomBackendWarning_ | Agda.Interaction.Options.Warnings
CutOff |
1 (Type/Class) | Agda.Termination.CutOff
2 (Data Constructor) | Agda.Termination.CutOff
cxtSubst | Agda.TypeChecking.Names
Cycle | Agda.TypeChecking.Rules.LHS.Unify.Types
cycle | Agda.Utils.List1
cycleAt | Agda.TypeChecking.Rules.LHS.Unify.Types
cycleDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types
cycleOccursIn | Agda.TypeChecking.Rules.LHS.Unify.Types
cycleParameters | Agda.TypeChecking.Rules.LHS.Unify.Types
cycleType | Agda.TypeChecking.Rules.LHS.Unify.Types
cycleVar | Agda.TypeChecking.Rules.LHS.Unify.Types
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CyclicModuleDependency_ | Agda.Interaction.Options.Errors