Agda-2.2.10: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ:!$&+./<=>|-
Index (C)
CAction
calc
calcEqRState
CALConcat
Call
1 (Type/Class)
2 (Type/Class)
3 (Data Constructor)
callGHC
CallGraph
callGraphInvariant
callInvariant
CallMatrix
1 (Type/Class)
2 (Data Constructor)
callMatrixInvariant
calls
CALNil
canonicalName
CantSplit
Case
1 (Data Constructor)
2 (Data Constructor)
3 (Type/Class)
caseSplitSearch
caseSplitSearch'
cat
catchAll
catchAllBranch
catchConstraint
catchError_
catchException
catchImpossible
categorizedecl
catMaybes
cdcont
cddeffreevars
cdecl
cdname
cdorigin
cdtype
CExp
chainl
chainl1
chainl1'
chainr
chainr1
chainr1'
char
1 (Function)
2 (Function)
checkArgs
CheckArguments
checkArguments
checkArguments'
checkArguments_
checkAxiom
CheckClause
checkClause
CheckConstructor
checkConstructor
checkConstructorApplication
checkConstructorType
checkCover
checkCoverage
CheckDataDef
checkDataDef
checkDecl
checkDecls
checkDefinition
CheckDotPattern
checkDotPattern
checkeliminand
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
checkTelescope_
checkTypedBinding
checkTypedBindings
checkTypedBindings_
checkTypedBinding_
checkTypeOfMain
checkTypeSignature
checkWhere
checkWithFunction
Choice
choice
1 (Function)
2 (Function)
choose
1 (Function)
2 (Function)
choosePrioMeta
chop
Chr
Cl
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
ClauseBody
clauseBody
clausebody
clausePats
clausePerm
clauseRange
Clauses
1 (Type/Class)
2 (Data Constructor)
clausesAbove
clauseTel
clauseToFix
clearMetaListeners
clEnv
Clos
1 (Type/Class)
2 (Data Constructor)
closeBrace
ClosedLevel
closify
Closure
1 (Type/Class)
2 (Data Constructor)
Cls
clScope
clSignature
clValue
cm
cmd_auto
cmd_compile
cmd_compute
cmd_compute_toplevel
cmd_constraints
cmd_context
cmd_give
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_show_module_contents
cmd_show_module_contents_toplevel
cmd_solveAll
cmd_write_highlighting_info
CMFBlocked
CMFFlex
CMFlex
1 (Type/Class)
2 (Data Constructor)
CMFSemi
CMode
CmpEq
CmpInType
CmpLeq
CmpLevels
CmpSorts
CmpTeles
CmpTerms
CmpTypes
CMRigid
cnvh
CoArbitrary
coarbitrary
coarbitraryIntegral
coarbitraryReal
coarbitraryShow
Codata
code
CoinductionKit
1 (Type/Class)
2 (Data Constructor)
coinductionKit
CoInductive
CoinductiveDatatype
col
1 (Function)
2 (Function)
coldescr
collect
colon
cols
1 (Function)
2 (Function)
Column
columns
comma
1 (Function)
2 (Function)
Command
command
CommandLineOptions
commandLineOptions
Comment
1 (Type/Class)
2 (Data Constructor)
commutative
commuteM
comp'
compactP
compareArgs
compareAtom
compareLevel
compareSizes
compareSort
compareTel
compareTerm
compareType
Comparison
CompilationError
Compile
compile
1 (Function)
2 (Function)
compileClauses
1 (Function)
2 (Function)
CompiledClauses
CompiledDataPragma
1 (Data Constructor)
2 (Data Constructor)
CompiledEpicPragma
1 (Data Constructor)
2 (Data Constructor)
compileDir
CompiledPragma
1 (Data Constructor)
2 (Data Constructor)
CompiledTypePragma
1 (Data Constructor)
2 (Data Constructor)
compilerMain
1 (Function)
2 (Function)
CompileState
1 (Type/Class)
2 (Data Constructor)
complete
composeP
composePol
compress
CompressedFile
computeEdge
computeNeighbourhood
ComputeOccurrences
computeOccurrences
computePolarity
computeSizeConstraint
Con
1 (Data Constructor)
2 (Data Constructor)
3 (Data Constructor)
conAbstr
ConArgType
conBranches
conCase
concatargs
concatMapM
concatOccurs
ConcreteDef
ConcreteMode
concreteToAbstract
concreteToAbstract_
conData
condecl
conFreq
ConHead
conhqn
conHsCode
conInd
ConMP
ConName
1 (Data Constructor)
2 (Type/Class)
3 (Data Constructor)
ConnectHandle
ConP
1 (Data Constructor)
2 (Data Constructor)
conPars
1 (Function)
2 (Function)
ConPos
Cons
conSrcCon
Const
ConstDef
1 (Type/Class)
2 (Data Constructor)
Constr
1 (Type/Class)
2 (Data Constructor)
Constraint
1 (Type/Class)
2 (Type/Class)
ConstraintClosure
Constraints
1 (Type/Class)
2 (Type/Class)
ConstRef
constrIrr
constrType
Constructor
1 (Data Constructor)
2 (Type/Class)
3 (Type/Class)
4 (Data Constructor)
5 (Data Constructor)
constructorArity
1 (Function)
2 (Function)
constructorForm
constructorImpossible
ConstructorMismatch
constructorMismatch
ConstructorName
ConstructorPatternInWrongDatatype
constructorsInClause
constructorsInClauses
constructPats
constructs
Cont
containsAbsurdPattern
contains_constructor
Context
ContextEntry
contextOfMeta
Continue
continueAfter
ContinueIn
continuous
continuousPerLine
Contravariant
convertLineEndings
copyarg
copyScope
costAbsurdLam
costAddVarDepth
costAppConstructor
costAppConstructorSingle
costAppExtraRef
costAppHint
costAppHintUsed
costAppRecCall
costAppRecCallUsed
costAppVar
costAppVarUsed
costCaseSplitHigh
costCaseSplitLow
costCaseSplitVeryHigh
costEqCong
costEqEnd
costEqStep
costEqSym
costIncrease
costInferredTypeUnkown
costIotaStep
costLam
costLamUnfold
costPi
costSort
costUnification
costUnificationOccurs
count
Covariant
cover
1 (Function)
2 (Function)
CoverageCantSplitOn
CoverageCantSplitType
CoverageFailure
Covering
CoverM
createInterface
createMetaInfo
createModule
CSAbsurd
CSCtx
CSOmittedArg
CSPat
CSPatConApp
CSPatExp
CSPatI
CSPatVar
CSWith
cthandles
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
CurrentDir
CurrentInput
currentModule
currentMutualBlock
curSig
CyclicModuleDependency