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
:
!
$
+
.
/
<
=
>
|
-

Index - I

iBuiltin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ICArgList	Agda.Auto.Syntax
ICExp	Agda.Auto.Syntax
icnvh	Agda.Auto.Convert
Id
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Ident	Agda.Syntax.Concrete
identifier	Agda.Syntax.Parser.LexActions
identity	Agda.Utils.TestHelpers
IdentP	Agda.Syntax.Concrete
idP	Agda.Utils.Permutation
IdPart	Agda.Syntax.Notation
idSub	Agda.TypeChecking.Substitute
iEnd	Agda.Syntax.Position, Agda.Interaction.GhciTop
ifM	Agda.Utils.Monad
IgnoreAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ignoreBlocking	Agda.Syntax.Internal
ignoreForced	Agda.Syntax.Common
ignoreInterfaces	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
iHaskellImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlighting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihname	Agda.Compiler.MAlonzo.Misc
iImportedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IM	Agda.Interaction.Monad
iModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsert	Agda.TypeChecking.Implicit
impInsert	Agda.TypeChecking.Implicit
ImplicitInsertion	Agda.TypeChecking.Implicit
ImplicitP	Agda.Syntax.Abstract
Import
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
ImportDirective
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
importDirRange	Agda.Syntax.Concrete
ImportedModule	Agda.Syntax.Concrete
ImportedName
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
importedName	Agda.Syntax.Concrete
importedNameSpace	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportedNS	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportPragma	Agda.Syntax.Concrete
imports	Agda.Compiler.MAlonzo.Compiler
importsForPrim	Agda.Compiler.MAlonzo.Primitives
Impossible
1 (Type/Class)	Agda.Utils.Impossible
2 (Data Constructor)	Agda.Utils.Impossible
ImpossiblePragma	Agda.Syntax.Concrete
impossibleTerm	Agda.Syntax.Internal
imp_dir	Agda.Syntax.Parser.Lexer
inAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inc	Agda.Utils.Warshall
InClause	Agda.TypeChecking.Positivity
includeDirectories	Agda.Interaction.GhciTop
IncompletePattern	Agda.Interaction.Highlighting.Precise
IncompletePatternMatching	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
InDefOf	Agda.TypeChecking.Positivity
indent	Agda.Utils.String
Index
1 (Data Constructor)	Agda.Utils.Suffix
2 (Type/Class)	Agda.Termination.CallGraph
Induction	Agda.Syntax.Common
Inductive	Agda.Syntax.Common
inductiveCheck	Agda.TypeChecking.Rules.Builtin
Inf	Agda.Syntax.Internal
InferDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferDef	Agda.TypeChecking.Rules.Term
InferExpr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferExpr	Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
inferHead	Agda.TypeChecking.Rules.Term
infertypevar	Agda.Auto.CaseSplit
InferVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
infimum	Agda.Termination.CallGraph
Infinite	Agda.Utils.Warshall
infinite	Agda.Utils.Warshall
Infix	Agda.Syntax.Concrete
InfixDef	Agda.Syntax.Common
infixlP	Agda.Syntax.Concrete.Operators.Parser
infixP	Agda.Syntax.Concrete.Operators.Parser
infixrP	Agda.Syntax.Concrete.Operators.Parser
Info	Agda.Syntax.Info
infodecl	Agda.Compiler.MAlonzo.Compiler
infoOnException	Agda.Interaction.GhciTop
initEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraph	Agda.Utils.Warshall
initMapS	Agda.Auto.Convert
initMeta	Agda.Auto.NarrowingSearch
initState
1 (Function)	Agda.Syntax.Parser.Monad
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Function)	Agda.Interaction.GhciTop
inMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpace	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScope	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeTag	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inScopeTag	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
insert
1 (Function)	Agda.Utils.Graph
2 (Function)	Agda.Utils.Trie
3 (Function)	Agda.Termination.CallGraph
insertImplicit	Agda.TypeChecking.Implicit
insertImplicitPatterns	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblem	Agda.TypeChecking.Rules.LHS.Implicit
insertPatterns	Agda.TypeChecking.Rules.Def
insertWithKeyM	Agda.Utils.Map
InsideOperandCtx	Agda.Syntax.Fixity
insideScope	Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
Instantiate	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiate	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
Instantiated	Agda.Interaction.BasicOps
instantiateDef	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFull	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateFull	Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiatePattern	Agda.TypeChecking.Rules.LHS
instantiateTel	Agda.TypeChecking.Rules.LHS.Instantiate
inState	Agda.Syntax.Parser.LexActions
InstS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstV	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
int	Agda.Utils.Pretty
integer	Agda.Utils.Pretty
integerSemiring	Agda.Termination.Semiring
Interaction
1 (Type/Class)	Agda.Interaction.GhciTop
2 (Data Constructor)	Agda.Interaction.GhciTop
interaction	Agda.Interaction.CommandLine.CommandLine
InteractionId
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interactionLoop	Agda.Interaction.CommandLine.CommandLine
InteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interestingCall	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
Interface
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InternalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
intersectWith	Agda.Termination.SparseMatrix
Interval
1 (Type/Class)	Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)	Agda.Syntax.Position, Agda.Interaction.GhciTop
intervalInvariant	Agda.Syntax.Position, Agda.Interaction.GhciTop
intMap	Agda.Utils.Warshall
introTactic	Agda.Interaction.BasicOps
Inv	Agda.TypeChecking.Injectivity
InvalidPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Invariant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Inverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseScopeLookup	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupModule	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupName	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
invertP	Agda.Utils.Permutation
InvView	Agda.TypeChecking.Injectivity
io	Agda.TypeChecking.Primitive
IOException	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotapossmeta	Agda.Auto.Typecheck
iotastep	Agda.Auto.Typecheck
ioTCM	Agda.Interaction.GhciTop
ioTCM_	Agda.Interaction.GhciTop
iPragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Irrelevant	Agda.Syntax.Common
IrrelevantDatatype	Agda.TypeChecking.Coverage
IsAbstract	Agda.Syntax.Common
isAHole	Agda.Syntax.Notation
isBelow	Agda.Utils.Warshall
isBindingHole	Agda.Syntax.Notation
isBlockedTerm	Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isCoinductive	Agda.TypeChecking.Rules.Data
iScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isDatatype
1 (Function)	Agda.TypeChecking.Datatypes
2 (Function)	Agda.TypeChecking.Coverage
IsEmpty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Termination.SparseMatrix
3 (Function)	Agda.Termination.Matrix
IsEmptyType	Agda.Interaction.BasicOps
isEmptyType	Agda.TypeChecking.Empty
isEmptyTypeC	Agda.TypeChecking.Empty
isEtaExpandable	Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isEtaRecord	Agda.TypeChecking.Records
IsExpr	Agda.Syntax.Concrete.Operators.Parser
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isHaskellKind	Agda.Compiler.HaskellTypes
isHiddenArg	Agda.Syntax.Common
isHole	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
iSignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isImported	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isIndependent	Agda.Interaction.GhciTop
IsInfix	Agda.Syntax.Common
isInfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInModule	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isInstantiatedMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInteractionMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isJust	Agda.Utils.Maybe
isLambdaHole	Agda.Syntax.Notation
isLeft	Agda.Utils.Either
isLevelConstraint	Agda.TypeChecking.UniversePolymorphism
isLiterate	Agda.Interaction.Options
isNewerThan	Agda.Interaction.Imports
isNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothing	Agda.Utils.Maybe
isntTypeConf	Agda.TypeChecking.Test.Generators
isOperator
1 (Function)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isPostfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isRecord	Agda.TypeChecking.Records
isRight	Agda.Utils.Either
isSingleton	Agda.Termination.SparseMatrix
isSingletonRecord	Agda.TypeChecking.Records
isSizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblem	Agda.TypeChecking.Rules.LHS
IsSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isString	Agda.Utils.Generics
isSubModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isSuccess	Agda.Utils.QuickCheck
iStart	Agda.Syntax.Position, Agda.Interaction.GhciTop
isType	Agda.TypeChecking.Rules.Term
IsTypeCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConf	Agda.TypeChecking.Test.Generators
IsType_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_	Agda.TypeChecking.Rules.Term
isUnicodeId	Agda.Utils.Unicode
isVar	Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isVisited	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScoped	Agda.TypeChecking.Test.Generators
isZero	Agda.Utils.TestHelpers
Item	Agda.TypeChecking.Positivity
iterate'	Agda.Utils.Function