Agda-2.6.0.1: 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 |
1 (Data Constructor) | Agda.Auto.Options
2 (Type/Class) | Agda.Utils.Cluster
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
CAction | Agda.Auto.Syntax
calc | Agda.Auto.NarrowingSearch
calcEqRState | Agda.Auto.Typecheck
CALConcat | Agda.Auto.Syntax
Call |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
callBackend | 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
callGHC | Agda.Compiler.MAlonzo.Compiler
CallGraph |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
CallInfo |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, 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
callInfoRange | 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
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
CALNil | Agda.Auto.Syntax
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
candidateOverlappable | 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
CannotCreateMissingClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CannotResolveAmbiguousPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
cArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend
Carrier | Agda.Utils.Zipper
Case |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.TypeChecking.CompiledClause
3 (Type/Class) | Agda.TypeChecking.CompiledClause
CaseContext | Agda.Interaction.MakeCase
caseEitherM | Agda.Utils.Either
CaseInfo |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseLazy | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseList | Agda.Utils.List
caseListM | Agda.Utils.List
caseListNe | Agda.Utils.NonemptyList
caseListT | Agda.Utils.ListT
caseMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
caseMaybeM |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
CaseSplit | Agda.Syntax.Common
caseSplitSearch | Agda.Auto.CaseSplit
caseSplitSearch' | Agda.Auto.CaseSplit
caseToSeq | Agda.Compiler.Treeless.Uncase
CaseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve
castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve
cat | Agda.Utils.Pretty
catchAll | Agda.TypeChecking.CompiledClause
catchAllBranch | Agda.TypeChecking.CompiledClause
CatchallClause | Agda.Interaction.Highlighting.Precise
CatchallPragma | Agda.Syntax.Concrete
catchConstraint | Agda.TypeChecking.Constraints
catchError | Agda.Utils.Except
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term
catchImpossible | Agda.Utils.Impossible
CatchIO | Agda.Utils.IO
catchIO | Agda.Utils.IO
categorizedecl | Agda.Auto.Syntax
catMaybes |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
catMaybesMP | Agda.Utils.Monad
CC |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve
2 (Type/Class) | Agda.Compiler.MAlonzo.Compiler
CCContext | Agda.Compiler.MAlonzo.Compiler
ccContext | Agda.Compiler.MAlonzo.Compiler
CCEnv |
1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler
ccNameSupply | Agda.Compiler.MAlonzo.Compiler
cdcont | Agda.Auto.Syntax
cddeffreevars | Agda.Auto.Syntax
cdname | Agda.Auto.Syntax
cdorigin | Agda.Auto.Syntax
cdtype | Agda.Auto.Syntax
CExp | Agda.Auto.Syntax
chainl | Agda.Utils.Parser.ReadP
chainl1 | Agda.Utils.Parser.ReadP
chainr | Agda.Utils.Parser.ReadP
chainr1 | Agda.Utils.Parser.ReadP
Change | Agda.Utils.Update
Char |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
char |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Utils.Parser.ReadP
chaseDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
chaseMsg | Agda.Interaction.Imports
checkAbsurdLambda | Agda.TypeChecking.Rules.Term
checkAlias | Agda.TypeChecking.Rules.Def
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
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
checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl
checkCompilerPragmas | Agda.Compiler.JS.Compiler
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
checkConstructorCount | Agda.Compiler.MAlonzo.HaskellTypes
CheckConstructorFitsIn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkConstructorType | Agda.Compiler.MAlonzo.Compiler
checkCover | Agda.Compiler.MAlonzo.Compiler
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkDataDef | Agda.TypeChecking.Rules.Data
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclCached | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDisplayPragma | Agda.TypeChecking.Rules.Display
checkDontExpandLast | Agda.TypeChecking.Rules.Term
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
checkeliminand | Agda.Auto.Typecheck
checkEmptyTel | Agda.TypeChecking.Empty
checkEmptyType | 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
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.IApplyConfluence
checkIApplyConfluence_ | Agda.TypeChecking.IApplyConfluence
checkImport | Agda.TypeChecking.Rules.Decl
checkIndexSorts | Agda.TypeChecking.Rules.Data
checkInjectivity | Agda.TypeChecking.Injectivity
checkInjectivity_ | Agda.TypeChecking.Rules.Decl
checkInternal | Agda.TypeChecking.CheckInternal
checkInternal' | Agda.TypeChecking.CheckInternal
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
checkLetBindings | Agda.TypeChecking.Rules.Term
checkLevel | Agda.TypeChecking.Rules.Term
CheckLHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkLinearity | Agda.TypeChecking.MetaVars
checkLiteral | Agda.TypeChecking.Rules.Term
checkMacroType | Agda.TypeChecking.Rules.Def
checkMeta | Agda.TypeChecking.Rules.Term
checkModuleArity | Agda.TypeChecking.Rules.Decl
checkModuleName | Agda.Interaction.FindFile
checkMutual | Agda.TypeChecking.Rules.Decl
checkNamedArg | Agda.TypeChecking.Rules.Term
CheckNamedWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkOptionsCompatible | Agda.Interaction.Imports
checkOpts | Agda.Interaction.Options
checkOrInferMeta | Agda.TypeChecking.Rules.Term
checkOverapplication | Agda.TypeChecking.Injectivity
checkPath | Agda.TypeChecking.Rules.Term
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPatternLinearity | Agda.Syntax.Abstract.Pattern
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkPragma | Agda.TypeChecking.Rules.Decl
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
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
checkSizeIndex | Agda.TypeChecking.Polarity
CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
checkSizeLtSat | Agda.TypeChecking.SizedTypes
checkSizeNeverZero | Agda.TypeChecking.SizedTypes
checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes
checkSort | Agda.TypeChecking.CheckInternal
checkSortOfSplitVar | Agda.TypeChecking.Rules.LHS
checkStrictlyPositive | Agda.TypeChecking.Positivity
checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality
checkSystemCoverage | Agda.TypeChecking.Rules.Def
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.CheckInternal
checkType' | Agda.TypeChecking.CheckInternal
checkTypeCheckingProblem | Agda.TypeChecking.Constraints
checkTypedBindings | Agda.TypeChecking.Rules.Term
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.Auto.NarrowingSearch
choice |
1 (Function) | Agda.Utils.Parser.ReadP
2 (Function) | Agda.TypeChecking.Unquote
choiceP | Agda.Utils.Parser.MemoisedCPS
choose | Agda.Auto.NarrowingSearch
ChooseEither | Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseHighlightingMethod | Agda.Interaction.Highlighting.Common
ChooseLeft | Agda.TypeChecking.Rules.LHS.Problem
choosePrioMeta | Agda.Auto.NarrowingSearch
ChooseRight | Agda.TypeChecking.Rules.LHS.Problem
chop | Agda.Utils.List
chopWhen | Agda.Utils.List
Chr | Agda.Utils.Pretty
Cl |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile
cl | Agda.TypeChecking.Names
cl' | Agda.TypeChecking.Names
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
classifyForeign | Agda.Compiler.MAlonzo.Pragmas
classifyPragma | Agda.Compiler.MAlonzo.Pragmas
classifyWarning | Agda.TypeChecking.Warnings
classifyWarnings | Agda.TypeChecking.Warnings
Clause |
1 (Type/Class) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Type/Class) | Agda.Syntax.Internal
5 (Data Constructor) | Agda.Syntax.Internal
6 (Type/Class) | Agda.Syntax.Abstract
7 (Data Constructor) | Agda.Syntax.Abstract
8 (Type/Class) | Agda.Syntax.Concrete.Definitions
9 (Data Constructor) | Agda.Syntax.Concrete.Definitions
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
clauseFullRange | Agda.Syntax.Internal
clauseLHS | Agda.Syntax.Abstract
clauseLHSRange | Agda.Syntax.Internal
clausePats | Agda.Syntax.Internal
clausePerm | Agda.Syntax.Internal.Pattern
clauseRHS | Agda.Syntax.Abstract
ClausesPostChecks | Agda.TypeChecking.Rules.Def
clauseStrippedPats | Agda.Syntax.Abstract
clauseTel | Agda.Syntax.Internal
clauseToSplitClause | Agda.TypeChecking.Coverage
clauseType | Agda.Syntax.Internal
clauseUnreachable | Agda.Syntax.Internal
clauseWhereDecls | Agda.Syntax.Abstract
ClauseZipper | Agda.Interaction.MakeCase
clBody | Agda.TypeChecking.CompiledClause.Compile
Clean | Agda.TypeChecking.Unquote
clean | Agda.Utils.Graph.AdjacencyMap.Unidirectional
cleanCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
clearRunningInfo | Agda.Interaction.EmacsCommand
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
Clos |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
closeBrace | Agda.Syntax.Parser.Layout
closed | Agda.TypeChecking.Free
ClosedLevel | Agda.Syntax.Internal
closedTerm | Agda.Compiler.MAlonzo.Compiler
closedTermToTreeless | Agda.Compiler.ToTreeless
ClosedType | Agda.TypeChecking.Rules.Data
closify | Agda.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
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
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
cmdToName | Agda.TypeChecking.Primitive
Cmd_abort | Agda.Interaction.InteractionTop
Cmd_autoAll | Agda.Interaction.InteractionTop
Cmd_autoOne | Agda.Interaction.InteractionTop
Cmd_compile | Agda.Interaction.InteractionTop
Cmd_compute | Agda.Interaction.InteractionTop
Cmd_compute_toplevel | Agda.Interaction.InteractionTop
Cmd_constraints | Agda.Interaction.InteractionTop
Cmd_context | Agda.Interaction.InteractionTop
Cmd_elaborate_give | Agda.Interaction.InteractionTop
Cmd_give | Agda.Interaction.InteractionTop
Cmd_goal_type | Agda.Interaction.InteractionTop
Cmd_goal_type_context | Agda.Interaction.InteractionTop
cmd_goal_type_context_and | Agda.Interaction.InteractionTop
Cmd_goal_type_context_check | Agda.Interaction.InteractionTop
Cmd_goal_type_context_infer | Agda.Interaction.InteractionTop
Cmd_helper_function | Agda.Interaction.InteractionTop
cmd_helper_function | Agda.Interaction.InteractionTop
Cmd_highlight | Agda.Interaction.InteractionTop
Cmd_infer | Agda.Interaction.InteractionTop
Cmd_infer_toplevel | Agda.Interaction.InteractionTop
Cmd_intro | Agda.Interaction.InteractionTop
Cmd_load | Agda.Interaction.InteractionTop
cmd_load' | Agda.Interaction.InteractionTop
Cmd_load_highlighting_info | Agda.Interaction.InteractionTop
Cmd_make_case | Agda.Interaction.InteractionTop
Cmd_metas | Agda.Interaction.InteractionTop
Cmd_refine | Agda.Interaction.InteractionTop
Cmd_refine_or_intro | Agda.Interaction.InteractionTop
Cmd_search_about_toplevel | Agda.Interaction.InteractionTop
Cmd_show_module_contents | Agda.Interaction.InteractionTop
Cmd_show_module_contents_toplevel | Agda.Interaction.InteractionTop
Cmd_show_version | Agda.Interaction.InteractionTop
Cmd_solveAll | Agda.Interaction.InteractionTop
Cmd_solveOne | Agda.Interaction.InteractionTop
Cmd_tokenHighlighting | Agda.Interaction.InteractionTop
Cmd_why_in_scope | Agda.Interaction.InteractionTop
Cmd_why_in_scope_toplevel | Agda.Interaction.InteractionTop
CMFBlocked | Agda.Auto.Typecheck
CMFFlex | Agda.Auto.Typecheck
CMFlex |
1 (Type/Class) | Agda.Auto.Typecheck
2 (Data Constructor) | Agda.Auto.Typecheck
CMFSemi | Agda.Auto.Typecheck
CMode | Agda.Auto.Typecheck
Cmp | Agda.TypeChecking.SizedTypes.Syntax
cmp | Agda.TypeChecking.SizedTypes.Syntax
CmpElim | Agda.Interaction.BasicOps
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpInType | Agda.Interaction.BasicOps
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CmpLevels | Agda.Interaction.BasicOps
CmpSorts | Agda.Interaction.BasicOps
CmpTeles | Agda.Interaction.BasicOps
CmpTypes | Agda.Interaction.BasicOps
CMRigid | Agda.Auto.Typecheck
CMSet |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
cmSet | Agda.Termination.CallMatrix
Codata | Agda.Syntax.Concrete.Definitions
Code | Agda.Syntax.Parser.Literate
code |
1 (Function) | Agda.Syntax.Parser.Lexer
2 (Function) | Agda.Interaction.Highlighting.HTML
CoDomain | Agda.Utils.TypeLevel
CoDomain' | Agda.Utils.TypeLevel
coerce | Agda.TypeChecking.Conversion
coerceSize | Agda.TypeChecking.Conversion
CoinductionKit |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin
coinductionKit | Agda.TypeChecking.Monad.Builtin
coinductionKit' | Agda.TypeChecking.Monad.Builtin
CoInductive | Agda.Syntax.Common
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CoInfectiveImport_ | Agda.Interaction.Options.Warnings
coinfectiveOptions | Agda.Interaction.Options
col | Agda.Termination.SparseMatrix
coldescr | Agda.Utils.Warshall
collapseDefault | Agda.Utils.WithDefault
collapseO | Agda.Termination.Order
collectStats | Agda.TypeChecking.Serialise.Base
colon |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
cols | Agda.Termination.SparseMatrix
combineHashes | Agda.Utils.Hash
comma |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Command |
1 (Type/Class) | Agda.Interaction.CommandLine
2 (Type/Class) | Agda.Interaction.InteractionTop
3 (Data Constructor) | Agda.Interaction.InteractionTop
Command' | Agda.Interaction.InteractionTop
commandLineFlags | Agda.Compiler.Backend
CommandLineOptions | Agda.Interaction.Options
commandLineOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CommandM | Agda.Interaction.InteractionTop
commandMToIO | Agda.Interaction.InteractionTop
CommandQueue |
1 (Type/Class) | Agda.Interaction.InteractionTop
2 (Data Constructor) | Agda.Interaction.InteractionTop
commandQueue | Agda.Interaction.InteractionTop
commands | Agda.Interaction.InteractionTop
CommandState |
1 (Type/Class) | Agda.Interaction.InteractionTop
2 (Data Constructor) | Agda.Interaction.InteractionTop
Comment |
1 (Data Constructor) | Agda.Syntax.Parser.Literate
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
commitInfo | Agda.VersionCommit
commonParentModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver
commonPrefix | Agda.Utils.List
commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver
commonSuffix | Agda.Utils.List
comp' | Agda.Auto.Typecheck
compactP | Agda.Utils.Permutation
compactS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Comparable | Agda.Utils.PartialOrd
comparable | Agda.Utils.PartialOrd
comparableOrd | Agda.Utils.PartialOrd
Compare | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compareArgs | Agda.TypeChecking.Conversion
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
compareFloat | Agda.Syntax.Literal
compareInterval | Agda.TypeChecking.Conversion
compareIrrelevant | Agda.TypeChecking.Conversion
compareLevel | Agda.TypeChecking.Conversion
compareMaxViews | Agda.TypeChecking.SizedTypes
compareOffset | Agda.TypeChecking.SizedTypes.Syntax
compareRelevance | Agda.TypeChecking.Conversion
CompareResult | Agda.Utils.Favorites
compareSizes | Agda.TypeChecking.SizedTypes
compareSizeViews | Agda.TypeChecking.SizedTypes
compareSort | Agda.TypeChecking.Conversion
compareTel | Agda.TypeChecking.Conversion
compareTerm | Agda.TypeChecking.Conversion
compareTerm' | Agda.TypeChecking.Conversion
compareTermDir | Agda.TypeChecking.Conversion
compareTermOnFace | Agda.TypeChecking.Conversion
compareTermOnFace' | Agda.TypeChecking.Conversion
compareType | Agda.TypeChecking.Conversion
compareWithFavorites | Agda.Utils.Favorites
compareWithPol | Agda.TypeChecking.Conversion
Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compile | Agda.TypeChecking.CompiledClause.Compile
compileAlt | Agda.Compiler.JS.Compiler
compileClauses | Agda.TypeChecking.CompiledClause.Compile
compileClauses' | Agda.TypeChecking.CompiledClause.Compile
Compiled |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
compiledClauseBody | Agda.TypeChecking.Substitute
CompiledClauses | Agda.TypeChecking.CompiledClause
CompiledClauses' | Agda.TypeChecking.CompiledClause
compiledcondecl | Agda.Compiler.MAlonzo.Compiler
compileDef | Agda.Compiler.Backend
compileDir | Agda.Compiler.Common
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
compiledTypeSynonym | Agda.Compiler.MAlonzo.Compiler
CompilePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compilePrim |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
CompilerBackend | Agda.Interaction.InteractionTop
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
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
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
composeFlexRig | Agda.TypeChecking.Free.Lazy
composeModality | Agda.Syntax.Common
composeP | Agda.Utils.Permutation
composePol | Agda.TypeChecking.Polarity
composeQuantity | Agda.Syntax.Common
composeRelevance | Agda.Syntax.Common
composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
composeVarOcc | Agda.TypeChecking.Free.Lazy
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
ComposeZip | Agda.Utils.Zipper
ComposeZipper | Agda.Utils.Zipper
Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compress | Agda.Interaction.Highlighting.Precise
CompressedFile |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
compressedFileInvariant | Agda.Interaction.Highlighting.Precise
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.BasicOps
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
computeUnsolvedConstraints | Agda.Interaction.Highlighting.Generate
computeUnsolvedMetaWarnings | Agda.Interaction.Highlighting.Generate
computeWrapInput | Agda.Interaction.BasicOps
Con |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conApp | Agda.TypeChecking.Substitute
ConArgType | Agda.TypeChecking.Positivity.Occurrence
conArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conArityAndPars | Agda.Compiler.Common
conBranches | Agda.TypeChecking.CompiledClause
conCase | Agda.TypeChecking.CompiledClause
Concat | Agda.TypeChecking.Positivity
Concat' | Agda.TypeChecking.Positivity
concatargs | Agda.Auto.CaseSplit
concatListT | Agda.Utils.ListT
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
concreteNamesInScope | Agda.Syntax.Scope.Base
concreteOptionsToOptionPragmas | Agda.Interaction.Imports
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConDecl |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
condecl | Agda.Compiler.MAlonzo.Compiler
Condition | Agda.TypeChecking.MetaVars
conErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conFields | Agda.Syntax.Internal
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
conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conInductive | Agda.Syntax.Internal
ConInfo | Agda.Syntax.Internal
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Conj | Agda.TypeChecking.Conversion
ConName | Agda.Syntax.Scope.Base
conName | Agda.Syntax.Internal
ConnectHandle | Agda.Auto.NarrowingSearch
connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConOCon | Agda.Syntax.Common
ConORec | Agda.Syntax.Common
ConOrigin | Agda.Syntax.Common
ConOSplit | Agda.Syntax.Common
ConOSystem | Agda.Syntax.Common
ConP |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Internal
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
ConPatLazy |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
ConPatternInfo |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
conPFallThrough | Agda.Syntax.Internal
conPLazy | Agda.Syntax.Internal
conPRecord | Agda.Syntax.Internal
conPType | Agda.Syntax.Internal
Cons |
1 (Data Constructor) | Agda.Utils.IndexedList
2 (Data Constructor) | Agda.Interaction.EmacsCommand
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
consNe | Agda.Utils.NonemptyList
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.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Auto.Syntax
Constant | Agda.Utils.TypeLevel
Constant0 | Agda.Utils.TypeLevel
Constant1 | Agda.Utils.TypeLevel
ConstDef |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
Constr |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
constrainedPrims | Agda.TypeChecking.Monad.Builtin
Constraint |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class) | Agda.Utils.Warshall
4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.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 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstraintStatus | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ConstRef | Agda.Auto.Syntax
constructIScope | Agda.Interaction.Imports
Constructor |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Type/Class) | Agda.Syntax.Abstract
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructorCoverageCode | Agda.Compiler.MAlonzo.Compiler
constructorForm |
1 (Function) | Agda.TypeChecking.Monad.Builtin
2 (Function) | Agda.TypeChecking.Reduce.Monad
constructorForm' | Agda.TypeChecking.Monad.Builtin
constructorImpossible | Agda.Auto.Typecheck
ConstructorInfo | Agda.TypeChecking.Datatypes
ConstructorName | Agda.Syntax.Scope.Base
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
constructPats | Agda.Auto.Convert
constructs | Agda.TypeChecking.Rules.Data
containsAbsurdPattern | Agda.Syntax.Abstract.Pattern
containsAPattern | Agda.Syntax.Abstract.Pattern
containsAsPattern | Agda.Syntax.Abstract.Pattern
contains_constructor | Agda.Auto.Convert
content | Agda.TypeChecking.CompiledClause
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
contextOfMeta | Agda.Interaction.BasicOps
contextSize | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Continue | Agda.Interaction.CommandLine
continueAfter | Agda.Interaction.CommandLine
ContinueIn | Agda.Interaction.CommandLine
continuous | Agda.Syntax.Position
continuousPerLine | Agda.Syntax.Position
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
conUseSizeLt | Agda.Termination.Monad
convError | Agda.TypeChecking.Conversion
Conversion | Agda.Auto.Convert
convert | Agda.Auto.Convert
convertGuards | Agda.Compiler.Treeless.GuardsToPrims
CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
copatternsNotImplemented | Agda.Auto.Convert
copyarg | Agda.Auto.Typecheck
copyDirContent | Agda.Utils.IO.Directory
copyRTEModules |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
copyScope | Agda.Syntax.Scope.Monad
copyTerm | Agda.Syntax.Internal.Generic
CosplitCatchall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
CosplitNoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Cost |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
costAbsurdLam | Agda.Auto.SearchControl
costAddVarDepth | Agda.Auto.CaseSplit
costAppConstructor | Agda.Auto.SearchControl
costAppConstructorSingle | Agda.Auto.SearchControl
costAppExtraRef | Agda.Auto.SearchControl
costAppHint | Agda.Auto.SearchControl
costAppHintUsed | Agda.Auto.SearchControl
costAppRecCall | Agda.Auto.SearchControl
costAppRecCallUsed | Agda.Auto.SearchControl
costAppVar | Agda.Auto.SearchControl
costAppVarUsed | Agda.Auto.SearchControl
costCaseSplitHigh | Agda.Auto.CaseSplit
costCaseSplitLow | Agda.Auto.CaseSplit
costCaseSplitVeryHigh | Agda.Auto.CaseSplit
costEqCong | Agda.Auto.SearchControl
costEqEnd | Agda.Auto.SearchControl
costEqStep | Agda.Auto.SearchControl
costEqSym | Agda.Auto.SearchControl
costIncrease | Agda.Auto.SearchControl
costInferredTypeUnkown | Agda.Auto.SearchControl
costIotaStep | Agda.Auto.SearchControl
costLam | Agda.Auto.SearchControl
costLamUnfold | Agda.Auto.SearchControl
costPi | Agda.Auto.SearchControl
costSort | Agda.Auto.SearchControl
costUnification | Agda.Auto.SearchControl
costUnificationIf | Agda.Auto.SearchControl
costUnificationOccurs | Agda.Auto.SearchControl
count |
1 (Function) | Agda.Utils.Bag
2 (Function) | Agda.Utils.Parser.ReadP
CountPatternVars | Agda.Syntax.Internal.Pattern
countPatternVars | Agda.Syntax.Internal.Pattern
countTelVars | Agda.Syntax.Concrete
countWithArgs | Agda.TypeChecking.With
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
coverageCheck | Agda.TypeChecking.Coverage
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.Interaction.Highlighting.Precise
Covering |
1 (Type/Class) | Agda.TypeChecking.Coverage
2 (Data Constructor) | Agda.TypeChecking.Coverage
covSplitArg | Agda.TypeChecking.Coverage
covSplitClauses | Agda.TypeChecking.Coverage
CPatternLike | Agda.Syntax.Concrete.Pattern
CPC | Agda.TypeChecking.Rules.Def
cpcPartialSplits | Agda.TypeChecking.Rules.Def
CPUTime |
1 (Type/Class) | Agda.Utils.Time
2 (Data Constructor) | Agda.Utils.Time
createInterface | Agda.Interaction.Imports
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
createModule | Agda.Syntax.Scope.Monad
CSAbsurd | Agda.Auto.CaseSplit
CSCtx | Agda.Auto.CaseSplit
CSOmittedArg | Agda.Auto.CaseSplit
CSPat | Agda.Auto.CaseSplit
CSPatConApp | Agda.Auto.CaseSplit
CSPatExp | Agda.Auto.CaseSplit
CSPatI | Agda.Auto.CaseSplit
CSPatVar | Agda.Auto.CaseSplit
CSWith | Agda.Auto.CaseSplit
CTChar | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTData | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTFloat | Agda.Syntax.Treeless, Agda.Compiler.Backend
cthandles | Agda.Auto.NarrowingSearch
CTInt | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTNat | Agda.Syntax.Treeless, Agda.Compiler.Backend
ctparent | Agda.Auto.NarrowingSearch
ctpriometa | Agda.Auto.NarrowingSearch
CTQName | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTrans | Agda.TypeChecking.SizedTypes.Syntax
CTree |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
cTreeless | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTString | Agda.Syntax.Treeless, Agda.Compiler.Backend
ctsub | Agda.Auto.NarrowingSearch
Ctx | Agda.Auto.Syntax
CType | Agda.TypeChecking.Rules.Data
curDefs | Agda.Compiler.Common
curHsMod | Agda.Compiler.MAlonzo.Misc
curIF | Agda.Compiler.Common
curMName | Agda.Compiler.Common
curModule | Agda.Compiler.JS.Compiler
CurrentAccount | Agda.Utils.Benchmark
currentAccount | Agda.Utils.Benchmark
currentCxt | Agda.TypeChecking.Names
CurrentInput | Agda.Syntax.Parser.Alex
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, 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
curSig | Agda.Compiler.Common
CutOff |
1 (Type/Class) | Agda.Termination.CutOff
2 (Data Constructor) | Agda.Termination.CutOff
cxtSubst | Agda.TypeChecking.Names
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend