Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant

Index - I

IApplyAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
IApplyPAgda.Syntax.Internal
iApplyVarsAgda.TypeChecking.Telescope.Path
iBuiltinAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ICArgListAgda.Auto.Syntax
ICExpAgda.Auto.Syntax
icnvhAgda.Auto.Convert
ICODEAgda.TypeChecking.Serialise.Base
icodeAgda.TypeChecking.Serialise.Base
icodeArgsAgda.TypeChecking.Serialise.Base
icodeDoubleAgda.TypeChecking.Serialise.Base
icodeIntegerAgda.TypeChecking.Serialise.Base
icodeMemoAgda.TypeChecking.Serialise.Base
icodeNAgda.TypeChecking.Serialise.Base
icodeN'Agda.TypeChecking.Serialise.Base
icodeNodeAgda.TypeChecking.Serialise.Base
icodeStringAgda.TypeChecking.Serialise.Base
icodeXAgda.TypeChecking.Serialise.Base
icod_Agda.TypeChecking.Serialise.Base
Id 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
iDefaultPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
idempotentAgda.Termination.Termination
Ident 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
identifierAgda.Syntax.Parser.LexActions
IdentPAgda.Syntax.Concrete
IdiomBracketsAgda.Syntax.Concrete
IdiomTypeAgda.Syntax.Internal
iDisplayFormsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
idPAgda.Utils.Permutation
IdPartAgda.Syntax.Common
IdSAgda.Syntax.Internal, Agda.TypeChecking.Substitute
idSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
idViewAsPathAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
iEndAgda.Syntax.Position
If 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Type/Class)Agda.Utils.TypeLevel
ifBlockedAgda.TypeChecking.Reduce
ifDirtyAgda.Utils.Update
iFilePragmaOptionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iFileTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ifIsSortAgda.TypeChecking.Sort
ifJustAgda.Utils.Maybe
ifJustM 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
ifLeAgda.TypeChecking.SizedTypes.Syntax
ifMAgda.Utils.Monad
ifNoConstraintsAgda.TypeChecking.Constraints
ifNoConstraints_Agda.TypeChecking.Constraints
ifNotMAgda.Utils.Monad
ifNotNull 
1 (Function)Agda.Utils.Null
2 (Function)Agda.Utils.List1
ifNotNullMAgda.Utils.Null
ifNotPiAgda.TypeChecking.Telescope
ifNotPiOrPathTypeAgda.TypeChecking.Telescope
ifNotPiTypeAgda.TypeChecking.Telescope
ifNotSortAgda.TypeChecking.Sort
ifNull 
1 (Function)Agda.Utils.Null
2 (Function)Agda.Utils.List1
ifNullMAgda.Utils.Null
iForeignCodeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ifPathAgda.TypeChecking.Rules.Term
ifPiAgda.TypeChecking.Telescope
ifPiTypeAgda.TypeChecking.Telescope
ifTopLevelAndHighlightingLevelIsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIsOrAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iFullHashAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IgnoreAbstractAgda.Interaction.Base
IgnoreAbstractModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ignoreAbstractModeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
IgnoreAllAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreBlockingAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
IgnoreInAnnotationsAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
IgnoreNotAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IgnoreSortsAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
iHighlightingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ihnameAgda.Compiler.MAlonzo.Misc
iImportedModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iImportWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iInsideScopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ilamAgda.TypeChecking.Names
iLengthAgda.Syntax.Position
IllegalLetInTelescopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllegalPatternInTelescopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllformedAsClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllformedAsClause_Agda.Interaction.Options.Warnings
IllformedProjectionPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
illiterateAgda.Syntax.Parser.Literate
IMAgda.Interaction.Monad
IMaxAgda.Syntax.Internal
imaxAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
IMinAgda.Syntax.Internal
iminAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
imoduleMapAgda.Syntax.Scope.Monad
iModuleNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ImpInsertAgda.TypeChecking.Implicit
implicitArgsAgda.TypeChecking.Implicit
ImplicitFlexAgda.TypeChecking.Rules.LHS.Problem
ImplicitInsertionAgda.TypeChecking.Implicit
implicitNamedArgsAgda.TypeChecking.Implicit
implicitPAgda.TypeChecking.Rules.LHS.Implicit
impliesAgda.TypeChecking.SizedTypes.WarshallSolver
ImpMissingDefinitionsAgda.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
importDirRangeAgda.Syntax.Common
ImportedModuleAgda.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
importedNameMapFromListAgda.Syntax.Scope.Monad
ImportedNSAgda.Syntax.Scope.Base
importModuleAgda.Utils.Haskell.Syntax
importPrimitivesAgda.Syntax.Translation.ConcreteToAbstract
importQualifiedAgda.Utils.Haskell.Syntax
imports 
1 (Function)Agda.Compiler.JS.Syntax
2 (Function)Agda.Compiler.MAlonzo.Compiler
importsForPrimAgda.Compiler.MAlonzo.Primitives
ImportSpecAgda.Utils.Haskell.Syntax
importSpecsAgda.Utils.Haskell.Syntax
Impossible 
1 (Type/Class)Agda.Utils.Impossible
2 (Data Constructor)Agda.Utils.Impossible
impossibleAgda.Utils.Impossible
ImpossibleConstructorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ImpossibleErrorAgda.Interaction.ExitCode
ImpossiblePragmaAgda.Syntax.Concrete
impossibleTermAgda.Syntax.Internal
impossibleTestAgda.ImpossibleTest
impossibleTestReduceMAgda.ImpossibleTest
impRenamingAgda.Syntax.Common
imp_dirAgda.Syntax.Parser.Lexer
InAgda.Syntax.Concrete.Operators.Parser
In1Agda.Utils.Three
In2Agda.Utils.Three
In3Agda.Utils.Three
inAbstractModeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
inameMapAgda.Syntax.Scope.Monad
incAgda.Utils.Warshall
InClauseAgda.TypeChecking.Positivity.Occurrence
includesAgda.TypeChecking.Serialise.Base
Inclusion 
1 (Type/Class)Agda.Utils.PartialOrd
2 (Data Constructor)Agda.Utils.PartialOrd
inclusionAgda.Utils.PartialOrd
incomingAgda.TypeChecking.SizedTypes.WarshallSolver
inCompilerEnvAgda.Compiler.Common
incompleteMatchWarningsAgda.Interaction.Options.Warnings
IncompletePatternAgda.Interaction.Highlighting.Precise
inConcreteModeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
inConcreteOrAbstractModeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
increaseAgda.Termination.Order
inCxtAgda.TypeChecking.Names
IndArgTypeAgda.TypeChecking.Positivity.Occurrence
InDefOfAgda.TypeChecking.Positivity.Occurrence
IndentAgda.Compiler.JS.Pretty
indent 
1 (Function)Agda.Utils.String
2 (Function)Agda.Compiler.JS.Pretty
indentByAgda.Compiler.JS.Pretty
independentAgda.Interaction.InteractionTop
Index 
1 (Type/Class)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Utils.Suffix
indexWithDefaultAgda.Utils.List
IndirectAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Induction 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
InductiveAgda.Syntax.Common
INegAgda.Syntax.Internal
InfAgda.Syntax.Internal
infAgda.TypeChecking.Positivity
InfectiveImportAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InfectiveImport_Agda.Interaction.Options.Warnings
infectiveOptionsAgda.Interaction.Options
inferAgda.TypeChecking.CheckInternal
inferApplicationAgda.TypeChecking.Rules.Application
InferDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InferExprAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
inferExprAgda.TypeChecking.Rules.Term, Agda.TheTypeChecker
inferExpr'Agda.TypeChecking.Rules.Term
inferExprForWithAgda.TypeChecking.Rules.Term
inferFunSortAgda.TypeChecking.Sort
inferMetaAgda.TypeChecking.Rules.Term
inferPiSortAgda.TypeChecking.Sort
InferredAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
inferredBlockAgda.Syntax.Concrete.Definitions.Types
inferredChecksAgda.Syntax.Concrete.Definitions.Types
inferredLeftoversAgda.Syntax.Concrete.Definitions.Types
InferredMutual 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
inferSpine'Agda.TypeChecking.CheckInternal
infertypevarAgda.Auto.CaseSplit
inferUnivSortAgda.TypeChecking.Sort
InferVarAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
infimumAgda.Termination.Order
InfiniteAgda.Utils.Warshall
infiniteAgda.Utils.Warshall
InfinityAgda.TypeChecking.SizedTypes.WarshallSolver
infinityFlexsAgda.TypeChecking.SizedTypes.WarshallSolver
InfixAgda.Syntax.Concrete
InfixAppAgda.Utils.Haskell.Syntax
InfixDefAgda.Syntax.Common
InfixNotationAgda.Syntax.Notation
infodeclAgda.Compiler.MAlonzo.Compiler
Info_AllGoalsWarningsAgda.Interaction.Response
Info_AutoAgda.Interaction.Response
Info_CompilationErrorAgda.Interaction.Response
Info_CompilationOkAgda.Interaction.Response
Info_ConstraintsAgda.Interaction.Response
Info_ContextAgda.Interaction.Response
Info_Error 
1 (Type/Class)Agda.Interaction.Response
2 (Data Constructor)Agda.Interaction.Response
Info_GenericErrorAgda.Interaction.Response
Info_GoalSpecificAgda.Interaction.Response
Info_HighlightingParseErrorAgda.Interaction.Response
Info_HighlightingScopeCheckErrorAgda.Interaction.Response
Info_InferredTypeAgda.Interaction.Response
Info_Intro_ConstructorUnknownAgda.Interaction.Response
Info_Intro_NotFoundAgda.Interaction.Response
Info_ModuleContentsAgda.Interaction.Response
Info_NormalFormAgda.Interaction.Response
Info_SearchAboutAgda.Interaction.Response
Info_TimeAgda.Interaction.Response
Info_VersionAgda.Interaction.Response
Info_WhyInScopeAgda.Interaction.Response
inFreshModuleIfFreeParamsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
InfSAgda.Syntax.Reflected
InftyAgda.TypeChecking.SizedTypes.Syntax
init 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
init1Agda.Utils.List
initAutoOptionsAgda.Auto.Options
initCCEnvAgda.Compiler.MAlonzo.Compiler
initCommandStateAgda.Interaction.Base
initCopyInfoAgda.Syntax.Abstract
initEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initExpRefInfoAgda.Auto.SearchControl
initFreeEnvAgda.TypeChecking.Free.Lazy
initGraphAgda.Utils.Warshall
initialiseCommandQueueAgda.Interaction.InteractionTop
initLast 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
initLast1Agda.Utils.List
initLHSStateAgda.TypeChecking.Rules.LHS.ProblemRest
initMapSAgda.Auto.Convert
initMaybeAgda.Utils.List
initMetaAgda.Auto.NarrowingSearch
initNiceEnvAgda.Syntax.Concrete.Definitions.Monad
initOccursCheckAgda.TypeChecking.MetaVars.Occurs
initPersistentStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initPostScopeStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initPreScopeStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initsAgda.Utils.List1
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initWithDefaultAgda.Utils.List
InjectivePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
InjectivityAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InlinePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
InlineReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InMutual 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
inMutualBlockAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
inNameSpaceAgda.Syntax.Scope.Base
inOriginalContextAgda.TypeChecking.Unquote
inplaceSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
inputFlagAgda.Interaction.Options
InScope 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Scope.Base
inScopeBecauseAgda.Syntax.Scope.Base
InScopeSetAgda.Syntax.Scope.Base
InScopeTagAgda.Syntax.Scope.Base
inScopeTagAgda.Syntax.Scope.Base
InSeq 
1 (Type/Class)Agda.Compiler.Treeless.Subst
2 (Data Constructor)Agda.Compiler.Treeless.Subst
inSeqAgda.Compiler.Treeless.Subst
insert 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
4 (Function)Agda.Utils.Trie
5 (Function)Agda.Utils.BiMap
6 (Function)Agda.Utils.RangeMap
7 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
8 (Function)Agda.Utils.Favorites
9 (Function)Agda.Utils.AssocList
10 (Function)Agda.Termination.CallMatrix
11 (Function)Agda.Termination.CallGraph
insertAfterAgda.Compiler.JS.Compiler
insertComparedAgda.Utils.Favorites
InsertedAgda.Syntax.Common
insertEdge 
1 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function)Agda.TypeChecking.SizedTypes.WarshallSolver
insertEdgeWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
insertHiddenLambdasAgda.TypeChecking.Rules.Term
insertImplicitAgda.TypeChecking.Implicit
insertImplicit'Agda.TypeChecking.Implicit
insertImplicitBindersTAgda.TypeChecking.Implicit
insertImplicitBindersT1Agda.TypeChecking.Implicit
insertImplicitPatSynArgsAgda.Syntax.Abstract
insertImplicitPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitPatternsTAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitSizeLtPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertInspectsAgda.TypeChecking.Rules.Def
insertLookupWithKeyAgda.Utils.BiMap
insertLookupWithKeyPreconditionAgda.Utils.BiMap
insertMetaSetAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
insertMetaVarAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
insertMissingFieldsAgda.TypeChecking.Records
insertMissingFieldsFailAgda.TypeChecking.Records
insertMissingFieldsWarnAgda.TypeChecking.Records
insertMutualBlockInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
insertNamesAgda.TypeChecking.Rules.Def
insertOldInteractionScopeAgda.Interaction.InteractionTop
insertPatternsAgda.TypeChecking.Rules.Def
insertPatternsLHSCoreAgda.TypeChecking.Rules.Def
insertPreconditionAgda.Utils.BiMap
insertTrailingArgsAgda.TypeChecking.Coverage
insertWith 
1 (Function)Agda.Utils.Trie
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
insideAndOutsideAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
insideDotPatternAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
InsideOperandCtxAgda.Syntax.Fixity
InstanceAgda.Syntax.Common
InstanceArgAgda.Syntax.Concrete
InstanceArgVAgda.Syntax.Concrete.Operators.Parser
InstanceArgWithExplicitArgAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceArgWithExplicitArg_Agda.Interaction.Options.Warnings
InstanceBAgda.Syntax.Concrete
InstanceBlockAgda.Syntax.Concrete.Definitions.Types
InstanceDefAgda.Syntax.Common
InstanceNoCandidateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceNoOutputTypeNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceNoOutputTypeName_Agda.Interaction.Options.Warnings
InstancePAgda.Syntax.Concrete
InstanceSearchAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InstanceSearchDepthExhaustedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceTableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceWithExplicitArgAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceWithExplicitArg_Agda.Interaction.Options.Warnings
InstantiableAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstantiateAgda.TypeChecking.Reduce
instantiateAgda.TypeChecking.Reduce
instantiate'Agda.TypeChecking.Reduce
InstantiatedAgda.Interaction.Base
instantiateDefAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateDefinitionTypeAgda.TypeChecking.Rules.Decl
InstantiateFullAgda.TypeChecking.Reduce
instantiateFullAgda.TypeChecking.Reduce
instantiateFull'Agda.TypeChecking.Reduce
instantiateFullExceptForDefinitionsAgda.TypeChecking.Reduce
instantiateFullExceptForDefinitions'Agda.TypeChecking.Reduce
instantiateRewriteRuleAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateRewriteRulesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateTelescopeAgda.TypeChecking.Telescope
instantiateVarHeadsAgda.TypeChecking.Injectivity
inStateAgda.Syntax.Parser.LexActions
InstVAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IntAgda.Utils.Haskell.Syntax
int 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.Treeless.EliminateLiteralPatterns
IntegerAgda.Compiler.JS.Syntax
integer 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Syntax.Parser.LexActions
integerCAgda.TypeChecking.Serialise.Base
integerDAgda.TypeChecking.Serialise.Base
integerEAgda.TypeChecking.Serialise.Base
integerSemiringAgda.Termination.Semiring
integerToCharAgda.Utils.Char
InteractionAgda.Interaction.Base
Interaction'Agda.Interaction.Base
InteractionId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
interactionIdAgda.Syntax.Common
InteractionOutputCallbackAgda.Interaction.Response
InteractionPoint 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InteractionPointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InteractiveAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InteractorAgda.Main
interAssocWithAgda.Termination.SparseMatrix
interestingCallAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
interestingConstraintAgda.TypeChecking.Pretty.Constraint
Interface 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InterfaceFileAgda.Interaction.FindFile
InterleavedDataAgda.Syntax.Concrete.Definitions.Types
interleavedDataConsAgda.Syntax.Concrete.Definitions.Types
InterleavedDeclAgda.Syntax.Concrete.Definitions.Types
interleavedDeclAgda.Syntax.Concrete.Definitions.Types
interleavedDeclNumAgda.Syntax.Concrete.Definitions.Types
interleavedDeclSigAgda.Syntax.Concrete.Definitions.Types
InterleavedFunAgda.Syntax.Concrete.Definitions.Types
interleavedFunClausesAgda.Syntax.Concrete.Definitions.Types
InterleavedMutual 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
interleaveRangesAgda.Syntax.Position
InternalErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
internalErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
interpretAgda.Interaction.InteractionTop
intersection 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.SmallSet
intersectVarsAgda.TypeChecking.Conversion
intersectWithAgda.Termination.SparseMatrix
intersperseAgda.Utils.List1
Interval 
1 (Type/Class)Agda.Syntax.Position
2 (Data Constructor)Agda.Syntax.Position
intervalAgda.Syntax.Parser.Literate
Interval'Agda.Syntax.Position
intervalInvariantAgda.Syntax.Position
intervalsToRangeAgda.Syntax.Position
intervalToRangeAgda.Syntax.Position
intervalUnviewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
intervalUnview'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
IntervalViewAgda.Syntax.Internal
intervalViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
intervalView'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
IntervalWithoutFileAgda.Syntax.Position
intFilePathAgda.Interaction.FindFile
intMapAgda.Utils.Warshall
inTopContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
IntroAgda.Interaction.InteractionTop
introsAgda.Compiler.MAlonzo.Compiler
introTacticAgda.Interaction.BasicOps
intSemiringAgda.Termination.Semiring
IntSetAgda.Utils.IntSet.Infinite
intSignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
intToDoubleAgda.Utils.Float
intViewAgda.Syntax.Treeless, Agda.Compiler.Backend
InvAgda.TypeChecking.Injectivity
InvalidCatchallPragmaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidCatchallPragma_Agda.Interaction.Options.Warnings
InvalidConstructorAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidConstructorBlockAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidConstructorBlock_Agda.Interaction.Options.Warnings
InvalidConstructor_Agda.Interaction.Options.Warnings
InvalidCoverageCheckPragmaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidCoverageCheckPragma_Agda.Interaction.Options.Warnings
InvalidExtensionErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
InvalidMeasureMutualAgda.Syntax.Concrete.Definitions.Errors
InvalidNameAgda.Syntax.Concrete.Definitions.Errors
InvalidNoPositivityCheckPragmaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragma_Agda.Interaction.Options.Warnings
InvalidNoUniverseCheckPragmaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidNoUniverseCheckPragma_Agda.Interaction.Options.Warnings
InvalidPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InvalidRecordDirectiveAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidRecordDirective_Agda.Interaction.Options.Warnings
InvalidTerminationCheckPragmaAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidTerminationCheckPragma_Agda.Interaction.Options.Warnings
InvalidTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InvalidTypeSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InvariantAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
invariant 
1 (Function)Agda.Utils.IntSet.Infinite
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
InverseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
inverseApplyCohesionAgda.Syntax.Common
inverseApplyModalityButNotQuantityAgda.Syntax.Common
inverseApplyQuantityAgda.Syntax.Common
inverseApplyRelevanceAgda.Syntax.Common
inverseComposeAgda.Utils.POMonoid
inverseComposeCohesionAgda.Syntax.Common
inverseComposeModalityAgda.Syntax.Common
inverseComposeQuantityAgda.Syntax.Common
inverseComposeRelevanceAgda.Syntax.Common
InversePermuteAgda.Utils.Permutation
inversePermuteAgda.Utils.Permutation
InverseScopeLookupAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
inverseScopeLookupModuleAgda.Syntax.Scope.Base
inverseScopeLookupModule'Agda.Syntax.Scope.Base
inverseScopeLookupNameAgda.Syntax.Scope.Base
inverseScopeLookupName'Agda.Syntax.Scope.Base
inverseScopeLookupName''Agda.Syntax.Scope.Base
inverseSubstAgda.TypeChecking.MetaVars
InversionDepthReachedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InversionDepthReached_Agda.Interaction.Options.Warnings
InversionMapAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InvertAgda.Syntax.Common
InvertExceptAgda.TypeChecking.MetaVars
invertFunctionAgda.TypeChecking.Injectivity
invertPAgda.Utils.Permutation
invLookupAgda.Utils.BiMap
InvViewAgda.TypeChecking.Injectivity
ioAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
IOExceptionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IOneAgda.Syntax.Internal
iOptionsUsedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IORefAgda.Utils.IORef
iotapossmetaAgda.Auto.Typecheck
iotastepAgda.Auto.Typecheck
IOTCM 
1 (Data Constructor)Agda.Interaction.Base
2 (Type/Class)Agda.Interaction.Base
IOTCM'Agda.Interaction.Base
iPartialDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iPatternSynsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbEquationsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbMetaAppAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPBoundary 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPBoundary'Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbOverappliedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbValueAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcBoundaryAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClauseNoAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClosureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPClause 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcQNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcWithSubAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipMetaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPNoClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipSolvedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IrrelevantAgda.Syntax.Common
irrToNonStrictAgda.Syntax.Common
IsAbstractAgda.Syntax.Common
isAbsurdBodyAgda.Syntax.Internal
isAbsurdLambdaNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isAbsurdPAgda.Syntax.Concrete
isAbsurdPatternNameAgda.Syntax.Internal
isAHoleAgda.Syntax.Notation
isAliasAgda.TypeChecking.Rules.Def
isAmbiguousAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isAnonymousModuleNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
IsApplyAgda.TypeChecking.Coverage.Match
isApplyElimAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
isApplyElim'Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
IsBaseAgda.Utils.TypeLevel
IsBasicRangeMapAgda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
isBelowAgda.Utils.Warshall
isBenchmarkOnAgda.Utils.Benchmark
isBinderPAgda.Syntax.Concrete
isBinderUsedAgda.TypeChecking.Free
isBindingHoleAgda.Syntax.Notation
isBlockedAgda.TypeChecking.Reduce
isBlockedTermAgda.TypeChecking.MetaVars
isBoundedAgda.TypeChecking.SizedTypes
isBoundedProjVarAgda.TypeChecking.SizedTypes
isBoundedSizeTypeAgda.TypeChecking.SizedTypes
isBuiltinAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
isBuiltinModuleAgda.Interaction.Options.Lenses
isBuiltinModuleWithSafePostulatesAgda.Interaction.Options.Lenses
isBuiltinNoDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
isCanonicalAgda.TypeChecking.Conversion
isClosedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
isCodeAgda.Syntax.Parser.Literate
isCodeLayerAgda.Syntax.Parser.Literate
isCoFibrantSortAgda.TypeChecking.Irrelevance
isCoinductiveAgda.TypeChecking.Rules.Data
isCoinductiveProjectionAgda.Termination.Monad
isConAgda.TypeChecking.Unquote
isConNameAgda.Syntax.Scope.Base
isCopatternLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iScopeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isCoveredAgda.TypeChecking.Coverage
IsData 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.TypeChecking.Rules.LHS
IsDataModuleAgda.Syntax.Scope.Base
isDataOrRecordAgda.TypeChecking.Datatypes
isDataOrRecordTypeAgda.TypeChecking.Datatypes
isDatatypeAgda.TypeChecking.Datatypes
isDatatypeModuleAgda.Syntax.Scope.Monad
isDebugPrintingAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isDecrAgda.Termination.Order
isDefAgda.TypeChecking.Unquote
isDefAccountAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isDefaultImportDirAgda.Syntax.Common
isDefNameAgda.Syntax.Scope.Base
IsDominatedAgda.Utils.Favorites
isDontExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IsEllipsisAgda.Syntax.Concrete.Pattern
isEllipsisAgda.Syntax.Concrete.Pattern
IsEmptyAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isEmpty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Termination.SparseMatrix
isEmptyFunctionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isEmptyObjectAgda.Compiler.JS.Compiler
isEmptyTelAgda.TypeChecking.Empty
IsEmptyTypeAgda.Interaction.Base
isEmptyTypeAgda.TypeChecking.Empty
isEnabledAgda.Compiler.Backend
isEqualityTypeAgda.Syntax.Internal
isErasableAgda.Compiler.Treeless.Erase
isErasedAgda.Syntax.Common
isEtaConAgda.TypeChecking.Records
isEtaExpandableAgda.TypeChecking.MetaVars
isEtaOrCoinductiveRecordConstructorAgda.TypeChecking.Records
isEtaRecordAgda.TypeChecking.Records
isEtaRecordTypeAgda.TypeChecking.Records
isEtaVarAgda.TypeChecking.Records
IsExprAgda.Syntax.Concrete.Operators.Parser
isExtendedLambdaNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IsFamAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
IsFibrant 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
isFibrantAgda.TypeChecking.Irrelevance
isFlexibleAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
IsFlexiblePatternAgda.TypeChecking.Rules.LHS
isFlexiblePatternAgda.TypeChecking.Rules.LHS
isFlexNodeAgda.TypeChecking.SizedTypes.WarshallSolver
IsForcedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isForcedAgda.TypeChecking.Forcing
IsFreeAgda.TypeChecking.Free.Reduce
isFrozenAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isFullyInstantiatedMetaAgda.TypeChecking.Reduce
isFunNameAgda.Syntax.Concrete.Definitions.Types
isGeneralizableMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isGeneratedRecordConstructorAgda.TypeChecking.Records
isHoleAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsIApplyAgda.TypeChecking.Coverage.Match
iSignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isImportedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
IsIndexAgda.TypeChecking.Positivity.Occurrence
isInductiveRecordAgda.TypeChecking.Records
IsInfixAgda.Syntax.Common
isInfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInftyNodeAgda.TypeChecking.SizedTypes.WarshallSolver
isInlineFunAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isInModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInsertedHiddenAgda.Syntax.Common
isInsideDotPatternAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
IsInstanceAgda.Syntax.Common
isInstanceAgda.Syntax.Common
isInstanceConstraintAgda.TypeChecking.InstanceArguments
IsInstantiatedMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInstantiatedMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInstantiatedMeta'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInteractionMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInterleavedDataAgda.Syntax.Concrete.Definitions.Types
isInterleavedFunAgda.Syntax.Concrete.Definitions.Types
isInternalAccountAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isIntervalAgda.TypeChecking.Telescope.Path
isIOneAgda.Syntax.Internal
isIrrelevantAgda.Syntax.Common
isIrrelevantOrPropMAgda.TypeChecking.Irrelevance
isJust 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
isLabeledAgda.Syntax.Concrete.Pretty
isLambdaHoleAgda.Syntax.Notation
isLeChildModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLeftAgda.Utils.Either
isLeParentModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLevelTypeAgda.TypeChecking.Level
IsLHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isLocalAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
IsLockAgda.Syntax.Common
isLtChildModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isLtParentModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
IsMacroAgda.Syntax.Common
isMacroAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IsMain 
1 (Type/Class)Agda.Compiler.Backend, Agda.Compiler.Common
2 (Data Constructor)Agda.Compiler.Backend, Agda.Compiler.Common
IsMetaAgda.TypeChecking.Reduce
isMetaAgda.TypeChecking.Reduce
isMetaTCWarningAgda.TypeChecking.Warnings
isMetaWarningAgda.TypeChecking.Warnings
isModCharAgda.Compiler.MAlonzo.Misc
isModuleAccountAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
isModuleFreeVarAgda.TypeChecking.Rules.Term
isNameAgda.Interaction.BasicOps
isNameInScopeAgda.Syntax.Scope.Base
isNameInScopeUnqualifiedAgda.Syntax.Scope.Base
isNegInfAgda.Utils.Float
isNegZeroAgda.Utils.Float
isNeutralAgda.TypeChecking.MetaVars.Occurs
isNewerThanAgda.Utils.FileName
IsNoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isNoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isNonfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonStrictAgda.Syntax.Common
isNormalHoleAgda.Syntax.Notation
IsNotAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
isNothing 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
IsNotLockAgda.Syntax.Common
isolatedNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
isOpenMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isOpenMixfixAgda.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
isOrderAgda.Termination.Order
iSourceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iSourceHashAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isOverlappableAgda.Syntax.Common
isPathAgda.TypeChecking.Telescope
IsPathConsAgda.TypeChecking.Rules.Data
isPathTypeAgda.Syntax.Internal
IsPatSynAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isPatternAgda.Syntax.Concrete
isPosInfAgda.Utils.Float
isPostfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPosZeroAgda.Utils.Float
isPrefixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsPrefixOfAgda.TypeChecking.Abstract
isPrefixOf 
1 (Function)Agda.Utils.List1
2 (Function)Agda.TypeChecking.Abstract
isPrimEqAgda.Syntax.Treeless, Agda.Compiler.Backend
isPrimitiveAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
isPrimitiveModuleAgda.Interaction.Options.Lenses
isProblemSolvedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
isProjectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isProjectionButNotCoinductiveAgda.Termination.Monad
isProjection_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
IsProjElimAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
isProjElimAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
IsProjPAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isProjPAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
isPropEnabledAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isProperProjectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isPropMAgda.TypeChecking.Irrelevance
isQNameAgda.Interaction.BasicOps
isQualifiedAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isQuantityAttributeAgda.Syntax.Concrete.Attribute
isReconstructedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IsRecord 
1 (Data Constructor)Agda.Syntax.Internal
2 (Data Constructor)Agda.TypeChecking.Rules.LHS
isRecordAgda.TypeChecking.Records
isRecordConstructorAgda.TypeChecking.Records
isRecordDirectiveAgda.Syntax.Concrete
IsRecordModuleAgda.Syntax.Scope.Base
isRecordTypeAgda.TypeChecking.Records
isRecursiveRecordAgda.TypeChecking.Records
IsReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isReducedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isRelevanceAttributeAgda.Syntax.Concrete.Attribute
isRelevantAgda.Syntax.Common
isRelevantProjectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isRelevantProjection_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isRightAgda.Utils.Either
isSafeIntegerAgda.Utils.Float
isSingleIdentifierPAgda.Syntax.Concrete
isSingletonAgda.Termination.SparseMatrix
isSingletonRecordAgda.TypeChecking.Records
isSingletonRecord'Agda.TypeChecking.Records
isSingletonRecordModuloRelevanceAgda.TypeChecking.Records
isSingletonTypeAgda.TypeChecking.Records
isSingletonType'Agda.TypeChecking.Records
isSingletonTypeModuloRelevanceAgda.TypeChecking.Records
isSizeConstraintAgda.TypeChecking.SizedTypes
isSizeConstraint_Agda.TypeChecking.SizedTypes
isSizeNameTestAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeNameTestRawAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeProblemAgda.TypeChecking.SizedTypes
IsSizeTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeTypeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeTypeTestAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSmallSortAgda.TypeChecking.Substitute
isSolvingConstraintsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
IsSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isSortAgda.Syntax.Internal
isSortMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isSortMeta_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isStaticFunAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
IsStrictAgda.Syntax.Internal
isStronglyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isSublistOfAgda.Utils.List
isSubscriptDigitAgda.Utils.Suffix
isSubsetOf 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.SmallSet
isSurrogateCodePointAgda.Utils.Char
isTacticAttributeAgda.Syntax.Concrete.Attribute
iStartAgda.Syntax.Position
isTimelessAgda.TypeChecking.Lock
isTopAgda.TypeChecking.SizedTypes.Utils
isTopLevelValueAgda.Compiler.JS.Compiler
isTrivialPatternAgda.TypeChecking.Coverage.Match
isTwoLevelEnabledAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isTypeAgda.TypeChecking.Rules.Term
isType'Agda.TypeChecking.Rules.Term
IsTypeCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isTypeEqualToAgda.TypeChecking.Rules.Term
IsType_Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isType_Agda.TypeChecking.Rules.Term
isUnderscoreAgda.Syntax.Common
isUnguardedAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isUnnamedAgda.Syntax.Common
isUnqualifiedAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isUnreachableAgda.Syntax.Treeless, Agda.Compiler.Backend
isUnsolvedWarningAgda.TypeChecking.Warnings
isUntypedBuiltinAgda.TypeChecking.Rules.Builtin
isValidJSIdentAgda.Compiler.JS.Pretty
isVarAgda.TypeChecking.CompiledClause.Compile
IsVarSetAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isWeaklyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
IsWithPAgda.Syntax.Concrete.Pattern
isWithPAgda.Syntax.Concrete.Pattern
isWithPatternAgda.Syntax.Concrete.Pattern
isZeroNodeAgda.TypeChecking.SizedTypes.WarshallSolver
ItemAgda.TypeChecking.Positivity
iterateAgda.Utils.List1
iterate'Agda.Utils.Function
iterateSolverAgda.TypeChecking.SizedTypes.WarshallSolver
iterateUntilAgda.Utils.Function
iterateUntilMAgda.Utils.Function
iterWhileAgda.Utils.Function
iUserWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IVarAgda.Utils.Haskell.Syntax
iWarningsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IxAgda.Utils.SmallSet
IZeroAgda.Syntax.Internal