Agda-2.3.2: 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

CAction | Agda.Auto.Syntax
calc | Agda.Auto.NarrowingSearch
calcEqRState | Agda.Auto.Typecheck
CALConcat | Agda.Auto.Syntax
Call |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callCompiler | Agda.Compiler.CallCompiler
callCompiler' | Agda.Compiler.CallCompiler
callGHC | Agda.Compiler.MAlonzo.Compiler
CallGraph | Agda.Termination.CallGraph
callGraphInvariant | Agda.Termination.CallGraph
CallInfo |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInfoRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
callInvariant | Agda.Termination.CallGraph
CallMatrix |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
callMatrixInvariant | Agda.Termination.CallGraph
calls | Agda.Termination.Lexicographic
CALNil | Agda.Auto.Syntax
canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
CantSplit | Agda.TypeChecking.Coverage
Case |
1 (Type/Class) | Agda.Compiler.JS.Case
2 (Data Constructor) | Agda.Compiler.JS.Case
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST
4 (Data Constructor) | Agda.TypeChecking.CompiledClause
5 (Type/Class) | Agda.TypeChecking.CompiledClause
CaseContext | Agda.Interaction.MakeCase
casee | Agda.Compiler.Epic.AuxAST
caseOpts | Agda.Compiler.Epic.CaseOpts
caseOptsExpr | Agda.Compiler.Epic.CaseOpts
caseSplitSearch | Agda.Auto.CaseSplit
caseSplitSearch' | Agda.Auto.CaseSplit
cat | Agda.Utils.Pretty
catchAll | Agda.TypeChecking.CompiledClause
catchAllBranch | Agda.TypeChecking.CompiledClause
catchConstraint | Agda.TypeChecking.Constraints
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
catchException | Agda.TypeChecking.Monad.Exception
catchImpossible | Agda.Utils.Impossible
categorizedecl | Agda.Auto.Syntax
catMaybes | Agda.Utils.Maybe
cdcont | Agda.Auto.Syntax
cddeffreevars | Agda.Auto.Syntax
cdecl | Agda.Compiler.MAlonzo.Compiler
cdname | Agda.Auto.Syntax
cdorigin | Agda.Auto.Syntax
cdtype | Agda.Auto.Syntax
CExp | Agda.Auto.Syntax
chainl | Agda.Utils.ReadP
chainl1 | Agda.Utils.ReadP
chainl1' | Agda.Syntax.Concrete.Operators.Parser
chainr | Agda.Utils.ReadP
chainr1 | Agda.Utils.ReadP
chainr1' | Agda.Syntax.Concrete.Operators.Parser
Char | Agda.Compiler.JS.Syntax
char |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Utils.ReadP
chatty | Agda.Utils.QuickCheck
checkAlias | Agda.TypeChecking.Rules.Def
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkArguments | Agda.TypeChecking.Rules.Term
checkArguments' | Agda.TypeChecking.Rules.Term
checkArguments_ | Agda.TypeChecking.Rules.Term
checkAxiom | Agda.TypeChecking.Rules.Decl
checkCandidates | Agda.TypeChecking.InstanceArguments
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkClause | Agda.TypeChecking.Rules.Def
CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkConstructor | Agda.TypeChecking.Rules.Data
checkConstructorApplication | Agda.TypeChecking.Rules.Term
checkConstructorType | Agda.Compiler.MAlonzo.Compiler
checkCover | Agda.Compiler.MAlonzo.Compiler
checkCoverage | Agda.TypeChecking.Coverage
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDataDef | Agda.TypeChecking.Rules.Data
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkDotPattern | Agda.TypeChecking.Rules.LHS
checkeliminand | Agda.Auto.Typecheck
checkEqualities | Agda.TypeChecking.Rules.LHS.Unify
checkEquality | Agda.TypeChecking.Rules.LHS.Unify
checkEqualityHH | Agda.TypeChecking.Rules.LHS.Unify
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkFunDef | Agda.TypeChecking.Rules.Def
checkFunDef' | Agda.TypeChecking.Rules.Def
checkHeadApplication | Agda.TypeChecking.Rules.Term
checkImport | Agda.TypeChecking.Rules.Decl
checkInjectivity | Agda.TypeChecking.Injectivity
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLambda | Agda.TypeChecking.Rules.Term
checkLeftHandSide | Agda.TypeChecking.Rules.LHS
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkLetBinding | Agda.TypeChecking.Rules.Term
checkLetBindings | Agda.TypeChecking.Rules.Term
checkLinearity | Agda.TypeChecking.MetaVars
checkLiteral | Agda.TypeChecking.Rules.Term
checkMeta | Agda.TypeChecking.Rules.Term
checkModuleArity | Agda.TypeChecking.Rules.Decl
checkModuleName | Agda.Interaction.FindFile
checkMutual | Agda.TypeChecking.Rules.Decl
checkOpts | Agda.Interaction.Options
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPragma | Agda.TypeChecking.Rules.Decl
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkPrimitive | Agda.TypeChecking.Rules.Decl
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkRecDef | Agda.TypeChecking.Rules.Record
checkRecordProjections | Agda.TypeChecking.Rules.Record
checkSection | Agda.TypeChecking.Rules.Decl
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
checkSectionApplication | Agda.TypeChecking.Rules.Decl
checkSectionApplication' | Agda.TypeChecking.Rules.Decl
checkSizeIndex | Agda.TypeChecking.Polarity
checkStrictlyPositive | Agda.TypeChecking.Positivity
checkTelescope_ | Agda.TypeChecking.Rules.Term
checkTerm | Agda.TypeChecking.Rules.Term
checkTypedBinding | Agda.TypeChecking.Rules.Term
checkTypedBindings | Agda.TypeChecking.Rules.Term
checkTypedBindings_ | Agda.TypeChecking.Rules.Term
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives
checkTypeSignature | Agda.TypeChecking.Rules.Decl
checkWhere | Agda.TypeChecking.Rules.Def
checkWithFunction | Agda.TypeChecking.Rules.Def
CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Choice | Agda.Auto.NarrowingSearch
choice |
1 (Function) | Agda.Utils.ReadP
2 (Function) | Agda.TypeChecking.Coverage.Match
3 (Function) | Agda.TypeChecking.Quote
choose |
1 (Function) | Agda.Utils.QuickCheck
2 (Function) | Agda.Auto.NarrowingSearch
choosePrioMeta | Agda.Auto.NarrowingSearch
chop | Agda.Utils.List
Chr | Agda.Utils.Pretty
Cl | Agda.TypeChecking.CompiledClause.Compile
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
classify | Agda.Utils.QuickCheck
Clause |
1 (Type/Class) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Internal
4 (Type/Class) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.Syntax.Abstract
6 (Type/Class) | Agda.Syntax.Concrete.Definitions
7 (Data Constructor) | Agda.Syntax.Concrete.Definitions
clause |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
ClauseBody | Agda.Syntax.Internal
clauseBody | Agda.Syntax.Internal
clausebody | Agda.Compiler.MAlonzo.Compiler
clauseLHS | Agda.Syntax.Abstract
clausePats | Agda.Syntax.Internal
clausePerm | Agda.Syntax.Internal
clauseRange | Agda.Syntax.Internal
clauseRHS | Agda.Syntax.Abstract
clauseTel | Agda.Syntax.Internal
clauseToSplitClause | Agda.TypeChecking.Coverage
clauseWhereDecls | Agda.Syntax.Abstract
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
clearRunningInfo | Agda.Interaction.EmacsCommand
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ClockTime | Agda.Utils.Time
Clos |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
closeBrace | Agda.Syntax.Parser.Layout
ClosedLevel | Agda.Syntax.Internal
closify | Agda.Auto.Syntax
Closure |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Cls | Agda.TypeChecking.CompiledClause.Compile
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cm | Agda.Termination.CallGraph
Cmd_auto | 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_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_infer | 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_show_module_contents | Agda.Interaction.InteractionTop
Cmd_show_module_contents_toplevel | Agda.Interaction.InteractionTop
Cmd_solveAll | 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
CmpElim | Agda.Interaction.BasicOps
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpInType | Agda.Interaction.BasicOps
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CmpLevels | Agda.Interaction.BasicOps
CmpSorts | Agda.Interaction.BasicOps
CmpTeles | Agda.Interaction.BasicOps
CmpTypes | Agda.Interaction.BasicOps
CMRigid | Agda.Auto.Typecheck
CName |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree
cnvh | Agda.Auto.Convert
CoArbitrary | Agda.Utils.QuickCheck
coarbitrary | Agda.Utils.QuickCheck
coarbitraryEnum | Agda.Utils.QuickCheck
coarbitraryIntegral | Agda.Utils.QuickCheck
coarbitraryReal | Agda.Utils.QuickCheck
coarbitraryShow | Agda.Utils.QuickCheck
Codata | Agda.Syntax.Concrete.Definitions
code | Agda.Syntax.Parser.Lexer
coerce | Agda.TypeChecking.Conversion
CoinductionKit |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin
coinductionKit | Agda.TypeChecking.Monad.Builtin
CoInductive | Agda.Syntax.Common
CoinductiveDatatype | Agda.TypeChecking.Coverage
col |
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Termination.SparseMatrix
coldescr | Agda.Utils.Warshall
collect | Agda.Utils.QuickCheck
colon |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
cols |
1 (Function) | Agda.Termination.Matrix
2 (Function) | Agda.Termination.SparseMatrix
Column | Agda.Termination.Lexicographic
columns | Agda.Termination.Lexicographic
comma |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Command | Agda.Interaction.CommandLine.CommandLine
CommandLineOptions | Agda.Interaction.Options
commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
CommandM |
1 (Type/Class) | Agda.Interaction.InteractionTop
2 (Data Constructor) | Agda.Interaction.InteractionTop
commandMToIO | Agda.Interaction.InteractionTop
CommandState |
1 (Type/Class) | Agda.Interaction.InteractionTop
2 (Data Constructor) | Agda.Interaction.InteractionTop
Comment |
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise
2 (Type/Class) | Agda.Compiler.Epic.AuxAST
commutative | Agda.Utils.TestHelpers
comp' | Agda.Auto.Typecheck
compactP | Agda.Utils.Permutation
compareArgs | Agda.TypeChecking.Conversion
compareAtom | Agda.TypeChecking.Conversion
compareBelowMax | Agda.TypeChecking.SizedTypes
compareElims | Agda.TypeChecking.Conversion
compareIrrelevant | Agda.TypeChecking.Conversion
compareLevel | Agda.TypeChecking.UniversePolymorphism
compareMaxViews | Agda.TypeChecking.SizedTypes
compareRelevance | Agda.TypeChecking.Conversion
compareSizes | Agda.TypeChecking.SizedTypes
compareSizeViews | Agda.TypeChecking.SizedTypes
compareSort | Agda.TypeChecking.Conversion
compareTel | Agda.TypeChecking.Conversion
compareTerm | Agda.TypeChecking.Conversion
compareTerm' | Agda.TypeChecking.Conversion
compareType | Agda.TypeChecking.Conversion
compareWithPol | Agda.TypeChecking.Conversion
Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Compile | Agda.Compiler.Epic.CompileState
compile |
1 (Function) | Agda.TypeChecking.CompiledClause.Compile
2 (Function) | Agda.Compiler.MAlonzo.Compiler
3 (Function) | Agda.Compiler.JS.Compiler
compileClauses |
1 (Function) | Agda.TypeChecking.CompiledClause.Compile
2 (Function) | Agda.Compiler.Epic.FromAgda
CompiledClauses | Agda.TypeChecking.CompiledClause
CompiledDataPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compiledEpic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledEpicPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compiledHaskell | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
compileDir |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
compiledJS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledJSPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compiledModules | Agda.Compiler.Epic.CompileState
CompiledPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
CompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CompiledTypePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compilerMain |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.Epic.Compiler
3 (Function) | Agda.Compiler.JS.Compiler
CompileState |
1 (Type/Class) | Agda.Compiler.Epic.CompileState
2 (Data Constructor) | Agda.Compiler.Epic.CompileState
compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile
complete | Agda.Termination.CallGraph
composeP | Agda.Utils.Permutation
composePol | Agda.TypeChecking.Polarity
composeRelevance | Agda.TypeChecking.Irrelevance
composeS | Agda.TypeChecking.Substitute
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
compressPointerChain | Agda.Syntax.Internal
computeEdge | Agda.TypeChecking.Positivity
computeNeighbourhood | Agda.TypeChecking.Coverage
ComputeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences | Agda.TypeChecking.Positivity
computePolarity | Agda.TypeChecking.Polarity
computeSizeConstraint | Agda.TypeChecking.SizedTypes
computeSizeConstraints | Agda.TypeChecking.SizedTypes
Con |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Compiler.Epic.AuxAST
3 (Data Constructor) | Agda.Syntax.Abstract
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConArgType | Agda.TypeChecking.Positivity
conArity | Agda.Compiler.Epic.Interface
conArityAndPars | Agda.Compiler.MAlonzo.Compiler
conBranches | Agda.TypeChecking.CompiledClause
conCase | Agda.TypeChecking.CompiledClause
concatargs | Agda.Auto.CaseSplit
concatOccurs | Agda.TypeChecking.Positivity
ConcreteDef | Agda.Syntax.Common
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
condecl | Agda.Compiler.MAlonzo.Compiler
Condition | Agda.TypeChecking.MetaVars
ConElim | Agda.TypeChecking.Eliminators
conFreq | Agda.TypeChecking.Test.Generators
ConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conhqn | Agda.Compiler.MAlonzo.Misc
conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
conjoin | Agda.Utils.QuickCheck
ConMP | Agda.TypeChecking.Coverage.Match
ConName |
1 (Data Constructor) | Agda.Syntax.Scope.Base
2 (Type/Class) | Agda.TypeChecking.Test.Generators
3 (Data Constructor) | Agda.TypeChecking.Test.Generators
ConnectHandle | Agda.Auto.NarrowingSearch
ConP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Abstract
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Cons | Agda.Interaction.EmacsCommand
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Const |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
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
Constraint |
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constraintProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Constraints |
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ConstRef | Agda.Auto.Syntax
constrGroup | Agda.Compiler.Epic.Injection
constrInScope | Agda.Compiler.Epic.CompileState
constrTags | Agda.Compiler.Epic.Interface
Constructor |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
4 (Type/Class) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructorArity | Agda.Compiler.Epic.CompileState
constructorForm | Agda.TypeChecking.Primitive
constructorImpossible | Agda.Auto.Typecheck
ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify
constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify
constructorMismatchHH | Agda.TypeChecking.Rules.LHS.Unify
ConstructorName | Agda.Syntax.Scope.Monad
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
constructPats | Agda.Auto.Convert
constructs | Agda.TypeChecking.Rules.Data
Cont | Agda.Utils.Monad
containsAbsurdPattern | Agda.TypeChecking.Rules.Def
contains_constructor | Agda.Auto.Convert
content | Agda.TypeChecking.CompiledClause
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
contextOfMeta | Agda.Interaction.BasicOps
Continue | Agda.Interaction.CommandLine.CommandLine
continueAfter | Agda.Interaction.CommandLine.CommandLine
ContinueIn | Agda.Interaction.CommandLine.CommandLine
continuous | Agda.Syntax.Position
continuousPerLine | Agda.Syntax.Position
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
convError | Agda.TypeChecking.Conversion
convertLineEndings | Agda.Utils.Unicode
copyarg | Agda.Auto.Typecheck
copyScope | Agda.Syntax.Scope.Monad
copyTerm | Agda.Syntax.Internal.Generic
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
costUnificationOccurs | Agda.Auto.SearchControl
count | Agda.Utils.ReadP
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
cover |
1 (Function) | Agda.Utils.QuickCheck
2 (Function) | Agda.TypeChecking.Coverage
CoverageCantSplitIrrelevantType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
coverageCheck | Agda.TypeChecking.Coverage
CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Covering |
1 (Type/Class) | Agda.TypeChecking.Coverage
2 (Data Constructor) | Agda.TypeChecking.Coverage
CoverM | Agda.TypeChecking.Coverage
covSplitArg | Agda.TypeChecking.Coverage
covSplitClauses | Agda.TypeChecking.Coverage
createInterface | Agda.Interaction.Imports
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
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
cthandles | Agda.Auto.NarrowingSearch
ctparent | Agda.Auto.NarrowingSearch
ctpriometa | Agda.Auto.NarrowingSearch
CTree |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
ctsub | Agda.Auto.NarrowingSearch
Ctx |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
CtxId |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
curDefs | Agda.Compiler.MAlonzo.Misc
curFun | Agda.Compiler.Epic.CompileState
curHsMod | Agda.Compiler.MAlonzo.Misc
curIF | Agda.Compiler.MAlonzo.Misc
curMName | Agda.Compiler.MAlonzo.Misc
curModule |
1 (Function) | Agda.Compiler.Epic.CompileState
2 (Function) | Agda.Compiler.JS.Compiler
CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
CurrentInput | Agda.Syntax.Parser.Alex
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
currentProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
curriedApply | Agda.Compiler.JS.Substitution
curriedLambda | Agda.Compiler.JS.Substitution
curSig | Agda.Compiler.MAlonzo.Misc
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad