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
Id
1 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Auto.Syntax
idempotent
1 (Function)	Agda.Utils.TestHelpers
2 (Function)	Agda.Termination.Termination
Ident	Agda.Syntax.Concrete
identifier
1 (Function)	Agda.Compiler.JS.Parser
2 (Function)	Agda.Syntax.Parser.LexActions
identity	Agda.Utils.TestHelpers
IdentP	Agda.Syntax.Concrete
idP	Agda.Utils.Permutation
IdPart	Agda.Syntax.Notation
IdS	Agda.TypeChecking.Substitute
idS	Agda.TypeChecking.Substitute
iEnd	Agda.Syntax.Position
If
1 (Data Constructor)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.Epic.AuxAST
ifBlock	Agda.Compiler.JS.Parser
ifBlocked	Agda.TypeChecking.Reduce
ifBlockedType	Agda.TypeChecking.Reduce
ifClean	Agda.TypeChecking.Rules.LHS.Unify
ifDirty	Agda.Utils.Update
ifJustM
1 (Function)	Agda.Utils.Maybe.Strict
2 (Function)	Agda.Utils.Maybe
ifLe	Agda.TypeChecking.SizedTypes.Syntax
ifM	Agda.Utils.Monad
ifNoConstraints	Agda.TypeChecking.Constraints
ifNoConstraints_	Agda.TypeChecking.Constraints
ifNotM	Agda.Utils.Monad
IFSNoCandidateInScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIs	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iFullHash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IgnoreAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IgnoreAll	Agda.TypeChecking.Free
ignoreBlocking	Agda.Syntax.Internal
ignoreForced
1 (Function)	Agda.TypeChecking.Irrelevance
2 (Function)	Agda.Compiler.Epic.Erasure
IgnoreInAnnotations	Agda.TypeChecking.Free
ignoreInterfaces	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
IgnoreNot	Agda.TypeChecking.Free
ignoreReduced	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreSharing	Agda.Syntax.Internal
ignoreSharingType	Agda.Syntax.Internal
IgnoreSorts	Agda.TypeChecking.Free
iHaskellImports	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlighting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihname	Agda.Compiler.MAlonzo.Misc
iImportedModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IllegalLetInTelescope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IllformedProjectionPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IM	Agda.Interaction.Monad
iModuleName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsert	Agda.TypeChecking.Implicit
impInsert	Agda.TypeChecking.Implicit
implicitArgs	Agda.TypeChecking.Implicit
ImplicitFlex	Agda.TypeChecking.Rules.LHS.Problem
ImplicitInsertion	Agda.TypeChecking.Implicit
implicitNamedArgs	Agda.TypeChecking.Implicit
ImplicitP	Agda.Syntax.Abstract
implicitP	Agda.TypeChecking.Rules.LHS.Implicit
implies	Agda.TypeChecking.SizedTypes.WarshallSolver
Import
1 (Data Constructor)	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Abstract
ImportDirective
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
importDirRange	Agda.Syntax.Concrete
ImportedModule	Agda.Syntax.Concrete
importedModules	Agda.Compiler.Epic.CompileState
ImportedName
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
importedName	Agda.Syntax.Concrete
ImportedNS	Agda.Syntax.Scope.Base
ImportPragma	Agda.Syntax.Concrete
imports	Agda.Compiler.MAlonzo.Compiler
importsForPrim	Agda.Compiler.MAlonzo.Primitives
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
imp_dir	Agda.Syntax.Parser.Lexer
inAbstractMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inc	Agda.Utils.Warshall
InClause	Agda.TypeChecking.Positivity
IncludeDirs	Agda.Interaction.Options
Inclusion
1 (Type/Class)	Agda.Utils.PartialOrd
2 (Data Constructor)	Agda.Utils.PartialOrd
inclusion	Agda.Utils.PartialOrd
incoming	Agda.TypeChecking.SizedTypes.WarshallSolver
IncompletePattern	Agda.Interaction.Highlighting.Precise
IncompletePatternMatching	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteMode	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
increase	Agda.Termination.Order
IndArgType	Agda.TypeChecking.Positivity
InDefOf	Agda.TypeChecking.Positivity
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
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
inferExprForWith	Agda.TypeChecking.Rules.Term
inferHead	Agda.TypeChecking.Rules.Term
inferMeta	Agda.TypeChecking.Rules.Term
infertypevar	Agda.Auto.CaseSplit
InferVar	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
infimum	Agda.Termination.Order
Infinite	Agda.Utils.Warshall
infinite	Agda.Utils.Warshall
infiniteList	Agda.Utils.QuickCheck
infiniteListOf	Agda.Utils.QuickCheck
Infinity	Agda.TypeChecking.SizedTypes.WarshallSolver
infinityFlexs	Agda.TypeChecking.SizedTypes.WarshallSolver
Infix	Agda.Syntax.Concrete
InfixDef	Agda.Syntax.Common
infixlP	Agda.Syntax.Concrete.Operators.Parser
infixP	Agda.Syntax.Concrete.Operators.Parser
infixrP	Agda.Syntax.Concrete.Operators.Parser
infodecl	Agda.Compiler.MAlonzo.Compiler
Info_AllGoals	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_WhyInScope	Agda.Interaction.Response
Infty	Agda.TypeChecking.SizedTypes.Syntax
initCommandState	Agda.Interaction.InteractionTop
initCompileState	Agda.Compiler.Epic.CompileState
initEnv	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraph	Agda.Utils.Warshall
initialDotState	Agda.Interaction.Highlighting.Dot
initialIFSCandidates	Agda.TypeChecking.InstanceArguments
initializeIFSMeta	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
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.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
Inline	Agda.Compiler.Epic.AuxAST
inlineWithClauses	Agda.Termination.Inlining
inMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpace	Agda.Syntax.Scope.Base
InScope	Agda.Syntax.Scope.Base
inScopeBecause	Agda.Syntax.Scope.Base
InScopeTag	Agda.Syntax.Scope.Base
inScopeTag	Agda.Syntax.Scope.Base
insert
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.Graph.AdjacencyMap
4 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
5 (Function)	Agda.Utils.Favorites
6 (Function)	Agda.Utils.Trie
7 (Function)	Agda.Termination.CallMatrix
8 (Function)	Agda.Termination.CallGraph
insertAfter	Agda.Compiler.JS.Compiler
insertAt	Agda.Compiler.Epic.Injection
insertCompared	Agda.Utils.Favorites
insertEdge
1 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)	Agda.TypeChecking.SizedTypes.WarshallSolver
insertEdgeWith	Agda.Utils.Graph.AdjacencyMap.Unidirectional
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
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
insideScope	Agda.Syntax.Translation.ConcreteToAbstract
Instance
1 (Data Constructor)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Auto.Syntax
InstanceArg	Agda.Syntax.Concrete
InstanceArgV	Agda.Syntax.Concrete.Operators.Parser
InstanceP	Agda.Syntax.Concrete
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
instantiatePattern	Agda.TypeChecking.Rules.LHS
instantiateTel	Agda.TypeChecking.Rules.LHS.Instantiate
inState	Agda.Syntax.Parser.LexActions
InstS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstV	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
int	Agda.Utils.Pretty
Integer	Agda.Compiler.JS.Syntax
integer	Agda.Utils.Pretty
integerSemiring	Agda.Termination.Semiring
Interaction	Agda.Interaction.InteractionTop
interaction	Agda.Interaction.CommandLine.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.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
interestingCall	Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
Interface
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InternalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalError	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interpret	Agda.Interaction.InteractionTop
intersection	Agda.Utils.HashMap
intersectionWith	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.Position
intervalInvariant	Agda.Syntax.Position
intLit	Agda.Compiler.JS.Parser
intMap	Agda.Utils.Warshall
inTopContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
introTactic	Agda.Interaction.BasicOps
intSemiring	Agda.Termination.Semiring
Inv	Agda.TypeChecking.Injectivity
InvalidNoTerminationCheckPragma	Agda.Syntax.Concrete.Definitions
InvalidPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InvalidType	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Invariant	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
invariant	Agda.Utils.Graph.AdjacencyMap
Inverse	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseApplyRelevance	Agda.TypeChecking.Irrelevance
inverseComposeRelevance	Agda.TypeChecking.Irrelevance
inverseScopeLookup	Agda.Syntax.Scope.Base
inverseScopeLookupModule	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
ioProperty	Agda.Utils.QuickCheck
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
ipMeta	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	Agda.TypeChecking.Free
irrelevantOrUnused	Agda.TypeChecking.Irrelevance
irrelevantVars	Agda.TypeChecking.Free
irrToNonStrict	Agda.TypeChecking.Irrelevance
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
isAnonymousModuleName	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
isApplyElim	Agda.Syntax.Internal
isBelow	Agda.Utils.Warshall
isBinderUsed	Agda.TypeChecking.Free
isBindingHole	Agda.Syntax.Notation
isBlockedTerm	Agda.TypeChecking.MetaVars
IsBothfix	Agda.Utils.List
isBounded	Agda.TypeChecking.SizedTypes
isCoinductive	Agda.TypeChecking.Rules.Data
isCoinductiveProjection	Agda.Termination.Monad
isCon	Agda.TypeChecking.Quote
iScope	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IsData	Agda.TypeChecking.Datatypes
isDataOrRecord	Agda.TypeChecking.Datatypes
isDataOrRecordType	Agda.TypeChecking.Datatypes
isDatatype
1 (Function)	Agda.TypeChecking.Datatypes
2 (Function)	Agda.TypeChecking.Coverage
isDatatypeModule	Agda.Syntax.Scope.Monad
isDecr	Agda.Termination.Order
IsDominated	Agda.Utils.Favorites
IsEmpty	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.Termination.SparseMatrix
isEmptyObject	Agda.Compiler.JS.Compiler
IsEmptyType	Agda.Interaction.BasicOps
isEmptyType	Agda.TypeChecking.Empty
ISet
1 (Type/Class)	Agda.Utils.PartialOrd
2 (Data Constructor)	Agda.Utils.PartialOrd
iset	Agda.Utils.PartialOrd
isEtaCon	Agda.TypeChecking.Records
isEtaExpandable	Agda.TypeChecking.MetaVars
isEtaRecord	Agda.TypeChecking.Records
isEtaRecordType	Agda.TypeChecking.Records
isEtaRecordTypeHH	Agda.TypeChecking.Rules.LHS.Unify
IsExpr	Agda.Syntax.Concrete.Operators.Parser
isFlexNode	Agda.TypeChecking.SizedTypes.WarshallSolver
isFrozen	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isHaskellKind	Agda.Compiler.HaskellTypes
isHidden	Agda.Syntax.Common
isHole	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isHom	Agda.TypeChecking.Rules.LHS.Unify
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
isInModule	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
isInsideDotPattern	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
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
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
IsLHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isLiterate	Agda.Interaction.Options
isNatish	Agda.Compiler.Epic.NatDetection
isNeutral	Agda.TypeChecking.MetaVars.Occurs
isNewerThan	Agda.Interaction.Imports
IsNofix	Agda.Utils.List
IsNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Syntax.Internal
isNoName	Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Syntax.Internal
isNonfix	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothing
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
isntTypeConf	Agda.TypeChecking.Test.Generators
isOperator
1 (Function)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
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
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
isProjP	Agda.Syntax.Abstract
isProperProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
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
isSet	Agda.Syntax.Abstract.Views
isSingleton
1 (Function)	Agda.Termination.SparseMatrix
2 (Function)	Agda.Compiler.JS.Compiler
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
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
isSublistOf	Agda.Utils.List
isSubModuleOf	Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal
isSubscriptDigit	Agda.Utils.Suffix
isSubsetOf	Agda.Utils.VarSet
isSuccess	Agda.Utils.QuickCheck
IsSuffix	Agda.Utils.List
IsTag	Agda.Compiler.Epic.Injection
iStart	Agda.Syntax.Position
isTop	Agda.TypeChecking.SizedTypes.Utils
isTopLevelValue	Agda.Compiler.JS.Compiler
isType	Agda.TypeChecking.Rules.Term
IsTypeCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConf	Agda.TypeChecking.Test.Generators
isTypeEqualTo	Agda.TypeChecking.Rules.Term
IsType_	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_	Agda.TypeChecking.Rules.Term
isUnderscore	Agda.Syntax.Common
isUnicodeId	Agda.Utils.Unicode
isVisited	Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScoped	Agda.TypeChecking.Test.Generators
isWithFunction	Agda.Termination.Inlining
isZero	Agda.Utils.TestHelpers
isZeroNode	Agda.TypeChecking.SizedTypes.WarshallSolver
Item	Agda.TypeChecking.Positivity
iterate'	Agda.Utils.Function
iterateUntil	Agda.Utils.Function
iterateUntilM	Agda.Utils.Function