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

Index - I

IApplyAgda.Syntax.Internal
IApplyPAgda.Syntax.Internal
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
Id 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Auto.Syntax
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
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 (Data Constructor)Agda.Compiler.JS.Syntax
3 (Type/Class)Agda.Utils.TypeLevel
ifBlockedAgda.TypeChecking.Reduce
ifDirtyAgda.Utils.Update
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
ifNotNullAgda.Utils.Null
ifNotNullMAgda.Utils.Null
ifNotPiAgda.TypeChecking.Telescope
ifNotPiOrPathTypeAgda.TypeChecking.Telescope
ifNotPiTypeAgda.TypeChecking.Telescope
ifNullAgda.Utils.Null
ifNullMAgda.Utils.Null
iForeignCodeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ifPathAgda.TypeChecking.Rules.Term
ifPiAgda.TypeChecking.Telescope
ifPiTypeAgda.TypeChecking.Telescope
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
ignoreAllInterfacesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ignoreBlockingAgda.Syntax.Internal
IgnoreInAnnotationsAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
ignoreInterfacesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
iInsideScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ilamAgda.TypeChecking.Names
iLengthAgda.Syntax.Position
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
IllformedProjectionPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
illiterateAgda.Syntax.Parser.Literate
IlltypedPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad, Agda.Compiler.Backend
IMaxAgda.Syntax.Internal
imaxAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
IMinAgda.Syntax.Internal
iminAgda.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
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
importQualifiedAgda.Utils.Haskell.Syntax
importsAgda.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
ImpossibleConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ImpossiblePragmaAgda.Syntax.Concrete
impossibleTermAgda.Syntax.Internal
impossibleTestAgda.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
includeStateChangesAgda.Interaction.Imports
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.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.Utils.String
independentAgda.Interaction.InteractionTop
Index 
1 (Type/Class)Agda.Utils.IndexedList
2 (Data Constructor)Agda.Utils.Suffix
indexWithDefaultAgda.Utils.List
IndirectAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InductionAgda.Syntax.Common
InductiveAgda.Syntax.Common
INegAgda.Syntax.Internal
InfAgda.Syntax.Internal
infAgda.TypeChecking.Positivity
InfectiveImportAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InfectiveImport_Agda.Interaction.Options.Warnings
infectiveOptionsAgda.Interaction.Options
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
inferMetaAgda.TypeChecking.Rules.Term
inferPiSortAgda.TypeChecking.Sort
InferredAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
inferSortAgda.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
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InftyAgda.TypeChecking.SizedTypes.Syntax
initAutoOptionsAgda.Auto.Options
initCCEnvAgda.Compiler.MAlonzo.Compiler
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
initialDotStateAgda.Interaction.Highlighting.Dot
initialiseCommandQueueAgda.Interaction.InteractionTop
initLastAgda.Utils.List
initLHSStateAgda.TypeChecking.Rules.LHS.ProblemRest
initMapSAgda.Auto.Convert
initMaybeAgda.Utils.List
initMetaAgda.Auto.NarrowingSearch
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
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InjectivePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
InjectivityAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InlinePragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
InlineReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.BiMap
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
4 (Function)Agda.Utils.Trie
5 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)Agda.Utils.Favorites
7 (Function)Agda.Utils.AssocList
8 (Function)Agda.Termination.CallMatrix
9 (Function)Agda.Termination.CallGraph
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
insertImplicitPatSynArgsAgda.Syntax.Abstract
insertImplicitPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitPatternsTAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitSizeLtPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertMetaSetAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
insertMetaVarAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertMissingFieldsAgda.TypeChecking.Records
insertMutualBlockInfoAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
insertOldInteractionScopeAgda.Interaction.InteractionTop
insertPatternsAgda.TypeChecking.Rules.Def
insertPatternsLHSCoreAgda.TypeChecking.Rules.Def
insertTrailingArgsAgda.TypeChecking.Coverage
insertWith 
1 (Function)Agda.Utils.Trie
2 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
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
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
instanceTransformBiMT'Agda.Utils.Geniplate
instanceUniverseBiT'Agda.Utils.Geniplate
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
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
inStateAgda.Syntax.Parser.LexActions
InstVAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
InteractionAgda.Interaction.Base
interactionAgda.Interaction.CommandLine
Interaction'Agda.Interaction.Base
InteractionId 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
interactionIdAgda.Syntax.Common
interactionLoopAgda.Interaction.CommandLine
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
InteractiveAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interAssocWithAgda.Termination.SparseMatrix
interestingCallAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interestingConstraintAgda.TypeChecking.Pretty.Warning
Interface 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InterfaceFileAgda.Interaction.FindFile
interleaveRangesAgda.Syntax.Position
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.SmallSet
intersectVarsAgda.TypeChecking.Conversion
intersectWithAgda.Termination.SparseMatrix
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.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
introsAgda.Compiler.MAlonzo.Compiler
introTacticAgda.Interaction.BasicOps
intSemiringAgda.Termination.Semiring
IntSetAgda.Utils.IntSet.Infinite
intViewAgda.Syntax.Treeless, Agda.Compiler.Backend
InvAgda.TypeChecking.Injectivity
InvalidCatchallPragmaAgda.Syntax.Concrete.Definitions
InvalidCatchallPragma_Agda.Interaction.Options.Warnings
InvalidCoverageCheckPragmaAgda.Syntax.Concrete.Definitions
InvalidCoverageCheckPragma_Agda.Interaction.Options.Warnings
InvalidExtensionErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
InvalidMeasureMutualAgda.Syntax.Concrete.Definitions
InvalidNameAgda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragmaAgda.Syntax.Concrete.Definitions
InvalidNoPositivityCheckPragma_Agda.Interaction.Options.Warnings
InvalidNoUniverseCheckPragmaAgda.Syntax.Concrete.Definitions
InvalidNoUniverseCheckPragma_Agda.Interaction.Options.Warnings
InvalidPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTerminationCheckPragmaAgda.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
inverseApplyModalityAgda.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
inverseScopeLookupAgda.Syntax.Scope.Base
inverseScopeLookup'Agda.Syntax.Scope.Base
inverseScopeLookupModuleAgda.Syntax.Scope.Base
inverseScopeLookupNameAgda.Syntax.Scope.Base
inverseScopeLookupName'Agda.Syntax.Scope.Base
inverseSubstAgda.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
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
ipbEquationsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbMetaAppAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPBoundary 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPBoundary'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbOverappliedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipbValueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ipcBoundaryAgda.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
ipMetaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IPNoClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iPragmaOptionsAgda.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
IrrelevantDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
isApplyElim'Agda.Syntax.Internal
IsBaseAgda.Utils.TypeLevel
isBelowAgda.Utils.Warshall
isBenchmarkOnAgda.Utils.Benchmark
isBinderPAgda.Syntax.Concrete
isBinderUsedAgda.TypeChecking.Free
isBindingHoleAgda.Syntax.Notation
isBlockedAgda.TypeChecking.Reduce
isBlockedTermAgda.TypeChecking.MetaVars
isBoundedAgda.TypeChecking.SizedTypes
isBuiltinAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
isBuiltinModuleAgda.Interaction.Options.Lenses
isBuiltinModuleWithSafePostulatesAgda.Interaction.Options.Lenses
isCachedAgda.Interaction.Imports
isCanonicalAgda.TypeChecking.Conversion
isClosedAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCodeAgda.Syntax.Parser.Literate
isCodeLayerAgda.Syntax.Parser.Literate
isCoinductiveAgda.TypeChecking.Rules.Data
isCoinductiveProjectionAgda.Termination.Monad
isConAgda.TypeChecking.Unquote
isCopatternLHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
iScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isCoveredAgda.TypeChecking.Coverage
IsDataAgda.Syntax.Common
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.Utils.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
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.TypeChecking.Monad, Agda.Compiler.Backend
IsFamAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
isFullyInstantiatedMetaAgda.TypeChecking.Reduce
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
isImportedAgda.TypeChecking.Monad.Imports, 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.InstanceArguments
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
isInternalAccountAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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.TypeChecking.Monad, Agda.Compiler.Backend
isLocalAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isMainFunctionAgda.Compiler.MAlonzo.Primitives
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
isNameInScopeAgda.Syntax.Scope.Base
isNeutralAgda.TypeChecking.MetaVars.Occurs
isNewerThanAgda.Interaction.Imports
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.Cubical, Agda.TypeChecking.Primitive
isNothing 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
isolatedNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
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
isPathTypeAgda.Syntax.Internal
IsPatSynAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPatternAgda.Syntax.Concrete
isPostfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsPrefixOfAgda.TypeChecking.Abstract
isPrefixOfAgda.TypeChecking.Abstract
isPrimEqAgda.Syntax.Treeless, Agda.Compiler.Backend
isPrimitiveAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isProjElimAgda.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
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
IsRecordAgda.Syntax.Common
isRecordAgda.TypeChecking.Records
isRecordConstructorAgda.TypeChecking.Records
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
isRightAgda.Utils.Either
isSetAgda.Syntax.Abstract.Views
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
isSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isSortAgda.Syntax.Internal
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
isStronglyRigidAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isSublistOfAgda.Utils.List
isSubscriptDigitAgda.Utils.Suffix
isSubsetOf 
1 (Function)Agda.Utils.VarSet
2 (Function)Agda.Utils.SmallSet
isTacticAttributeAgda.Syntax.Concrete.Attribute
iStartAgda.Syntax.Position
isTopAgda.TypeChecking.SizedTypes.Utils
isTopLevelValueAgda.Compiler.JS.Compiler
isTrivialPatternAgda.TypeChecking.Coverage.Match
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
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
isVisitedAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
iterate'Agda.Utils.Function
iterateSolverAgda.TypeChecking.SizedTypes.WarshallSolver
iterateUntilAgda.Utils.Function
iterateUntilMAgda.Utils.Function
iterWhileAgda.Utils.Function
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