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

IApply	Agda.Syntax.Internal
IApplyP	Agda.Syntax.Internal
iApplyVars	Agda.TypeChecking.Telescope.Path
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.Common
IdS	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
idS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
idViewAsPath	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ifDirty	Agda.Utils.Update
iFileType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifIsSort	Agda.TypeChecking.Sort
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
ifNotNull	Agda.Utils.Null
ifNotNullM	Agda.Utils.Null
ifNotPi	Agda.TypeChecking.Telescope
ifNotPiOrPathType	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
ifPath	Agda.TypeChecking.Rules.Term
ifPi	Agda.TypeChecking.Telescope
ifPiType	Agda.TypeChecking.Telescope
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.Base
IgnoreAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreAll	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreAllInterfaces	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreBlocking	Agda.Syntax.Internal
IgnoreInAnnotations	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreInterfaces	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreNot	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreSorts	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
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
iImportWarning	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iInsideScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ilam	Agda.TypeChecking.Names
iLength	Agda.Syntax.Position
IllegalLetInTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalPatternInTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedAsClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedAsClause_	Agda.Interaction.Options.Warnings
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
IMax	Agda.Syntax.Internal
imax	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
IMin	Agda.Syntax.Internal
imin	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
imoduleMap	Agda.Syntax.Scope.Monad
iModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ImpMissingDefinitions	Agda.Utils.Impossible
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
ImportedNameMap
1 (Type/Class)	Agda.Syntax.Scope.Monad
2 (Data Constructor)	Agda.Syntax.Scope.Monad
importedNameMapFromList	Agda.Syntax.Scope.Monad
ImportedNS	Agda.Syntax.Scope.Base
importModule	Agda.Utils.Haskell.Syntax
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
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
In1	Agda.Utils.Three
In2	Agda.Utils.Three
In3	Agda.Utils.Three
inAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inameMap	Agda.Syntax.Scope.Monad
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
incompleteMatchWarnings	Agda.Interaction.Options.Warnings
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
inCxt	Agda.TypeChecking.Names
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
indexWithDefault	Agda.Utils.List
Indirect	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Induction	Agda.Syntax.Common
Inductive	Agda.Syntax.Common
INeg	Agda.Syntax.Internal
Inf	Agda.Syntax.Internal
inf	Agda.TypeChecking.Positivity
InfectiveImport	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InfectiveImport_	Agda.Interaction.Options.Warnings
infectiveOptions	Agda.Interaction.Options
infer	Agda.TypeChecking.CheckInternal
inferApplication	Agda.TypeChecking.Rules.Application
InferDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
inferFunSort	Agda.TypeChecking.Sort
inferMeta	Agda.TypeChecking.Rules.Term
inferPiSort	Agda.TypeChecking.Sort
Inferred	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferSort	Agda.TypeChecking.CheckInternal
infertypevar	Agda.Auto.CaseSplit
inferUnivSort	Agda.TypeChecking.Sort
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_CompilationError	Agda.Interaction.Response
Info_CompilationOk	Agda.Interaction.Response
Info_Constraints	Agda.Interaction.Response
Info_Context	Agda.Interaction.Response
Info_Error
1 (Type/Class)	Agda.Interaction.Response
2 (Data Constructor)	Agda.Interaction.Response
Info_GenericError	Agda.Interaction.Response
Info_GoalSpecific	Agda.Interaction.Response
Info_HighlightingParseError	Agda.Interaction.Response
Info_HighlightingScopeCheckError	Agda.Interaction.Response
Info_InferredType	Agda.Interaction.Response
Info_Intro_ConstructorUnknown	Agda.Interaction.Response
Info_Intro_NotFound	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.Base
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
initialiseCommandQueue	Agda.Interaction.InteractionTop
initLast	Agda.Utils.List
initLHSState	Agda.TypeChecking.Rules.LHS.ProblemRest
initMapS	Agda.Auto.Convert
initMaybe	Agda.Utils.List
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
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
1 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Type/Class)	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.Bag
3 (Function)	Agda.Utils.SmallSet
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
insertImplicit'	Agda.TypeChecking.Implicit
insertImplicitPatSynArgs	Agda.Syntax.Abstract
insertImplicitPatterns	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitPatternsT	Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitSizeLtPatterns	Agda.TypeChecking.Rules.LHS.Implicit
insertMetaSet	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
insertMetaVar	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertMissingFields	Agda.TypeChecking.Records
insertMutualBlockInfo	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertOldInteractionScope	Agda.Interaction.InteractionTop
insertPatterns	Agda.TypeChecking.Rules.Def
insertPatternsLHSCore	Agda.TypeChecking.Rules.Def
insertTrailingArgs	Agda.TypeChecking.Coverage
insertWith
1 (Function)	Agda.Utils.Trie
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
insideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InsideOperandCtx	Agda.Syntax.Fixity
Instance	Agda.Syntax.Common
InstanceArg	Agda.Syntax.Concrete
InstanceArgV	Agda.Syntax.Concrete.Operators.Parser
InstanceArgWithExplicitArg	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceArgWithExplicitArg_	Agda.Interaction.Options.Warnings
InstanceB	Agda.Syntax.Concrete
InstanceDef	Agda.Syntax.Common
InstanceNoCandidate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoOutputTypeName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoOutputTypeName_	Agda.Interaction.Options.Warnings
InstanceP	Agda.Syntax.Concrete
InstanceSearch	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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
InstanceWithExplicitArg	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceWithExplicitArg_	Agda.Interaction.Options.Warnings
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.Base
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
instantiateTelescope	Agda.TypeChecking.Telescope
instantiateVarHeads	Agda.TypeChecking.Injectivity
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
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Syntax.Parser.LexActions
integerC	Agda.TypeChecking.Serialise.Base
integerD	Agda.TypeChecking.Serialise.Base
integerE	Agda.TypeChecking.Serialise.Base
integerSemiring	Agda.Termination.Semiring
Interaction	Agda.Interaction.Base
interaction	Agda.Interaction.CommandLine
Interaction'	Agda.Interaction.Base
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
interestingConstraint	Agda.TypeChecking.Pretty.Warning
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
InterfaceFile	Agda.Interaction.FindFile
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
intersection
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.SmallSet
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
intervalUnview	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
intervalUnview'	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntervalView	Agda.Syntax.Internal
intervalView	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
intervalView'	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntervalWithoutFile	Agda.Syntax.Position
intFilePath	Agda.Interaction.FindFile
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
IntSet	Agda.Utils.IntSet.Infinite
intView	Agda.Syntax.Treeless, Agda.Compiler.Backend
Inv	Agda.TypeChecking.Injectivity
InvalidCatchallPragma	Agda.Syntax.Concrete.Definitions
InvalidCatchallPragma_	Agda.Interaction.Options.Warnings
InvalidCoverageCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidCoverageCheckPragma_	Agda.Interaction.Options.Warnings
InvalidExtensionError	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
InvalidMeasureMutual	Agda.Syntax.Concrete.Definitions
InvalidName	Agda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragma_	Agda.Interaction.Options.Warnings
InvalidNoUniverseCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidNoUniverseCheckPragma_	Agda.Interaction.Options.Warnings
InvalidPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTerminationCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidTerminationCheckPragma_	Agda.Interaction.Options.Warnings
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
invariant
1 (Function)	Agda.Utils.IntSet.Infinite
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
Inverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inverseApplyCohesion	Agda.Syntax.Common
inverseApplyModality	Agda.Syntax.Common
inverseApplyQuantity	Agda.Syntax.Common
inverseApplyRelevance	Agda.Syntax.Common
inverseCompose	Agda.Utils.POMonoid
inverseComposeCohesion	Agda.Syntax.Common
inverseComposeModality	Agda.Syntax.Common
inverseComposeQuantity	Agda.Syntax.Common
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
InversionDepthReached	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InversionDepthReached_	Agda.Interaction.Options.Warnings
InversionMap	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Invert	Agda.Syntax.Common
InvertExcept	Agda.TypeChecking.MetaVars
invertFunction	Agda.TypeChecking.Injectivity
invertP	Agda.Utils.Permutation
invLookup	Agda.Utils.BiMap
InvView	Agda.TypeChecking.Injectivity
io	Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
IOException	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IOne	Agda.Syntax.Internal
iOptionsUsed	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.Base
2 (Type/Class)	Agda.Interaction.Base
IOTCM'	Agda.Interaction.Base
iPartialDefs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iPatternSyns	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbEquations	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbMetaApp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPBoundary
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
IPBoundary'	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbOverapplied	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbValue	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcBoundary	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
ipcClosure	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
ipcType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcWithSub	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
Irrelevant	Agda.Syntax.Common
IrrelevantDatatype	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
irrToNonStrict	Agda.Syntax.Common
IsAbstract	Agda.Syntax.Common
isAbsurdBody	Agda.Syntax.Internal
isAbsurdLambdaName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isAbsurdP	Agda.Syntax.Concrete
isAbsurdPatternName	Agda.Syntax.Internal
isAHole	Agda.Syntax.Notation
isAlias	Agda.TypeChecking.Rules.Def
isAmbiguous	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isAnonymousModuleName	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
IsApply	Agda.TypeChecking.Coverage.Match
isApplyElim	Agda.Syntax.Internal
isApplyElim'	Agda.Syntax.Internal
IsBase	Agda.Utils.TypeLevel
isBelow	Agda.Utils.Warshall
isBenchmarkOn	Agda.Utils.Benchmark
isBinderP	Agda.Syntax.Concrete
isBinderUsed	Agda.TypeChecking.Free
isBindingHole	Agda.Syntax.Notation
isBlocked	Agda.TypeChecking.Reduce
isBlockedTerm	Agda.TypeChecking.MetaVars
isBounded	Agda.TypeChecking.SizedTypes
isBuiltin	Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
isBuiltinModule	Agda.Interaction.Options.Lenses
isBuiltinModuleWithSafePostulates	Agda.Interaction.Options.Lenses
isCached	Agda.Interaction.Imports
isCanonical	Agda.TypeChecking.Conversion
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
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
isDebugPrinting	Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isDecr	Agda.Termination.Order
isDef	Agda.TypeChecking.Unquote
isDefAccount	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isDefaultImportDir	Agda.Syntax.Common
isDefName	Agda.Syntax.Scope.Base
IsDominated	Agda.Utils.Favorites
isDontExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsEllipsis	Agda.Syntax.Concrete.Pattern
isEllipsis	Agda.Syntax.Concrete.Pattern
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
isEmptyTel	Agda.TypeChecking.Empty
IsEmptyType	Agda.Interaction.Base
isEmptyType	Agda.TypeChecking.Empty
isEnabled	Agda.Compiler.Backend
isEqualityType	Agda.Syntax.Internal
isErasable	Agda.Compiler.Treeless.Erase
isEtaCon	Agda.TypeChecking.Records
isEtaExpandable	Agda.TypeChecking.MetaVars
isEtaOrCoinductiveRecordConstructor	Agda.TypeChecking.Records
isEtaRecord	Agda.TypeChecking.Records
isEtaRecordType	Agda.TypeChecking.Records
isEtaVar	Agda.TypeChecking.Records
IsExpr	Agda.Syntax.Concrete.Operators.Parser
isExtendedLambdaName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsFam	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
isFlexible	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
IsFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexNode	Agda.TypeChecking.SizedTypes.WarshallSolver
IsForced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isForced	Agda.TypeChecking.Forcing
IsFree	Agda.TypeChecking.Free.Reduce
isFrozen	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isFullyInstantiatedMeta	Agda.TypeChecking.Reduce
isGeneralizableMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isHole	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsIApply	Agda.TypeChecking.Coverage.Match
iSignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isImported	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsIndex	Agda.TypeChecking.Positivity.Occurrence
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
isInScope	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInsertedHidden	Agda.Syntax.Common
isInsideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsInstance	Agda.Syntax.Common
isInstance	Agda.Syntax.Common
isInstanceConstraint	Agda.TypeChecking.InstanceArguments
IsInstantiatedMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInstantiatedMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isIOne	Agda.Syntax.Internal
isIrrelevant	Agda.Syntax.Common
isIrrelevantOrPropM	Agda.TypeChecking.Irrelevance
isJust
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
isLabeled	Agda.Syntax.Concrete.Pretty
isLambdaHole	Agda.Syntax.Notation
isLeChildModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLeft	Agda.Utils.Either
isLeParentModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLevelType	Agda.TypeChecking.Level
IsLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isLocal	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isLtChildModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLtParentModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
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
IsMeta	Agda.TypeChecking.Reduce
isMeta	Agda.TypeChecking.Reduce
isMetaTCWarning	Agda.TypeChecking.Warnings
isMetaWarning	Agda.TypeChecking.Warnings
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
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
isNonStrict	Agda.Syntax.Common
isNormalHole	Agda.Syntax.Notation
IsNot	Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
isNothing
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
isolatedNodes	Agda.Utils.Graph.AdjacencyMap.Unidirectional
isOpenMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isOpenMixfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
iSource	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iSourceHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isOverlappable	Agda.Syntax.Common
isPath	Agda.TypeChecking.Telescope
IsPathCons	Agda.TypeChecking.Rules.Data
isPathType	Agda.Syntax.Internal
IsPatSyn	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPattern	Agda.Syntax.Concrete
isPostfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsPrefixOf	Agda.TypeChecking.Abstract
isPrefixOf	Agda.TypeChecking.Abstract
isPrimEq	Agda.Syntax.Treeless, Agda.Compiler.Backend
isPrimitive	Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isPropEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProperProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPropM	Agda.TypeChecking.Irrelevance
isQName	Agda.Interaction.BasicOps
isQualified	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isQuantityAttribute	Agda.Syntax.Concrete.Attribute
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
isRelevanceAttribute	Agda.Syntax.Concrete.Attribute
isRelevant	Agda.Syntax.Common
isRight	Agda.Utils.Either
isSet	Agda.Syntax.Abstract.Views
isSingleIdentifierP	Agda.Syntax.Concrete
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
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
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
isStaticFun	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isStronglyRigid	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isSublistOf	Agda.Utils.List
isSubscriptDigit	Agda.Utils.Suffix
isSubsetOf
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.SmallSet
isTacticAttribute	Agda.Syntax.Concrete.Attribute
iStart	Agda.Syntax.Position
isTop	Agda.TypeChecking.SizedTypes.Utils
isTopLevelValue	Agda.Compiler.JS.Compiler
isTrivialPattern	Agda.TypeChecking.Coverage.Match
isType	Agda.TypeChecking.Rules.Term
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
isUnguarded	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isUnqualified	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isUnreachable	Agda.Syntax.Treeless, Agda.Compiler.Backend
isUnsolvedWarning	Agda.TypeChecking.Warnings
isUntypedBuiltin	Agda.TypeChecking.Rules.Builtin
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
isWeaklyRigid	Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
IsWithP	Agda.Syntax.Concrete.Pattern
isWithP	Agda.Syntax.Concrete.Pattern
isWithPattern	Agda.Syntax.Concrete.Pattern
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
iUserWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IVar	Agda.Utils.Haskell.Syntax
iWarnings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Ix	Agda.Utils.SmallSet
IZero	Agda.Syntax.Internal