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
ICArgList	Agda.Auto.Syntax
ICExp	Agda.Auto.Syntax
icnvh	Agda.Auto.Convert
icode	Agda.TypeChecking.Serialise.Base
icode0	Agda.TypeChecking.Serialise.Base
icode0'	Agda.TypeChecking.Serialise.Base
icode1	Agda.TypeChecking.Serialise.Base
icode1'	Agda.TypeChecking.Serialise.Base
icode10	Agda.TypeChecking.Serialise.Base
icode10'	Agda.TypeChecking.Serialise.Base
icode11	Agda.TypeChecking.Serialise.Base
icode11'	Agda.TypeChecking.Serialise.Base
icode12	Agda.TypeChecking.Serialise.Base
icode12'	Agda.TypeChecking.Serialise.Base
icode13	Agda.TypeChecking.Serialise.Base
icode13'	Agda.TypeChecking.Serialise.Base
icode14	Agda.TypeChecking.Serialise.Base
icode14'	Agda.TypeChecking.Serialise.Base
icode15	Agda.TypeChecking.Serialise.Base
icode2	Agda.TypeChecking.Serialise.Base
icode2'	Agda.TypeChecking.Serialise.Base
icode3	Agda.TypeChecking.Serialise.Base
icode3'	Agda.TypeChecking.Serialise.Base
icode4	Agda.TypeChecking.Serialise.Base
icode4'	Agda.TypeChecking.Serialise.Base
icode5	Agda.TypeChecking.Serialise.Base
icode5'	Agda.TypeChecking.Serialise.Base
icode6	Agda.TypeChecking.Serialise.Base
icode6'	Agda.TypeChecking.Serialise.Base
icode7	Agda.TypeChecking.Serialise.Base
icode7'	Agda.TypeChecking.Serialise.Base
icode8	Agda.TypeChecking.Serialise.Base
icode8'	Agda.TypeChecking.Serialise.Base
icode9	Agda.TypeChecking.Serialise.Base
icode9'	Agda.TypeChecking.Serialise.Base
icodeDouble	Agda.TypeChecking.Serialise.Base
icodeInteger	Agda.TypeChecking.Serialise.Base
icodeMemo	Agda.TypeChecking.Serialise.Base
icodeN	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
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 (Data Constructor)	Agda.Compiler.Epic.AuxAST
ifBlocked	Agda.TypeChecking.Reduce
ifBlockedType	Agda.TypeChecking.Reduce
ifDirty	Agda.Utils.Update
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
ifPi	Agda.TypeChecking.Telescope
ifPiType	Agda.TypeChecking.Telescope
IFSNoCandidateInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iFullHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IgnoreAbstract	Agda.Interaction.BasicOps
IgnoreAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IgnoreAll
1 (Data Constructor)	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
ignoreBlocking	Agda.Syntax.Internal
IgnoreFlags
1 (Type/Class)	Agda.Interaction.Options
2 (Data Constructor)	Agda.Interaction.Options
ignoreForced
1 (Function)	Agda.Syntax.Common
2 (Function)	Agda.Compiler.Epic.Erasure
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
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
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
iHaskellCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHaskellImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHaskellImportsUHC	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
iLength	Agda.Syntax.Position
IllegalLetInTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IllformedProjectionPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
illiterate	Agda.Syntax.Parser.Literate
IlltypedPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad
iModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
importedModules	Agda.Compiler.Epic.CompileState
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	Agda.Compiler.Epic.AuxAST
Impossible
1 (Type/Class)	Agda.Utils.Impossible
2 (Data Constructor)	Agda.Utils.Impossible
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
inc	Agda.Utils.Warshall
InClause	Agda.TypeChecking.Positivity.Occurrence
includes	Agda.TypeChecking.Serialise.Base
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
IncompletePatternMatching	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inConcreteOrAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
increase	Agda.Termination.Order
IndArgType	Agda.TypeChecking.Positivity.Occurrence
InDefOf	Agda.TypeChecking.Positivity.Occurrence
indent	Agda.Utils.String
independent	Agda.Interaction.InteractionTop
Index	Agda.Utils.Suffix
IndexVariablesNotDistinct	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesFreeInParameters	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesNotConstructorApplications	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Indirect	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Induction	Agda.Syntax.Common
Inductive	Agda.Syntax.Common
Inf	Agda.Syntax.Internal
inf	Agda.TypeChecking.Positivity
infer	Agda.TypeChecking.CheckInternal
inferable	Agda.Compiler.Epic.Smashing
inferableTerm	Agda.Compiler.Epic.Smashing
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.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
infertypevar	Agda.Auto.CaseSplit
InferVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
Infty	Agda.TypeChecking.SizedTypes.Syntax
initCCEnv	Agda.Compiler.MAlonzo.Compiler
initCommandState	Agda.Interaction.InteractionTop
initCompileState	Agda.Compiler.Epic.CompileState
initCopyInfo	Agda.Syntax.Abstract
initEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initFreeEnv	Agda.TypeChecking.Free.Lazy
initGraph	Agda.Utils.Warshall
initialDotState	Agda.Interaction.Highlighting.Dot
initialIFSCandidates	Agda.TypeChecking.InstanceArguments
initialPrims	Agda.Compiler.Epic.Primitive
initialRels	Agda.Compiler.Epic.Erasure
initialTags	Agda.Compiler.Epic.Injection
initiate	Agda.Compiler.Epic.Erasure
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
initPostScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initPreScopeState	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initState
1 (Function)	Agda.Syntax.Parser.Monad
2 (Function)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
injArg	Agda.Compiler.Epic.Interface
injArity	Agda.Compiler.Epic.Interface
InjConstraints	Agda.Compiler.Epic.Injection
Injectible	Agda.Compiler.Epic.Injection
InjectiveFun
1 (Type/Class)	Agda.Compiler.Epic.Interface
2 (Data Constructor)	Agda.Compiler.Epic.Interface
injectiveFuns	Agda.Compiler.Epic.Interface
Injectivity	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
Inline	Agda.Compiler.Epic.AuxAST
InlinePragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
InlineReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inlineWithClauses	Agda.Termination.Inlining
inMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
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.HashMap
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.Bag
4 (Function)	Agda.Utils.Favorites
5 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)	Agda.Utils.Trie
7 (Function)	Agda.Utils.AssocList
8 (Function)	Agda.Termination.CallMatrix
9 (Function)	Agda.Termination.CallGraph
insertAfter	Agda.Compiler.JS.Compiler
insertAt	Agda.Compiler.Epic.Injection
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
insertOldInteractionScope	Agda.Interaction.InteractionTop
insertPatterns	Agda.TypeChecking.Rules.Def
insertTele	Agda.Compiler.Epic.Forcing
insertWith
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)	Agda.Utils.Trie
insertWithKeyM	Agda.Utils.Map
insideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
InsideOperandCtx	Agda.Syntax.Fixity
insidePi	Agda.TypeChecking.InstanceArguments
Instance
1 (Data Constructor)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Auto.Syntax
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
InstanceTable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
instanceTransformBiMT'	Agda.Utils.Geniplate
instanceUniverseBiT'	Agda.Utils.Geniplate
Instantiable	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Instantiate	Agda.TypeChecking.Reduce
instantiate	Agda.TypeChecking.Reduce
instantiate'	Agda.TypeChecking.Reduce
Instantiated	Agda.Interaction.BasicOps
instantiateDef	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
instantiateDefinitionType	Agda.TypeChecking.Rules.Decl
InstantiateFull	Agda.TypeChecking.Reduce
instantiateFull	Agda.TypeChecking.Reduce
instantiateFull'	Agda.TypeChecking.Reduce
instantiateTel	Agda.TypeChecking.Rules.LHS.Instantiate
instantiateTelescope	Agda.TypeChecking.Telescope
inState	Agda.Syntax.Parser.LexActions
InstV	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Interactive	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interAssocWith	Agda.Termination.SparseMatrix
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
interleaveRanges	Agda.Syntax.Position
InternalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
Intro	Agda.Interaction.InteractionTop
intro1	Agda.TypeChecking.Telescope
intros	Agda.Compiler.MAlonzo.Compiler
introTactic	Agda.Interaction.BasicOps
intSemiring	Agda.Termination.Semiring
intView	Agda.Syntax.Treeless
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
InvalidTerminationCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InvalidTypeSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Invariant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Inverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
ipcClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ipcClauseNo	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IPClause
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ipClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ipcQName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ipMeta	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IPNoClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iPragmaOptions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ipRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Irr	Agda.Compiler.Epic.Interface
Irrel	Agda.TypeChecking.MetaVars.Occurs
Irrelevant	Agda.Syntax.Common
IrrelevantDatatype	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Irrelevantly
1 (Data Constructor)	Agda.TypeChecking.Free.Old
2 (Data Constructor)	Agda.TypeChecking.Free
irrelevantOrUnused	Agda.Syntax.Common
irrelevantVars
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
irrToNonStrict	Agda.Syntax.Common
IsAbstract	Agda.Syntax.Common
isAbsurdBody	Agda.Syntax.Internal
isAbsurdLambdaName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
isApplyElim	Agda.Syntax.Internal
isBelow	Agda.Utils.Warshall
isBinderUsed
1 (Function)	Agda.TypeChecking.Free.Old
2 (Function)	Agda.TypeChecking.Free
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
isCode	Agda.Syntax.Parser.Literate
isCoind	Agda.Compiler.JS.Syntax
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
iScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isCovered	Agda.TypeChecking.Coverage
IsData	Agda.TypeChecking.Datatypes
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
isDefaultImportDir	Agda.Syntax.Common
IsDigit	Agda.Utils.Char
IsDominated	Agda.Utils.Favorites
IsEmpty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Termination.SparseMatrix
isEmptyFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmptyObject	Agda.Compiler.JS.Compiler
IsEmptyType	Agda.Interaction.BasicOps
isEmptyType	Agda.TypeChecking.Empty
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
isFullyInstantiatedMeta	Agda.TypeChecking.Reduce
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isGlobal	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
isImported	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isInductiveRecord	Agda.TypeChecking.Records
IsInfix	Agda.Syntax.Common
isInfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInftyNode	Agda.TypeChecking.SizedTypes.WarshallSolver
isInjective	Agda.Compiler.Epic.Injection
isInjectiveHere	Agda.Compiler.Epic.Injection
isInlineFun	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isInModule	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
isInsideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
IsInstance	Agda.Syntax.Common
IsInstantiatedMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInstantiatedMeta
1 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
2 (Function)	Agda.TypeChecking.Reduce.Monad
isInstantiatedMeta'	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInt	Agda.Compiler.UHC.FromAgda
isInteractionMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isIrr	Agda.Compiler.Epic.Erasure
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
isLiterate	Agda.Interaction.Options
isLocal	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IsLower	Agda.Utils.Char
IsMacro	Agda.Syntax.Common
isMacro	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IsMain
1 (Type/Class)	Agda.Compiler.Common
2 (Data Constructor)	Agda.Compiler.Common
IsMark	Agda.Utils.Char
isModChar	Agda.Compiler.MAlonzo.Misc
isModuleFreeVar	Agda.TypeChecking.Rules.Term
isNameInScope	Agda.Syntax.Scope.Base
isNat	Agda.Compiler.UHC.FromAgda
isNatish	Agda.Compiler.Epic.NatDetection
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
isNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract
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
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
3 (Function)	Agda.Compiler.MAlonzo.Pretty
isOrder	Agda.Termination.Order
iSourceHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IsPatSyn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
IsPrint	Agda.Utils.Char
isProblemSolved	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
isProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isProjectionButNotCoinductive	Agda.Termination.Monad
isProjection_	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IsProjElim	Agda.Syntax.Internal
isProjElim	Agda.Syntax.Internal
IsProjP	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
isProjP	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
isProperProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IsPunctuation	Agda.Utils.Char
isQName	Agda.Interaction.BasicOps
isRec	Agda.Compiler.Epic.NatDetection
IsRecord	Agda.TypeChecking.Datatypes
isRecord	Agda.TypeChecking.Records
isRecordConstructor	Agda.TypeChecking.Records
isRecordType	Agda.TypeChecking.Records
isRecursiveRecord	Agda.TypeChecking.Records
IsReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isRel	Agda.Compiler.Epic.Erasure
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
isSizeNameTestRaw	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeProblem	Agda.TypeChecking.SizedTypes
IsSizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeType	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeTest	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblem	Agda.TypeChecking.Rules.LHS
isSolvingConstraints	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
IsSort	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isSortMeta_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
IsSpace	Agda.Utils.Char
isStaticFun	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isSublistOf	Agda.Utils.List
isSubModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract
isSubscriptDigit	Agda.Utils.Suffix
isSubsetOf	Agda.Utils.VarSet
IsSuffix	Agda.Utils.List
IsSymbol	Agda.Utils.Char
IsTag	Agda.Compiler.Epic.Injection
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
isTypeEqualTo	Agda.TypeChecking.Rules.Term
IsType_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_	Agda.TypeChecking.Rules.Term
isUnderscore	Agda.Syntax.Common
isUnreachable	Agda.Syntax.Treeless
isUntypedBuiltin	Agda.TypeChecking.Rules.Builtin
IsUpper	Agda.Utils.Char
isVar	Agda.TypeChecking.CompiledClause.Compile
isVisited	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
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