Agda-2.2.10: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ:!$&+./<=>|-
Index (I)
iBuiltin
ICArgList
ICExp
icnvh
Id
1 (Data Constructor)
2 (Data Constructor)
Ident
identifier
identity
IdentP
idP
IdPart
idSub
iEnd
If
ifM
IgnoreAbstractMode
ignoreAbstractMode
ignoreBlocking
ignoreForced
ignoreInterfaces
ignoreReduced
iHaskellImports
iHighlighting
ihname
iImportedModules
iInsideScope
IlltypedPattern
IM
iModuleName
ImpInsert
impInsert
ImplicitInsertion
ImplicitP
Import
1 (Data Constructor)
2 (Data Constructor)
ImportDirective
1 (Type/Class)
2 (Data Constructor)
importDirRange
ImportedModule
ImportedName
1 (Type/Class)
2 (Data Constructor)
importedName
importedNameSpace
ImportedNS
ImportPragma
imports
importsForPrim
IMPOSSIBLE
Impossible
1 (Type/Class)
2 (Data Constructor)
ImpossiblePragma
impossibleTerm
impossibleTest
imp_dir
inAbstractMode
inc
InClause
IncompletePattern
IncompletePatternMatching
inConcreteMode
inContext
InDefOf
indent
Independence
independence
Independent
Index
1 (Data Constructor)
2 (Type/Class)
IndexFreeInParameter
IndexVariablesNotDistinct
IndicesNotConstructorApplications
Induction
Inductive
inductiveCheck
Inf
InferDef
inferDef
InferExpr
inferExpr
inferHead
infertypevar
InferVar
infimum
Infinite
infinite
Infix
InfixDef
infixlP
infixP
infixrP
Info
infodecl
infoOnException
initCompileState
initEnv
initGraph
initiate
initMapS
initMeta
initState
1 (Function)
2 (Function)
3 (Function)
Inline
inMutualBlock
inNameSpace
InScope
InScopeTag
inScopeTag
insert
1 (Function)
2 (Function)
3 (Function)
insertImplicit
insertImplicitPatterns
insertImplicitProblem
insertPatterns
insertTele
insertWithKeyM
InsideOperandCtx
insideScope
Instantiate
instantiate
Instantiated
instantiateDef
InstantiateFull
instantiateFull
instantiatePattern
instantiateTel
inState
InstS
InstV
int
integer
integerSemiring
Interaction
1 (Type/Class)
2 (Data Constructor)
interaction
InteractionId
1 (Type/Class)
2 (Data Constructor)
interactionLoop
InteractionPoints
interestingCall
Interface
1 (Type/Class)
2 (Data Constructor)
InternalError
internalError
intersectWith
Interval
1 (Type/Class)
2 (Data Constructor)
intervalInvariant
intMap
introTactic
Inv
InvalidPattern
Invariant
Inverse
inverseScopeLookup
inverseScopeLookupModule
inverseScopeLookupName
invertP
InvView
io
IOException
iotapossmeta
iotastep
ioTCM
ioTCM_
iPragmaOptions
Irr
irrBranch
Irrelevant
irrelevant
IrrelevantDatatype
irrExpr
IrrFilter
irrFilter
irrFilters
irrFun
IsAbstract
isAHole
isBelow
isBindingHole
isBlockedTerm
isCoinductive
iScope
isDatatype
1 (Function)
2 (Function)
IsEmpty
isEmpty
1 (Function)
2 (Function)
3 (Function)
IsEmptyType
isEmptyType
isEmptyTypeC
isEtaExpandable
isEtaRecord
IsExpr
isGeneratedRecordConstructor
isHaskellKind
isHiddenArg
isHole
iSignature
isImported
isIn
isInCase
isIndependent
IsInfix
isInfix
isInModule
isInstantiatedMeta
isInteractionMeta
isInTerm
isIrr
isJust
isLambdaHole
isLeft
isLevelConstraint
isLiterate
isNewerThan
isNoName
isNonfix
isNothing
isntTypeConf
isOperator
1 (Function)
2 (Function)
isPostfix
isPrefix
isProjection
isRec
isRecord
isRecordConstructor
IsReduced
isReduced
isRel
isRight
isSingleton
isSingletonRecord
isSizeType
isSolvedProblem
IsSort
isSortMeta
isString
isSubModuleOf
isSuccess
iStart
isType
IsTypeCall
isTypeConf
IsType_
isType_
isUnicodeId
isVar
isVisited
isWellScoped
isZero
Item
iterate'