Agda-2.6.3.20230805: 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
iApplyVarsAgda.TypeChecking.Telescope.Path
iBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ICOptionAgda.Interaction.Options
icOptionActiveAgda.Interaction.Options
icOptionDescriptionAgda.Interaction.Options
icOptionKindAgda.Interaction.Options
icOptionOKAgda.Interaction.Options
icOptionWarningAgda.Interaction.Options
Id 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Auto.Syntax
iDefaultPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
idPAgda.Utils.Permutation
IdPartAgda.Syntax.Common
IdSAgda.Syntax.Internal, Agda.TypeChecking.Substitute
idSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
idViewAsPathAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iEndAgda.Syntax.Position
If 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Utils.TypeLevel
3 (Data Constructor)Agda.Compiler.JS.Syntax
ifBlockedAgda.TypeChecking.Reduce
ifDirtyAgda.Utils.Update
iFilePragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iFileTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ifNotPathBAgda.TypeChecking.Telescope
ifNotPiAgda.TypeChecking.Telescope
ifNotPiOrPathBAgda.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.TypeChecking.Monad, Agda.Compiler.Backend
ifPathAgda.TypeChecking.Telescope
ifPathBAgda.TypeChecking.Telescope
ifPiAgda.TypeChecking.Telescope
ifPiBAgda.TypeChecking.Telescope
ifPiOrPathBAgda.TypeChecking.Telescope
ifPiTypeAgda.TypeChecking.Telescope
ifPiTypeBAgda.TypeChecking.Telescope
ifThenElseAgda.Utils.Boolean
ifTopLevelAndHighlightingLevelIsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifTopLevelAndHighlightingLevelIsOrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iFullHashAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreAbstractAgda.Interaction.Base
IgnoreAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
IgnoreSortsAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
iHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ihnameAgda.Compiler.MAlonzo.Misc
iImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iImportWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IInfoAgda.TypeChecking.Coverage.SplitClause
iInsideScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ilamAgda.TypeChecking.Names
iLengthAgda.Syntax.Position
IllegalAgda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify
IllegalDeclarationInDataDefinitionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalHidingInPostfixProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalLetInTelescopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalPatternInTelescopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedAsClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedAsClause_Agda.Interaction.Options.Warnings
IllformedProjectionPatternAbstractAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedProjectionPatternConcreteAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
illiterateAgda.Syntax.Parser.Literate
IMAgda.Interaction.Monad
IMaxAgda.Syntax.Internal
imaxAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
iMetaBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IMinAgda.Syntax.Internal
iminAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
imoduleMapAgda.Syntax.Scope.Monad
iModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ImpInsertAgda.TypeChecking.Implicit
implicitArgsAgda.TypeChecking.Implicit
ImplicitFlexAgda.TypeChecking.Rules.LHS.Problem
ImplicitInsertionAgda.TypeChecking.Implicit
implicitNamedArgsAgda.TypeChecking.Implicit
implicitPAgda.TypeChecking.Rules.LHS.Implicit
implies 
1 (Function)Agda.Utils.Boolean
2 (Function)Agda.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
ImportSAgda.Syntax.Abstract
importsAgda.Compiler.JS.Syntax
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
inConcreteModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inConcreteOrAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
IndexedClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IndexedClauseArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
indexWithDefaultAgda.Utils.List
IndirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Induction 
1 (Type/Class)Agda.Syntax.Common.Aspect, Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Concrete
InductiveAgda.Syntax.Common.Aspect, Agda.Syntax.Common
INegAgda.Syntax.Internal
inegAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
InfAgda.Syntax.Internal
infAgda.TypeChecking.Positivity
infallibleSortKitAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InfectiveAgda.Interaction.Options
InfectiveCoinfectiveAgda.Interaction.Options
InfectiveCoinfectiveOptionAgda.Interaction.Options
infectiveCoinfectiveOptionsAgda.Interaction.Options
InfectiveImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InfectiveImport_Agda.Interaction.Options.Warnings
inferAgda.TypeChecking.CheckInternal
inferApplicationAgda.TypeChecking.Rules.Application
InferDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InferExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferExprAgda.TypeChecking.Rules.Term, Agda.TheTypeChecker
inferExpr'Agda.TypeChecking.Rules.Term
inferExprForWithAgda.TypeChecking.Rules.Term
inferFunSortAgda.TypeChecking.Sort
inferInternalAgda.TypeChecking.CheckInternal
inferInternal'Agda.TypeChecking.CheckInternal
inferMetaAgda.TypeChecking.Rules.Term
inferNeutralAgda.TypeChecking.ProjectionLike
inferPiSortAgda.TypeChecking.Sort
InferredAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
inferSpineAgda.TypeChecking.CheckInternal
infertypevarAgda.Auto.CaseSplit
inferUnivSortAgda.TypeChecking.Sort
InferVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
infoEqLHSAgda.TypeChecking.Coverage.SplitClause
infoEqRHSAgda.TypeChecking.Coverage.SplitClause
infoEqTelAgda.TypeChecking.Coverage.SplitClause
infoLeftInvAgda.TypeChecking.Coverage.SplitClause
infoRhoAgda.TypeChecking.Coverage.SplitClause
infoTauAgda.TypeChecking.Coverage.SplitClause
infoTelAgda.TypeChecking.Coverage.SplitClause
infoTel0Agda.TypeChecking.Coverage.SplitClause
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InfSAgda.Syntax.Reflected
InftyAgda.TypeChecking.SizedTypes.Syntax
init 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
init1Agda.Utils.List
initAutoOptionsAgda.Auto.Options
initCommandStateAgda.Interaction.Base
initCopyInfoAgda.Syntax.Abstract
initEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initExpRefInfoAgda.Auto.SearchControl
initFreeEnvAgda.TypeChecking.Free.Lazy
initGraphAgda.Utils.Warshall
initialiseCommandQueueAgda.Interaction.InteractionTop
initialMetaIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
initPostScopeStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initPreScopeStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initsAgda.Utils.List1
inits1Agda.Utils.List1
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initUnifyStateAgda.TypeChecking.Rules.LHS.Unify.Types
initWithDefaultAgda.Utils.List
injectAtAgda.TypeChecking.Rules.LHS.Unify.Types
injectConstructorAgda.TypeChecking.Rules.LHS.Unify.Types
injectDatatypeAgda.TypeChecking.Rules.LHS.Unify.Types
injectIndicesAgda.TypeChecking.Rules.LHS.Unify.Types
InjectivePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
Injectivity 
1 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify.Types
injectParametersAgda.TypeChecking.Rules.LHS.Unify.Types
injectTypeAgda.TypeChecking.Rules.LHS.Unify.Types
InlineNoExactSplitAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InlineNoExactSplit_Agda.Interaction.Options.Warnings
InlinePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
InlineReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InMutual 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Types
inMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.HashTable
3 (Function)Agda.Utils.BoolSet
4 (Function)Agda.Utils.Bag
5 (Function)Agda.Utils.SmallSet
6 (Function)Agda.Utils.Trie
7 (Function)Agda.Utils.BiMap
8 (Function)Agda.Utils.Favorites
9 (Function)Agda.Utils.AssocList
10 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
11 (Function)Agda.Termination.CallMatrix
12 (Function)Agda.Termination.CallGraph
13 (Function)Agda.Utils.RangeMap
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.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertMissingFieldsAgda.TypeChecking.Records
insertMissingFieldsFailAgda.TypeChecking.Records
insertMissingFieldsWarnAgda.TypeChecking.Records
insertMutualBlockInfoAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InsideOperandCtxAgda.Syntax.Fixity
InstanceAgda.Syntax.Common
InstanceArgAgda.Syntax.Concrete
InstanceArgVAgda.Syntax.Concrete.Operators.Parser
InstanceArgWithExplicitArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceArgWithExplicitArg_Agda.Interaction.Options.Warnings
InstanceBAgda.Syntax.Concrete
InstanceBlockAgda.Syntax.Concrete.Definitions.Types
InstanceDefAgda.Syntax.Common
InstanceNoCandidateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoOutputTypeNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoOutputTypeName_Agda.Interaction.Options.Warnings
InstancePAgda.Syntax.Concrete
InstanceSearchAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InstanceSearchDepthExhaustedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceTableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceWithExplicitArgAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceWithExplicitArg_Agda.Interaction.Options.Warnings
InstantiableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstantiateAgda.TypeChecking.Reduce
instantiateAgda.TypeChecking.Reduce
instantiate'Agda.TypeChecking.Reduce
InstantiatedAgda.Interaction.Base
instantiateDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateDefinitionTypeAgda.TypeChecking.Rules.Decl
InstantiateFullAgda.TypeChecking.Reduce
instantiateFullAgda.TypeChecking.Reduce
instantiateFull'Agda.TypeChecking.Reduce
instantiateFullExceptForDefinitionsAgda.TypeChecking.Reduce
instantiateRewriteRuleAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateRewriteRulesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateTelescopeAgda.TypeChecking.Telescope
instantiateVarHeadsAgda.TypeChecking.Injectivity
instantiateWhenAgda.TypeChecking.Reduce
Instantiation 
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
inStateAgda.Syntax.Parser.LexActions
instBodyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstVAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntAgda.Utils.Haskell.Syntax
int 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.Compiler.Treeless.EliminateLiteralPatterns
IntegerAgda.Compiler.JS.Syntax
integer 
1 (Function)Agda.Syntax.Common.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
interactionIdToMetaIdAgda.Interaction.BasicOps
InteractionMetaBoundariesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InteractionMetaBoundaries_Agda.Interaction.Options.Warnings
InteractionOutputCallbackAgda.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
InteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Interactive 
1 (Data Constructor)Agda.Utils.ProfileOptions
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InteractorAgda.Main
interAssocWithAgda.Termination.SparseMatrix
interestingCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interestingConstraintAgda.TypeChecking.Pretty.Constraint
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
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
InternalAgda.Utils.ProfileOptions
InternalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
internalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interpretAgda.Interaction.InteractionTop
intersection 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.BoolSet
3 (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
intervalSortAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
intervalsToRangeAgda.Syntax.Position
intervalToRangeAgda.Syntax.Position
IntervalUnivAgda.Syntax.Internal
intervalUnviewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
intervalUnview'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntervalViewAgda.Syntax.Internal
intervalViewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
intervalView'Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntervalWithoutFileAgda.Syntax.Position
intFilePathAgda.Interaction.FindFile
intMapAgda.Utils.Warshall
inTopContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IntroAgda.Interaction.InteractionTop
introTacticAgda.Interaction.BasicOps
intSemiringAgda.Termination.Semiring
IntSetAgda.Utils.IntSet.Infinite
intSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTypeSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
invariant 
1 (Function)Agda.Utils.IntSet.Infinite
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
InverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
inverseSubst'Agda.TypeChecking.MetaVars
InversionDepthReachedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InversionDepthReached_Agda.Interaction.Options.Warnings
InversionMapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvertAgda.Syntax.Common
InvertExceptAgda.TypeChecking.MetaVars
invertFunctionAgda.TypeChecking.Injectivity
invertPAgda.Utils.Permutation
invLookupAgda.Utils.BiMap
InvViewAgda.TypeChecking.Injectivity
ioAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
IOExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IOneAgda.Syntax.Internal
iOpaqueBlocksAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iOpaqueNamesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iOptionsUsedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
iPatternSynsAgda.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
ipBoundaryAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPBoundary'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcClauseNoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcClosureAgda.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
ipClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcQNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcWithSubAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPFace' 
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
ipMetaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPNoClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipSolvedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IrrelevantAgda.Syntax.Common
irrToNonStrictAgda.Syntax.Common
IsAbstractAgda.Syntax.Common
isAbsurdBodyAgda.Syntax.Internal
isAbsurdLambdaNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isAbsurdPAgda.Syntax.Concrete
isAbsurdPatternNameAgda.Syntax.Internal
isAccessibleDefAgda.TypeChecking.Opacity
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
isBinderAgda.Syntax.Notation
isBinderPAgda.Syntax.Concrete
isBinderUsedAgda.TypeChecking.Free
isBlockedAgda.TypeChecking.Reduce
isBlockedTermAgda.TypeChecking.MetaVars
IsBoolAgda.Utils.Boolean
isBoundaryConstraintAgda.TypeChecking.Pretty.Warning
isBoundedAgda.TypeChecking.SizedTypes
isBoundedProjVarAgda.TypeChecking.SizedTypes
isBoundedSizeTypeAgda.TypeChecking.SizedTypes
IsBuiltinAgda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isBuiltinAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
isBuiltinModuleAgda.Interaction.Options.Lenses
isBuiltinModuleWithSafePostulatesAgda.Interaction.Options.Lenses
isBuiltinNoDefAgda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCanonicalAgda.TypeChecking.Conversion
isClosedAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isConstructorAgda.TypeChecking.Datatypes
isCopatternLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCoveredAgda.TypeChecking.Coverage
isCubicalSubtypeAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
IsEllipsisAgda.Syntax.Concrete.Pattern
isEllipsisAgda.Syntax.Concrete.Pattern
IsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isEmpty 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.Termination.SparseMatrix
isEmptyFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsExprAgda.Syntax.Concrete.Operators.Parser
isExtendedLambdaNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isFaceConstraintAgda.TypeChecking.MetaVars
IsFamAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
IsFibrant 
1 (Type/Class)Agda.Syntax.Internal.Univ, Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal.Univ, 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.TypeChecking.Monad, Agda.Compiler.Backend
isForcedAgda.TypeChecking.Forcing
IsFreeAgda.TypeChecking.Free.Reduce
isFrozenAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isFunNameAgda.Syntax.Concrete.Definitions.Types
isGeneralizableMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isGeneratedRecordConstructorAgda.TypeChecking.Records
isHoleAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsIApplyAgda.TypeChecking.Coverage.Match
iSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsIndexAgda.TypeChecking.Positivity.Occurrence
isInductiveRecordAgda.TypeChecking.Records
IsInfixAgda.Syntax.Common
isInfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInftyNodeAgda.TypeChecking.SizedTypes.WarshallSolver
isInlineFunAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsInstanceAgda.Syntax.Common
isInstanceAgda.Syntax.Common
isInstanceConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend
IsInstantiatedMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInstantiatedMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInstantiatedMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInteractionMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isInteractionMetaBAgda.TypeChecking.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
isLambdaNotationAgda.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
isLevelUniverseEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsListAgda.Utils.List1
isLocalAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
IsMain 
1 (Type/Class)Agda.Compiler.Common, Agda.Compiler.Backend
2 (Data Constructor)Agda.Compiler.Common, Agda.Compiler.Backend
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
isNameOfUnivAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
IsNotAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
isNothing 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
IsNotLockAgda.Syntax.Common
isolatedNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
IsOpaqueAgda.Syntax.Common
isOpenMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
iSourceHashAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isOverlappableAgda.Syntax.Common
isPathAgda.TypeChecking.Telescope
IsPathConsAgda.TypeChecking.Rules.Data
isPathConsAgda.TypeChecking.Datatypes
isPathTypeAgda.Syntax.Internal
IsPatSynAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPrimitiveModuleAgda.Interaction.Options.Lenses
isProblemSolvedAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjectionButNotCoinductiveAgda.Termination.Monad
isProjection_Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
isProperApplyElimAgda.Syntax.Internal.Elim, Agda.Syntax.Internal
isProperProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPropMAgda.TypeChecking.Irrelevance
isQNameAgda.Interaction.BasicOps
isQualifiedAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isQuantityAttributeAgda.Syntax.Concrete.Attribute
isReconstructedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
isReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isRelevanceAttributeAgda.Syntax.Concrete.Attribute
isRelevantAgda.Syntax.Common
isRelevantProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isRelevantProjection_Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isRemoteMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeNameTestRawAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeProblemAgda.TypeChecking.SizedTypes
IsSizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSizeTypeTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSmallSortAgda.TypeChecking.Substitute
isSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSortAgda.Syntax.Internal
isSortJudgementAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSortMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSortMeta_Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isStaticFunAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsStrictAgda.Syntax.Internal.Univ, Agda.Syntax.Internal
isStrictDataSortAgda.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.BoolSet
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.TypeChecking.Monad, Agda.Compiler.Backend
isTypeAgda.TypeChecking.Rules.Term
isType'Agda.TypeChecking.Rules.Term
IsTypeCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isTypeEqualToAgda.TypeChecking.Rules.Term
IsType_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isType_Agda.TypeChecking.Rules.Term
isUnderscoreAgda.Syntax.Common
isUnguardedAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isUnifyStateSolvedAgda.TypeChecking.Rules.LHS.Unify.Types
isUnnamedAgda.Syntax.Common
isUnqualifiedAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isUnreachableAgda.Syntax.Treeless, Agda.Compiler.Backend
isUnsolvedWarningAgda.TypeChecking.Warnings
isUnstableDefAgda.TypeChecking.Injectivity
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
Item 
1 (Type/Class)Agda.Utils.List1, Agda.Utils.List1
2 (Type/Class)Agda.TypeChecking.Positivity
iterateAgda.Utils.List1
iterate'Agda.Utils.Function
iterateSolverAgda.TypeChecking.SizedTypes.WarshallSolver
iterateUntilAgda.Utils.Function
iterateUntilMAgda.Utils.Function
iterWhileAgda.Utils.Function
iTopLevelModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iUserWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IVarAgda.Utils.Haskell.Syntax
iWarningsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IxAgda.Utils.SmallSet
IZeroAgda.Syntax.Internal