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 - I

iBuiltin	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ICArgList	Agda.Auto.Syntax
ICExp	Agda.Auto.Syntax
icnvh	Agda.Auto.Convert
ICODE	Agda.TypeChecking.Serialise.Base
icode	Agda.TypeChecking.Serialise.Base
icodeArgs	Agda.TypeChecking.Serialise.Base
icodeDouble	Agda.TypeChecking.Serialise.Base
icodeInteger	Agda.TypeChecking.Serialise.Base
icodeMemo	Agda.TypeChecking.Serialise.Base
icodeN	Agda.TypeChecking.Serialise.Base
icodeN'	Agda.TypeChecking.Serialise.Base
icodeNode	Agda.TypeChecking.Serialise.Base
icodeString	Agda.TypeChecking.Serialise.Base
icodeX	Agda.TypeChecking.Serialise.Base
icod_	Agda.TypeChecking.Serialise.Base
Id
1 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Auto.Syntax
idempotent	Agda.Termination.Termination
Ident
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
identifier	Agda.Syntax.Parser.LexActions
IdentP	Agda.Syntax.Concrete
IdiomBrackets	Agda.Syntax.Concrete
iDisplayForms	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
idP	Agda.Utils.Permutation
IdPart	Agda.Syntax.Notation
IdS	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
idS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
iEnd	Agda.Syntax.Position
If
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
3 (Type/Class)	Agda.Utils.TypeLevel
ifBlocked	Agda.TypeChecking.Reduce
ifBlockedType	Agda.TypeChecking.Reduce
ifDirty	Agda.Utils.Update
ifJust	Agda.Utils.Maybe
ifJustM
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
ifLe	Agda.TypeChecking.SizedTypes.Syntax
ifM	Agda.Utils.Monad
ifNoConstraints	Agda.TypeChecking.Constraints
ifNoConstraints_	Agda.TypeChecking.Constraints
ifNotM	Agda.Utils.Monad
ifNotPi	Agda.TypeChecking.Telescope
ifNotPiType	Agda.TypeChecking.Telescope
ifNull	Agda.Utils.Null
ifNullM	Agda.Utils.Null
iForeignCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifPi	Agda.TypeChecking.Telescope
ifPiType	Agda.TypeChecking.Telescope
IFSNoCandidateInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifTopLevelAndHighlightingLevelIs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifTopLevelAndHighlightingLevelIsOr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iFullHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreAbstract	Agda.Interaction.BasicOps
IgnoreAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreAll
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
IgnoreAllWarnings	Agda.Interaction.Options
ignoreBlocking	Agda.Syntax.Internal
IgnoreFlags
1 (Type/Class)	Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options
ignoreForced	Agda.Syntax.Common
IgnoreInAnnotations
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
ignoreInterfaces	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreNot
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
ignoreReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreSharing	Agda.Syntax.Internal
ignoreSharingType	Agda.Syntax.Internal
IgnoreSorts
1 (Type/Class)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Type/Class)	Agda.TypeChecking.Free.Old
iHighlighting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ihname	Agda.Compiler.MAlonzo.Misc
iImportedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iInsideScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iLength	Agda.Syntax.Position
IllegalLetInTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedProjectionPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
illiterate	Agda.Syntax.Parser.Literate
IlltypedPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad, Agda.Compiler.Backend
iModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ImpInsert	Agda.TypeChecking.Implicit
impInsert	Agda.TypeChecking.Implicit
implicitArgs	Agda.TypeChecking.Implicit
ImplicitFlex	Agda.TypeChecking.Rules.LHS.Problem
ImplicitInsertion	Agda.TypeChecking.Implicit
implicitNamedArgs	Agda.TypeChecking.Implicit
implicitP	Agda.TypeChecking.Rules.LHS.Implicit
implies	Agda.TypeChecking.SizedTypes.WarshallSolver
Import
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
3 (Data Constructor)	Agda.Syntax.Abstract
ImportDecl
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Utils.Haskell.Syntax
ImportDirective
1 (Data Constructor)	Agda.Syntax.Common
2 (Type/Class)	Agda.Syntax.Concrete
3 (Type/Class)	Agda.Syntax.Abstract
ImportDirective'	Agda.Syntax.Common
importDirRange	Agda.Syntax.Common
ImportedModule	Agda.Syntax.Common
ImportedName
1 (Data Constructor)	Agda.Syntax.Common
2 (Type/Class)	Agda.Syntax.Concrete
3 (Type/Class)	Agda.Syntax.Abstract
ImportedName'	Agda.Syntax.Common
ImportedNS	Agda.Syntax.Scope.Base
importModule	Agda.Utils.Haskell.Syntax
ImportPragma	Agda.Syntax.Concrete
importQualified	Agda.Utils.Haskell.Syntax
imports	Agda.Compiler.MAlonzo.Compiler
importsForPrim	Agda.Compiler.MAlonzo.Primitives
ImportSpec	Agda.Utils.Haskell.Syntax
importSpecs	Agda.Utils.Haskell.Syntax
ImportUHCPragma	Agda.Syntax.Concrete
Impossible
1 (Type/Class)	Agda.Utils.Impossible
2 (Data Constructor)	Agda.Utils.Impossible
ImpossibleConstructor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ImpossiblePragma	Agda.Syntax.Concrete
impossibleTerm	Agda.Syntax.Internal
impossibleTest	Agda.ImpossibleTest
impRenaming	Agda.Syntax.Common
imp_dir	Agda.Syntax.Parser.Lexer
In	Agda.Syntax.Concrete.Operators.Parser
inAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inc	Agda.Utils.Warshall
InClause	Agda.TypeChecking.Positivity.Occurrence
includes	Agda.TypeChecking.Serialise.Base
includeStateChanges	Agda.Interaction.Imports
Inclusion
1 (Type/Class)	Agda.Utils.PartialOrd
2 (Data Constructor)	Agda.Utils.PartialOrd
inclusion	Agda.Utils.PartialOrd
incoming	Agda.TypeChecking.SizedTypes.WarshallSolver
inCompilerEnv	Agda.Compiler.Common
IncompletePattern	Agda.Interaction.Highlighting.Precise
inConcreteMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inConcreteOrAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
increase	Agda.Termination.Order
IndArgType	Agda.TypeChecking.Positivity.Occurrence
InDefOf	Agda.TypeChecking.Positivity.Occurrence
indent	Agda.Utils.String
independent	Agda.Interaction.InteractionTop
Index
1 (Type/Class)	Agda.Utils.IndexedList
2 (Data Constructor)	Agda.Utils.Suffix
Indirect	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Induction	Agda.Syntax.Common
Inductive	Agda.Syntax.Common
Inf	Agda.Syntax.Internal
inf	Agda.TypeChecking.Positivity
infer	Agda.TypeChecking.CheckInternal
InferDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferDef	Agda.TypeChecking.Rules.Term
InferExpr	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferExpr	Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker
inferExpr'	Agda.TypeChecking.Rules.Term
inferExprForWith	Agda.TypeChecking.Rules.Term
inferHead	Agda.TypeChecking.Rules.Term
inferHeadDef	Agda.TypeChecking.Rules.Term
inferMeta	Agda.TypeChecking.Rules.Term
inferOrCheckProjApp	Agda.TypeChecking.Rules.Term
inferProjApp	Agda.TypeChecking.Rules.Term
Inferred	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferSort	Agda.TypeChecking.CheckInternal
infertypevar	Agda.Auto.CaseSplit
InferVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
infimum	Agda.Termination.Order
Infinite	Agda.Utils.Warshall
infinite	Agda.Utils.Warshall
Infinity	Agda.TypeChecking.SizedTypes.WarshallSolver
infinityFlexs	Agda.TypeChecking.SizedTypes.WarshallSolver
Infix	Agda.Syntax.Concrete
InfixApp	Agda.Utils.Haskell.Syntax
InfixDef	Agda.Syntax.Common
InfixNotation	Agda.Syntax.Notation
infodecl	Agda.Compiler.MAlonzo.Compiler
Info_AllGoalsWarnings	Agda.Interaction.Response
Info_Auto	Agda.Interaction.Response
Info_CompilationOk	Agda.Interaction.Response
Info_Constraints	Agda.Interaction.Response
Info_Context	Agda.Interaction.Response
Info_CurrentGoal	Agda.Interaction.Response
Info_Error	Agda.Interaction.Response
Info_GoalType	Agda.Interaction.Response
Info_HelperFunction	Agda.Interaction.Response
Info_InferredType	Agda.Interaction.Response
Info_Intro	Agda.Interaction.Response
Info_ModuleContents	Agda.Interaction.Response
Info_NormalForm	Agda.Interaction.Response
Info_SearchAbout	Agda.Interaction.Response
Info_Time	Agda.Interaction.Response
Info_Version	Agda.Interaction.Response
Info_WhyInScope	Agda.Interaction.Response
inFreshModuleIfFreeParams	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Infty	Agda.TypeChecking.SizedTypes.Syntax
initAutoOptions	Agda.Auto.Options
initCCEnv	Agda.Compiler.MAlonzo.Compiler
initCommandState	Agda.Interaction.InteractionTop
initCopyInfo	Agda.Syntax.Abstract
initEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initExpRefInfo	Agda.Auto.SearchControl
initFreeEnv	Agda.TypeChecking.Free.Lazy
initGraph	Agda.Utils.Warshall
initialDotState	Agda.Interaction.Highlighting.Dot
initialIFSCandidates	Agda.TypeChecking.InstanceArguments
initialiseCommandQueue	Agda.Interaction.InteractionTop
initLast	Agda.Utils.List
initMapS	Agda.Auto.Convert
initMeta	Agda.Auto.NarrowingSearch
initOccursCheck	Agda.TypeChecking.MetaVars.Occurs
initPersistentState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initPostScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initPreScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initState
1 (Function)	Agda.Syntax.Parser.Monad
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InjectivePragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
Injectivity	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InlinePragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
InlineReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inlineWithClauses	Agda.Termination.Inlining
inMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inNameSpace	Agda.Syntax.Scope.Base
inOriginalContext	Agda.TypeChecking.Unquote
inplaceS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
inputFlag	Agda.Interaction.Options
InScope	Agda.Syntax.Scope.Base
inScopeBecause	Agda.Syntax.Scope.Base
InScopeSet	Agda.Syntax.Scope.Base
InScopeTag	Agda.Syntax.Scope.Base
inScopeTag	Agda.Syntax.Scope.Base
InSeq
1 (Type/Class)	Agda.Compiler.Treeless.Subst
2 (Data Constructor)	Agda.Compiler.Treeless.Subst
inSeq	Agda.Compiler.Treeless.Subst
insert
1 (Function)	Agda.Utils.BiMap
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Bag
4 (Function)	Agda.Utils.Trie
5 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)	Agda.Utils.Favorites
7 (Function)	Agda.Utils.AssocList
8 (Function)	Agda.Termination.CallMatrix
9 (Function)	Agda.Termination.CallGraph
insertAfter	Agda.Compiler.JS.Compiler
insertCompared	Agda.Utils.Favorites
Inserted	Agda.Syntax.Common
insertEdge
1 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)	Agda.TypeChecking.SizedTypes.WarshallSolver
insertEdgeWith	Agda.Utils.Graph.AdjacencyMap.Unidirectional
insertHiddenLambdas	Agda.TypeChecking.Rules.Term
insertImplicit	Agda.TypeChecking.Implicit
insertImplicitPatSynArgs	Agda.Syntax.Abstract
insertImplicitPatterns	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitPatternsT	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblem	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitSizeLtPatterns	Agda.TypeChecking.Rules.LHS.Implicit
insertMissingFields	Agda.TypeChecking.Records
insertMutualBlockInfo	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertOldInteractionScope	Agda.Interaction.InteractionTop
insertPatterns	Agda.TypeChecking.Rules.Def
insertWith
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Trie
3 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
insertWithKeyM	Agda.Utils.Map
insideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InsideOperandCtx	Agda.Syntax.Fixity
insidePi	Agda.TypeChecking.InstanceArguments
Instance	Agda.Syntax.Common
InstanceArg	Agda.Syntax.Concrete
InstanceArgV	Agda.Syntax.Concrete.Operators.Parser
InstanceB	Agda.Syntax.Concrete
InstanceDef	Agda.Syntax.Common
InstanceP	Agda.Syntax.Concrete
InstanceSearchDepthExhausted	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceTable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instanceTransformBiMT'	Agda.Utils.Geniplate
instanceUniverseBiT'	Agda.Utils.Geniplate
Instantiable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Instantiate	Agda.TypeChecking.Reduce
instantiate	Agda.TypeChecking.Reduce
instantiate'	Agda.TypeChecking.Reduce
Instantiated	Agda.Interaction.BasicOps
instantiateDef	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateDefinitionType	Agda.TypeChecking.Rules.Decl
InstantiateFull	Agda.TypeChecking.Reduce
instantiateFull	Agda.TypeChecking.Reduce
instantiateFull'	Agda.TypeChecking.Reduce
instantiateRewriteRule	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateRewriteRules	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateTel	Agda.TypeChecking.Rules.LHS.Instantiate
instantiateTelescope	Agda.TypeChecking.Telescope
inState	Agda.Syntax.Parser.LexActions
InstV	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Int	Agda.Utils.Haskell.Syntax
int
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Compiler.Treeless.EliminateLiteralPatterns
Integer	Agda.Compiler.JS.Syntax
integer	Agda.Utils.Pretty
integerC	Agda.TypeChecking.Serialise.Base
integerD	Agda.TypeChecking.Serialise.Base
integerE	Agda.TypeChecking.Serialise.Base
integerSemiring	Agda.Termination.Semiring
Interaction	Agda.Interaction.InteractionTop
interaction	Agda.Interaction.CommandLine
Interaction'	Agda.Interaction.InteractionTop
InteractionId
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
interactionId	Agda.Syntax.Common
interactionLoop	Agda.Interaction.CommandLine
InteractionOutputCallback	Agda.Interaction.Response
InteractionPoint
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Interactive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interAssocWith	Agda.Termination.SparseMatrix
interestingCall	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Interface
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interleaveRanges	Agda.Syntax.Position
InternalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
internalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interpret	Agda.Interaction.InteractionTop
interpretWarnings	Agda.Interaction.InteractionTop
intersection
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
intersectionWith	Agda.Utils.HashMap
intersectionWithKey	Agda.Utils.HashMap
intersectVars	Agda.TypeChecking.Conversion
intersectWith	Agda.Termination.SparseMatrix
Interval
1 (Type/Class)	Agda.Syntax.Position
2 (Data Constructor)	Agda.Syntax.Position
interval	Agda.Syntax.Parser.Literate
Interval'	Agda.Syntax.Position
intervalInvariant	Agda.Syntax.Position
intervalsToRange	Agda.Syntax.Position
intervalToRange	Agda.Syntax.Position
IntervalWithoutFile	Agda.Syntax.Position
intMap	Agda.Utils.Warshall
inTopContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Intro	Agda.Interaction.InteractionTop
intros	Agda.Compiler.MAlonzo.Compiler
introTactic	Agda.Interaction.BasicOps
intSemiring	Agda.Termination.Semiring
intView	Agda.Syntax.Treeless, Agda.Compiler.Backend
Inv	Agda.TypeChecking.Injectivity
InvalidCatchallPragma	Agda.Syntax.Concrete.Definitions
InvalidExtensionError	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
InvalidMeasureMutual	Agda.Syntax.Concrete.Definitions
InvalidName	Agda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTerminationCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTypeSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Invariant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Inverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inverseApplyRelevance	Agda.TypeChecking.Irrelevance
inverseComposeRelevance	Agda.Syntax.Common
InversePermute	Agda.Utils.Permutation
inversePermute	Agda.Utils.Permutation
InverseScopeLookup	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
inverseScopeLookup	Agda.Syntax.Scope.Base
inverseScopeLookup'	Agda.Syntax.Scope.Base
inverseScopeLookupModule	Agda.Syntax.Scope.Base
inverseScopeLookupName	Agda.Syntax.Scope.Base
inverseScopeLookupName'	Agda.Syntax.Scope.Base
inverseSubst	Agda.TypeChecking.MetaVars
InvertExcept	Agda.TypeChecking.MetaVars
invertP	Agda.Utils.Permutation
invLookup	Agda.Utils.BiMap
InvView	Agda.TypeChecking.Injectivity
io	Agda.TypeChecking.Primitive
IOException	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IORef	Agda.Utils.IORef
iotapossmeta	Agda.Auto.Typecheck
iotastep	Agda.Auto.Typecheck
IOTCM
1 (Data Constructor)	Agda.Interaction.InteractionTop
2 (Type/Class)	Agda.Interaction.InteractionTop
IOTCM'	Agda.Interaction.InteractionTop
iPatternSyns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcClauseNo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPClause
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcQName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipMeta	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPNoClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iPragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipSolved	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Irrel	Agda.TypeChecking.MetaVars.Occurs
Irrelevant	Agda.Syntax.Common
irrelevant	Agda.Syntax.Common
IrrelevantDatatype	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Irrelevantly
1 (Data Constructor)	Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
irrelevantVars
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
irrToNonStrict	Agda.Syntax.Common
IsAbstract	Agda.Syntax.Common
isAbsurdBody	Agda.Syntax.Internal
isAbsurdLambdaName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isAbsurdPatternName	Agda.Syntax.Internal
isAHole	Agda.Syntax.Notation
isAlias	Agda.TypeChecking.Rules.Def
IsAlpha	Agda.Utils.Char
IsAlphaNum	Agda.Utils.Char
isAnonymousModuleName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isApplyElim	Agda.Syntax.Internal
IsBase	Agda.Utils.TypeLevel
isBelow	Agda.Utils.Warshall
isBenchmarkOn	Agda.Utils.Benchmark
isBinderUsed
1 (Function)	Agda.TypeChecking.Free
2 (Function)	Agda.TypeChecking.Free.Old
isBindingHole	Agda.Syntax.Notation
isBlockedTerm	Agda.TypeChecking.MetaVars
IsBothfix	Agda.Utils.List
isBounded	Agda.TypeChecking.SizedTypes
isBuiltin	Agda.TypeChecking.Primitive
isCached	Agda.Interaction.Imports
isClosed	Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCode	Agda.Syntax.Parser.Literate
isCodeLayer	Agda.Syntax.Parser.Literate
isCoinductive	Agda.TypeChecking.Rules.Data
isCoinductiveProjection	Agda.Termination.Monad
isCon	Agda.TypeChecking.Unquote
IsControl	Agda.Utils.Char
isCopatternLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCovered	Agda.TypeChecking.Coverage
IsData	Agda.Syntax.Common
isDataOrRecord	Agda.TypeChecking.Datatypes
isDataOrRecordType	Agda.TypeChecking.Datatypes
isDatatype	Agda.TypeChecking.Datatypes
isDatatypeModule	Agda.Syntax.Scope.Monad
isDecr	Agda.Termination.Order
isDef	Agda.TypeChecking.Unquote
isDefAccount	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isDefaultImportDir	Agda.Syntax.Common
IsDigit	Agda.Utils.Char
IsDominated	Agda.Utils.Favorites
IsEmpty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isEmpty
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Termination.SparseMatrix
isEmptyFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isEmptyObject	Agda.Compiler.JS.Compiler
IsEmptyType	Agda.Interaction.BasicOps
isEmptyType	Agda.TypeChecking.Empty
isEnabled	Agda.Compiler.Backend
isEqualityType	Agda.Syntax.Internal
isEtaCon	Agda.TypeChecking.Records
isEtaExpandable	Agda.TypeChecking.MetaVars
isEtaRecord	Agda.TypeChecking.Records
isEtaRecordType	Agda.TypeChecking.Records
IsExpr	Agda.Syntax.Concrete.Operators.Parser
IsFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexNode	Agda.TypeChecking.SizedTypes.WarshallSolver
isFrozen	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isFullyInstantiatedMeta	Agda.TypeChecking.Reduce
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isGlobal	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isHackReifyToMeta	Agda.Syntax.Internal
IsHexDigit	Agda.Utils.Char
isHole	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isIFSConstraint	Agda.TypeChecking.InstanceArguments
iSignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isImported	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInductiveRecord	Agda.TypeChecking.Records
IsInfix	Agda.Syntax.Common
isInfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInftyNode	Agda.TypeChecking.SizedTypes.WarshallSolver
isInlineFun	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInModule	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isInsideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsInstance	Agda.Syntax.Common
isInstance	Agda.Syntax.Common
IsInstantiatedMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInstantiatedMeta
1 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)	Agda.TypeChecking.Reduce.Monad
isInstantiatedMeta'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInteractionMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInternalAccount	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isIrrelevant	Agda.Syntax.Common
isJust
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
isLambdaHole	Agda.Syntax.Notation
isLeft	Agda.Utils.Either
IsLetter	Agda.Utils.Char
IsLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isLiterate	Agda.Interaction.Options
isLocal	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsLower	Agda.Utils.Char
IsMacro	Agda.Syntax.Common
isMacro	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsMain
1 (Type/Class)	Agda.Compiler.Common, Agda.Compiler.Backend
2 (Data Constructor)	Agda.Compiler.Common, Agda.Compiler.Backend
isMainFunction	Agda.Compiler.MAlonzo.Primitives
IsMark	Agda.Utils.Char
isModChar	Agda.Compiler.MAlonzo.Misc
isModuleAccount	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isModuleFreeVar	Agda.TypeChecking.Rules.Term
isNameInScope	Agda.Syntax.Scope.Base
isNeutral	Agda.TypeChecking.MetaVars.Occurs
isNewerThan	Agda.Interaction.Imports
isNo	Agda.TypeChecking.InstanceArguments
IsNofix	Agda.Utils.List
IsNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isNonfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNormalHole	Agda.Syntax.Notation
isNothing
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
IsNumber	Agda.Utils.Char
IsOctDigit	Agda.Utils.Char
isOpenMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isOperator
1 (Function)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
3 (Function)	Agda.Compiler.MAlonzo.Pretty
isOrder	Agda.Termination.Order
iSourceHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isOverlappable	Agda.Syntax.Common
IsPatSyn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPostfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsPrefix	Agda.Utils.List
isPrefix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsPrefixOf	Agda.TypeChecking.Abstract
isPrefixOf	Agda.TypeChecking.Abstract
isPrimEq	Agda.Syntax.Treeless, Agda.Compiler.Backend
IsPrint	Agda.Utils.Char
isProblemSolved	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjectionButNotCoinductive	Agda.Termination.Monad
isProjection_	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsProjElim	Agda.Syntax.Internal
isProjElim	Agda.Syntax.Internal
IsProjP	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isProjP	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isProperProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsPunctuation	Agda.Utils.Char
isQName	Agda.Interaction.BasicOps
isQualified	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsRecord	Agda.Syntax.Common
isRecord	Agda.TypeChecking.Records
isRecordConstructor	Agda.TypeChecking.Records
isRecordType	Agda.TypeChecking.Records
isRecursiveRecord	Agda.TypeChecking.Records
IsReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isRelevant	Agda.Syntax.Common
isRight	Agda.Utils.Either
isRigid	Agda.TypeChecking.InstanceArguments
IsSeparator	Agda.Utils.Char
isSet	Agda.Syntax.Abstract.Views
isSingleton	Agda.Termination.SparseMatrix
isSingletonRecord	Agda.TypeChecking.Records
isSingletonRecord'	Agda.TypeChecking.Records
isSingletonRecordModuloRelevance	Agda.TypeChecking.Records
isSingletonType	Agda.TypeChecking.Records
isSingletonType'	Agda.TypeChecking.Records
isSingletonTypeModuloRelevance	Agda.TypeChecking.Records
isSizeConstraint	Agda.TypeChecking.SizedTypes
isSizeNameTest	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeNameTestRaw	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeProblem	Agda.TypeChecking.SizedTypes
IsSizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeTypeTest	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSolvedProblem	Agda.TypeChecking.Rules.LHS
isSolvingConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSort	Agda.Syntax.Internal
isSortMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSortMeta_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsSpace	Agda.Utils.Char
isStaticFun	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSublistOf	Agda.Utils.List
isSubModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isSubscriptDigit	Agda.Utils.Suffix
isSubsetOf	Agda.Utils.VarSet
IsSuffix	Agda.Utils.List
IsSymbol	Agda.Utils.Char
iStart	Agda.Syntax.Position
isTop	Agda.TypeChecking.SizedTypes.Utils
isTopLevelValue	Agda.Compiler.JS.Compiler
isTrivialPattern	Agda.TypeChecking.Coverage.Match
isType	Agda.TypeChecking.Rules.Term
IsTypeCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isTypeEqualTo	Agda.TypeChecking.Rules.Term
IsType_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isType_	Agda.TypeChecking.Rules.Term
isUnderscore	Agda.Syntax.Common
isUnreachable	Agda.Syntax.Treeless, Agda.Compiler.Backend
isUnsolvedWarning	Agda.TypeChecking.Warnings
isUntypedBuiltin	Agda.TypeChecking.Rules.Builtin
IsUpper	Agda.Utils.Char
isValidJSIdent	Agda.Compiler.JS.Pretty
isVar	Agda.TypeChecking.CompiledClause.Compile
IsVarSet	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isVisited	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isWithFunction	Agda.Termination.Inlining
isZeroNode	Agda.TypeChecking.SizedTypes.WarshallSolver
Item	Agda.TypeChecking.Positivity
iterate'	Agda.Utils.Function
iterateSolver	Agda.TypeChecking.SizedTypes.WarshallSolver
iterateUntil	Agda.Utils.Function
iterateUntilM	Agda.Utils.Function
iterWhile	Agda.Utils.Function
IVar	Agda.Utils.Haskell.Syntax
iWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend