Agda-2.2.6: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ!$+./<=>|-
Index (C)
CAction
calc
CALConcat
Call
1 (Type/Class)
2 (Type/Class)
3 (Data Constructor)
callGHC
CallGraph
callGraphInvariant
callInvariant
CallMatrix
1 (Type/Class)
2 (Data Constructor)
callMatrixInvariant
calls
CallTrace
CALNil
canonicalName
CantSplit
CArgList
cat
catchConstraint
catchException
catchImpossible
catMaybes
cdcont
cdecl
cdname
cdorigin
cdtype
CExp
chainl
chainl1
chainr
chainr1
char
1 (Function)
2 (Function)
checkArgs
CheckArguments
checkArguments
checkArguments'
checkArguments_
checkAxiom
CheckClause
checkClause
CheckConstructor
checkConstructor
checkConstructorType
checkCover
checkCoverage
CheckDataDef
checkDataDef
checkDecl
checkDecls
checkDefinition
CheckDotPattern
checkDotPattern
checkEqualities
CheckExpr
checkExpr
checkForImportCycle
CheckFunDef
checkFunDef
checkHeadApplication
checkImport
checkInjectivity
checkLeftHandSide
CheckLetBinding
checkLetBinding
checkLetBindings
checkLiteral
checkModuleArity
checkModuleName
checkMutual
checkOpts
CheckPattern
CheckPatternShadowing
CheckPragma
checkPragma
CheckPrimitive
checkPrimitive
CheckRecDef
checkRecDef
checkRecordProjections
checkSection
CheckSectionApplication
checkSectionApplication
checkSizeIndex
checkStrictlyPositive
checkTelescope
checkTypedBinding
checkTypedBindings
checkTypeOfMain
checkTypeSignature
checkWhere
checkWithFunction
Child
ChildCall
Choice
choice
1 (Function)
2 (Function)
choose
1 (Function)
2 (Function)
choosePrioMeta
chop
Chr
ClashingDefinition
ClashingFileNamesFor
ClashingImport
ClashingModule
ClashingModuleImport
classify
Clause
1 (Type/Class)
2 (Type/Class)
3 (Data Constructor)
4 (Type/Class)
5 (Data Constructor)
6 (Type/Class)
7 (Data Constructor)
clause
1 (Function)
2 (Function)
clauseBod
ClauseBody
clauseBody
clausebody
clausePats
clausePerm
clauseRange
clauseTel
clearMetaListeners
clEnv
Clos
1 (Type/Class)
2 (Data Constructor)
closeBrace
ClosedLevel
closify
Closure
1 (Type/Class)
2 (Data Constructor)
clScope
clSignature
clTrace
clValue
cm
cmd_auto
cmd_compile
cmd_compute
cmd_compute_toplevel
cmd_constraints
cmd_context
cmd_give
cmd_goals
cmd_goal_type
cmd_goal_type_context
cmd_goal_type_context_and
cmd_goal_type_context_infer
cmd_infer
cmd_infer_toplevel
cmd_intro
cmd_load
cmd_load'
cmd_make_case
cmd_metas
cmd_refine
cmd_refine_or_intro
cmd_reset
cmd_solveAll
cmd_write_highlighting_info
CmpEq
CmpInType
CmpLeq
CmpSorts
CmpTeles
CmpTypes
cnt
cnvh
CoArbitrary
coarbitrary
coarbitraryIntegral
coarbitraryReal
coarbitraryShow
code
CoInductive
col
coldescr
collect
colon
cols
Column
columns
comma
1 (Function)
2 (Function)
Command
command
CommandLineOptions
commandLineOptions
Comment
commutative
commuteM
comp
comp'
compactP
compareArgs
compareAtom
compareSizes
compareSort
compareTel
compareTerm
compareType
compargs
Comparison
comphn'
CompilationError
compile
CompiledDataPragma
1 (Data Constructor)
2 (Data Constructor)
CompiledPragma
1 (Data Constructor)
2 (Data Constructor)
CompiledTypePragma
1 (Data Constructor)
2 (Data Constructor)
compilerMain
1 (Function)
2 (Function)
3 (Function)
complete
composeP
composePol
compress
CompressedFile
computeEdge
computeGreatestFixedPoint
computeLeastFixedPoint
computeMaxArity
computeNeighbourhood
ComputeOccurrences
computeOccurrences
computePolarity
computeSizeConstraint
Con
1 (Data Constructor)
2 (Data Constructor)
conAbstr
ConArgType
concatMapM
concatOccurs
ConcreteDef
ConcreteMode
concreteToAbstract
concreteToAbstract_
conData
condecl
conFreq
ConHead
conhqn
conHsCode
conInd
ConMP
ConName
1 (Data Constructor)
2 (Type/Class)
3 (Data Constructor)
conName
ConP
1 (Data Constructor)
2 (Data Constructor)
conPars
ConPos
conQName
conQStr
consDefs
consForName
conSrcCon
Const
ConstDef
1 (Type/Class)
2 (Data Constructor)
Constr
1 (Type/Class)
2 (Data Constructor)
conStr
Constraint
1 (Type/Class)
2 (Type/Class)
ConstraintClosure
Constraints
1 (Type/Class)
2 (Type/Class)
ConstRef
Constructor
1 (Data Constructor)
2 (Type/Class)
3 (Type/Class)
4 (Data Constructor)
5 (Data Constructor)
constructorArity
constructorForm
ConstructorMismatch
constructorMismatch
ConstructorName
ConstructorPatternInWrongDatatype
constructorsInClause
constructorsInClauses
constructs
Cont
containsAbsurdPattern
contClause
Context
ContextEntry
contextOfMeta
Continue
continueAfter
ContinueIn
continuous
continuousPerLine
Contravariant
convertLineEndings
copyScope
count
Covariant
cover
1 (Function)
2 (Function)
CoverageCantSplitOn
CoverageCantSplitType
CoverageFailure
Covering
CoverM
createInterface
createMetaInfo
createModule
ctparent
ctpriometa
CTree
1 (Type/Class)
2 (Data Constructor)
ctsub
Ctx
1 (Type/Class)
2 (Data Constructor)
ctxEntry
CtxId
1 (Type/Class)
2 (Data Constructor)
ctxId
curDefs
curHsMod
curIF
curMName
Current
CurrentCall
CurrentDir
CurrentInput
currentModule
currentMutualBlock
curSig
CyclicModuleDependency