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.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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.Syntax.Internal, 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
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
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
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
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad
imapClauseBody	Agda.Syntax.Internal
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.Benchmarking, 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
inConcreteOrAbstractMode	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
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
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
InfixNotation	Agda.Syntax.Notation
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_Version	Agda.Interaction.Response
Info_WhyInScope	Agda.Interaction.Response
Infty	Agda.TypeChecking.SizedTypes.Syntax
initCCEnv	Agda.Compiler.MAlonzo.Compiler
initCommandState	Agda.Interaction.InteractionTop
initCompileState	Agda.Compiler.Epic.CompileState
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
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
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
inlineWithClauses	Agda.Termination.Inlining
inMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpace	Agda.Syntax.Scope.Base
inputFlag	Agda.Interaction.Options
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.BiMap
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.AssocList
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Favorites
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)	Agda.Utils.Trie
8 (Function)	Agda.Termination.CallMatrix
9 (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
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
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.Auto.Syntax
2 (Data Constructor)	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
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
instantiatePattern	Agda.TypeChecking.Rules.LHS
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
InsufficientCoverage	Agda.Utils.QuickCheck
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
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
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
1 (Function)	Agda.Utils.VarSet
2 (Function)	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
intro1	Agda.TypeChecking.Telescope
intros	Agda.Compiler.MAlonzo.Compiler
introTactic	Agda.Interaction.BasicOps
intSemiring	Agda.Termination.Semiring
Inv	Agda.TypeChecking.Injectivity
InvalidMeasureMutual	Agda.Syntax.Concrete.Definitions
InvalidName	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
ioProperty	Agda.Utils.QuickCheck
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
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
1 (Data Constructor)	Agda.TypeChecking.Free
2 (Data Constructor)	Agda.TypeChecking.Free.Old
irrelevantOrUnused	Agda.Syntax.Common
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
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.Abstract, Agda.Syntax.Internal
isApplyElim	Agda.Syntax.Internal
isBelow	Agda.Utils.Warshall
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
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
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
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
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
IsFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexiblePattern	Agda.TypeChecking.Rules.LHS
isFlexNode	Agda.TypeChecking.SizedTypes.WarshallSolver
isFrozen	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isGeneratedRecordConstructor	Agda.TypeChecking.Records
isHackReifyToMeta	Agda.Syntax.Internal
isHaskellKind	Agda.Compiler.HaskellTypes
IsHexDigit	Agda.Utils.Char
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
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
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
IsLower	Agda.Utils.Char
IsMark	Agda.Utils.Char
isModuleFreeVar	Agda.TypeChecking.Rules.Term
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
IsNumber	Agda.Utils.Char
IsOctDigit	Agda.Utils.Char
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
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
isProjP	Agda.Syntax.Abstract
isProperProjection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
IsPunctuation	Agda.Utils.Char
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
isReifyingUnquoted	Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
isRel	Agda.Compiler.Epic.Erasure
isRelevant	Agda.Syntax.Common
isRight	Agda.Utils.Either
IsSeparator	Agda.Utils.Char
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
IsSpace	Agda.Utils.Char
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
IsSymbol	Agda.Utils.Char
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
IsUpper	Agda.Utils.Char
isVar	Agda.TypeChecking.CompiledClause.Compile
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
iterWhile	Agda.Utils.Function