| IApply | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| IApplyP | Agda.Syntax.Internal |
| iApplyVars | Agda.TypeChecking.Telescope.Path |
| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ICArgList | Agda.Auto.Syntax |
| ICExp | Agda.Auto.Syntax |
| icnvh | Agda.Auto.Convert |
| ICODE | Agda.TypeChecking.Serialise.Base |
| icode | Agda.TypeChecking.Serialise.Base |
| icodeArgs | Agda.TypeChecking.Serialise.Base |
| icodeDouble | Agda.TypeChecking.Serialise.Base |
| icodeInteger | Agda.TypeChecking.Serialise.Base |
| icodeMemo | Agda.TypeChecking.Serialise.Base |
| icodeN | Agda.TypeChecking.Serialise.Base |
| icodeN' | Agda.TypeChecking.Serialise.Base |
| icodeNode | Agda.TypeChecking.Serialise.Base |
| icodeString | Agda.TypeChecking.Serialise.Base |
| icodeX | Agda.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 |
| iDefaultPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| idempotent | Agda.Termination.Termination |
| Ident | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| identifier | Agda.Syntax.Parser.LexActions |
| IdentP | Agda.Syntax.Concrete |
| IdiomBrackets | Agda.Syntax.Concrete |
| IdiomType | Agda.Syntax.Internal |
| iDisplayForms | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| idP | Agda.Utils.Permutation |
| IdPart | Agda.Syntax.Common |
| IdS | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| idS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| idViewAsPath | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| iEnd | Agda.Syntax.Position |
| If | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 3 (Type/Class) | Agda.Utils.TypeLevel |
| ifBlocked | Agda.TypeChecking.Reduce |
| ifDirty | Agda.Utils.Update |
| iFilePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iFileType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ifIsSort | Agda.TypeChecking.Sort |
| ifJust | Agda.Utils.Maybe |
| ifJustM | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| ifLe | Agda.TypeChecking.SizedTypes.Syntax |
| ifM | Agda.Utils.Monad |
| ifNoConstraints | Agda.TypeChecking.Constraints |
| ifNoConstraints_ | Agda.TypeChecking.Constraints |
| ifNotM | Agda.Utils.Monad |
| ifNotNull | |
| 1 (Function) | Agda.Utils.Null |
| 2 (Function) | Agda.Utils.List1 |
| ifNotNullM | Agda.Utils.Null |
| ifNotPi | Agda.TypeChecking.Telescope |
| ifNotPiOrPathType | Agda.TypeChecking.Telescope |
| ifNotPiType | Agda.TypeChecking.Telescope |
| ifNotSort | Agda.TypeChecking.Sort |
| ifNull | |
| 1 (Function) | Agda.Utils.Null |
| 2 (Function) | Agda.Utils.List1 |
| ifNullM | Agda.Utils.Null |
| iForeignCode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ifPath | Agda.TypeChecking.Rules.Term |
| ifPi | Agda.TypeChecking.Telescope |
| ifPiType | Agda.TypeChecking.Telescope |
| ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ifTopLevelAndHighlightingLevelIsOr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iFullHash | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IgnoreAbstract | Agda.Interaction.Base |
| IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ignoreAbstractMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| IgnoreAll | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| ignoreBlocking | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
| IgnoreInAnnotations | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| IgnoreNot | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IgnoreSorts | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| iHighlighting | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ihname | Agda.Compiler.MAlonzo.Misc |
| iImportedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iImportWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ilam | Agda.TypeChecking.Names |
| iLength | Agda.Syntax.Position |
| IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IllegalPatternInTelescope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IllformedAsClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IllformedAsClause_ | Agda.Interaction.Options.Warnings |
| IllformedProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| illiterate | Agda.Syntax.Parser.Literate |
| IM | Agda.Interaction.Monad |
| IMax | Agda.Syntax.Internal |
| imax | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| IMin | Agda.Syntax.Internal |
| imin | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| imoduleMap | Agda.Syntax.Scope.Monad |
| iModuleName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ImpInsert | Agda.TypeChecking.Implicit |
| implicitArgs | Agda.TypeChecking.Implicit |
| ImplicitFlex | Agda.TypeChecking.Rules.LHS.Problem |
| ImplicitInsertion | Agda.TypeChecking.Implicit |
| implicitNamedArgs | Agda.TypeChecking.Implicit |
| implicitP | Agda.TypeChecking.Rules.LHS.Implicit |
| implies | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ImpMissingDefinitions | Agda.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 |
| importDirRange | Agda.Syntax.Common |
| ImportedModule | Agda.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 |
| importedNameMapFromList | Agda.Syntax.Scope.Monad |
| ImportedNS | Agda.Syntax.Scope.Base |
| importModule | Agda.Utils.Haskell.Syntax |
| importPrimitives | Agda.Syntax.Translation.ConcreteToAbstract |
| importQualified | Agda.Utils.Haskell.Syntax |
| imports | |
| 1 (Function) | Agda.Compiler.JS.Syntax |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| importsForPrim | Agda.Compiler.MAlonzo.Primitives |
| ImportSpec | Agda.Utils.Haskell.Syntax |
| importSpecs | Agda.Utils.Haskell.Syntax |
| Impossible | |
| 1 (Type/Class) | Agda.Utils.Impossible |
| 2 (Data Constructor) | Agda.Utils.Impossible |
| impossible | Agda.Utils.Impossible |
| ImpossibleConstructor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ImpossibleError | Agda.Interaction.ExitCode |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impossibleTest | Agda.ImpossibleTest |
| impossibleTestReduceM | Agda.ImpossibleTest |
| impRenaming | Agda.Syntax.Common |
| imp_dir | Agda.Syntax.Parser.Lexer |
| In | Agda.Syntax.Concrete.Operators.Parser |
| In1 | Agda.Utils.Three |
| In2 | Agda.Utils.Three |
| In3 | Agda.Utils.Three |
| inAbstractMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| inameMap | Agda.Syntax.Scope.Monad |
| inc | Agda.Utils.Warshall |
| InClause | Agda.TypeChecking.Positivity.Occurrence |
| includes | Agda.TypeChecking.Serialise.Base |
| Inclusion | |
| 1 (Type/Class) | Agda.Utils.PartialOrd |
| 2 (Data Constructor) | Agda.Utils.PartialOrd |
| inclusion | Agda.Utils.PartialOrd |
| incoming | Agda.TypeChecking.SizedTypes.WarshallSolver |
| inCompilerEnv | Agda.Compiler.Common |
| incompleteMatchWarnings | Agda.Interaction.Options.Warnings |
| IncompletePattern | Agda.Interaction.Highlighting.Precise |
| inConcreteMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| inConcreteOrAbstractMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| increase | Agda.Termination.Order |
| inCxt | Agda.TypeChecking.Names |
| IndArgType | Agda.TypeChecking.Positivity.Occurrence |
| InDefOf | Agda.TypeChecking.Positivity.Occurrence |
| Indent | Agda.Compiler.JS.Pretty |
| indent | |
| 1 (Function) | Agda.Utils.String |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| indentBy | Agda.Compiler.JS.Pretty |
| independent | Agda.Interaction.InteractionTop |
| Index | |
| 1 (Type/Class) | Agda.Utils.IndexedList |
| 2 (Data Constructor) | Agda.Utils.Suffix |
| indexWithDefault | Agda.Utils.List |
| Indirect | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Induction | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| Inductive | Agda.Syntax.Common |
| INeg | Agda.Syntax.Internal |
| Inf | Agda.Syntax.Internal |
| inf | Agda.TypeChecking.Positivity |
| InfectiveImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InfectiveImport_ | Agda.Interaction.Options.Warnings |
| infectiveOptions | Agda.Interaction.Options |
| infer | Agda.TypeChecking.CheckInternal |
| inferApplication | Agda.TypeChecking.Rules.Application |
| InferDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InferExpr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| inferExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
| inferExpr' | Agda.TypeChecking.Rules.Term |
| inferExprForWith | Agda.TypeChecking.Rules.Term |
| inferFunSort | Agda.TypeChecking.Sort |
| inferMeta | Agda.TypeChecking.Rules.Term |
| inferPiSort | Agda.TypeChecking.Sort |
| Inferred | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| inferredBlock | Agda.Syntax.Concrete.Definitions.Types |
| inferredChecks | Agda.Syntax.Concrete.Definitions.Types |
| inferredLeftovers | Agda.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 |
| infertypevar | Agda.Auto.CaseSplit |
| inferUnivSort | Agda.TypeChecking.Sort |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| infimum | Agda.Termination.Order |
| Infinite | Agda.Utils.Warshall |
| infinite | Agda.Utils.Warshall |
| Infinity | Agda.TypeChecking.SizedTypes.WarshallSolver |
| infinityFlexs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Infix | Agda.Syntax.Concrete |
| InfixApp | Agda.Utils.Haskell.Syntax |
| InfixDef | Agda.Syntax.Common |
| InfixNotation | Agda.Syntax.Notation |
| infodecl | Agda.Compiler.MAlonzo.Compiler |
| Info_AllGoalsWarnings | Agda.Interaction.Response |
| Info_Auto | Agda.Interaction.Response |
| Info_CompilationError | Agda.Interaction.Response |
| Info_CompilationOk | Agda.Interaction.Response |
| Info_Constraints | Agda.Interaction.Response |
| Info_Context | Agda.Interaction.Response |
| Info_Error | |
| 1 (Type/Class) | Agda.Interaction.Response |
| 2 (Data Constructor) | Agda.Interaction.Response |
| Info_GenericError | Agda.Interaction.Response |
| Info_GoalSpecific | Agda.Interaction.Response |
| Info_HighlightingParseError | Agda.Interaction.Response |
| Info_HighlightingScopeCheckError | Agda.Interaction.Response |
| Info_InferredType | Agda.Interaction.Response |
| Info_Intro_ConstructorUnknown | Agda.Interaction.Response |
| Info_Intro_NotFound | Agda.Interaction.Response |
| Info_ModuleContents | Agda.Interaction.Response |
| Info_NormalForm | Agda.Interaction.Response |
| Info_SearchAbout | Agda.Interaction.Response |
| Info_Time | Agda.Interaction.Response |
| Info_Version | Agda.Interaction.Response |
| Info_WhyInScope | Agda.Interaction.Response |
| inFreshModuleIfFreeParams | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| InfS | Agda.Syntax.Reflected |
| Infty | Agda.TypeChecking.SizedTypes.Syntax |
| init | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List2 |
| init1 | Agda.Utils.List |
| initAutoOptions | Agda.Auto.Options |
| initCCEnv | Agda.Compiler.MAlonzo.Compiler |
| initCommandState | Agda.Interaction.Base |
| initCopyInfo | Agda.Syntax.Abstract |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| initExpRefInfo | Agda.Auto.SearchControl |
| initFreeEnv | Agda.TypeChecking.Free.Lazy |
| initGraph | Agda.Utils.Warshall |
| initialiseCommandQueue | Agda.Interaction.InteractionTop |
| initLast | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.List1 |
| initLast1 | Agda.Utils.List |
| initLHSState | Agda.TypeChecking.Rules.LHS.ProblemRest |
| initMapS | Agda.Auto.Convert |
| initMaybe | Agda.Utils.List |
| initMeta | Agda.Auto.NarrowingSearch |
| initNiceEnv | Agda.Syntax.Concrete.Definitions.Monad |
| initOccursCheck | Agda.TypeChecking.MetaVars.Occurs |
| initPersistentState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| initPostScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| initPreScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| inits | Agda.Utils.List1 |
| initState | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| initWithDefault | Agda.Utils.List |
| InjectivePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Injectivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InlinePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| InlineReductions | Agda.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 |
| inMutualBlock | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual |
| inNameSpace | Agda.Syntax.Scope.Base |
| inOriginalContext | Agda.TypeChecking.Unquote |
| inplaceS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| inputFlag | Agda.Interaction.Options |
| InScope | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Scope.Base |
| inScopeBecause | Agda.Syntax.Scope.Base |
| InScopeSet | Agda.Syntax.Scope.Base |
| InScopeTag | Agda.Syntax.Scope.Base |
| inScopeTag | Agda.Syntax.Scope.Base |
| InSeq | |
| 1 (Type/Class) | Agda.Compiler.Treeless.Subst |
| 2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
| inSeq | Agda.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 |
| insertAfter | Agda.Compiler.JS.Compiler |
| insertCompared | Agda.Utils.Favorites |
| Inserted | Agda.Syntax.Common |
| insertEdge | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| insertEdgeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| insertHiddenLambdas | Agda.TypeChecking.Rules.Term |
| insertImplicit | Agda.TypeChecking.Implicit |
| insertImplicit' | Agda.TypeChecking.Implicit |
| insertImplicitBindersT | Agda.TypeChecking.Implicit |
| insertImplicitBindersT1 | Agda.TypeChecking.Implicit |
| insertImplicitPatSynArgs | Agda.Syntax.Abstract |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitPatternsT | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitSizeLtPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertInspects | Agda.TypeChecking.Rules.Def |
| insertLookupWithKey | Agda.Utils.BiMap |
| insertLookupWithKeyPrecondition | Agda.Utils.BiMap |
| insertMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| insertMetaVar | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| insertMissingFields | Agda.TypeChecking.Records |
| insertMissingFieldsFail | Agda.TypeChecking.Records |
| insertMissingFieldsWarn | Agda.TypeChecking.Records |
| insertMutualBlockInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual |
| insertNames | Agda.TypeChecking.Rules.Def |
| insertOldInteractionScope | Agda.Interaction.InteractionTop |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertPatternsLHSCore | Agda.TypeChecking.Rules.Def |
| insertPrecondition | Agda.Utils.BiMap |
| insertTrailingArgs | Agda.TypeChecking.Coverage |
| insertWith | |
| 1 (Function) | Agda.Utils.Trie |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| insideAndOutside | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| insideDotPattern | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| InsideOperandCtx | Agda.Syntax.Fixity |
| Instance | Agda.Syntax.Common |
| InstanceArg | Agda.Syntax.Concrete |
| InstanceArgV | Agda.Syntax.Concrete.Operators.Parser |
| InstanceArgWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceArgWithExplicitArg_ | Agda.Interaction.Options.Warnings |
| InstanceB | Agda.Syntax.Concrete |
| InstanceBlock | Agda.Syntax.Concrete.Definitions.Types |
| InstanceDef | Agda.Syntax.Common |
| InstanceNoCandidate | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceNoOutputTypeName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceNoOutputTypeName_ | Agda.Interaction.Options.Warnings |
| InstanceP | Agda.Syntax.Concrete |
| InstanceSearch | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InstanceSearchDepthExhausted | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceTable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InstanceWithExplicitArg_ | Agda.Interaction.Options.Warnings |
| Instantiable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Instantiate | Agda.TypeChecking.Reduce |
| instantiate | Agda.TypeChecking.Reduce |
| instantiate' | Agda.TypeChecking.Reduce |
| Instantiated | Agda.Interaction.Base |
| instantiateDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| instantiateDefinitionType | Agda.TypeChecking.Rules.Decl |
| InstantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull' | Agda.TypeChecking.Reduce |
| instantiateFullExceptForDefinitions | Agda.TypeChecking.Reduce |
| instantiateFullExceptForDefinitions' | Agda.TypeChecking.Reduce |
| instantiateRewriteRule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| instantiateRewriteRules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| instantiateTelescope | Agda.TypeChecking.Telescope |
| instantiateVarHeads | Agda.TypeChecking.Injectivity |
| inState | Agda.Syntax.Parser.LexActions |
| InstV | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Int | Agda.Utils.Haskell.Syntax |
| int | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| Integer | Agda.Compiler.JS.Syntax |
| integer | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Syntax.Parser.LexActions |
| integerC | Agda.TypeChecking.Serialise.Base |
| integerD | Agda.TypeChecking.Serialise.Base |
| integerE | Agda.TypeChecking.Serialise.Base |
| integerSemiring | Agda.Termination.Semiring |
| integerToChar | Agda.Utils.Char |
| Interaction | Agda.Interaction.Base |
| Interaction' | Agda.Interaction.Base |
| InteractionId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| interactionId | Agda.Syntax.Common |
| InteractionOutputCallback | Agda.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 |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Interactive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Interactor | Agda.Main |
| interAssocWith | Agda.Termination.SparseMatrix |
| interestingCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| interestingConstraint | Agda.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 |
| InterfaceFile | Agda.Interaction.FindFile |
| InterleavedData | Agda.Syntax.Concrete.Definitions.Types |
| interleavedDataCons | Agda.Syntax.Concrete.Definitions.Types |
| InterleavedDecl | Agda.Syntax.Concrete.Definitions.Types |
| interleavedDecl | Agda.Syntax.Concrete.Definitions.Types |
| interleavedDeclNum | Agda.Syntax.Concrete.Definitions.Types |
| interleavedDeclSig | Agda.Syntax.Concrete.Definitions.Types |
| InterleavedFun | Agda.Syntax.Concrete.Definitions.Types |
| interleavedFunClauses | Agda.Syntax.Concrete.Definitions.Types |
| InterleavedMutual | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types |
| interleaveRanges | Agda.Syntax.Position |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| internalError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| interpret | Agda.Interaction.InteractionTop |
| intersection | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.SmallSet |
| intersectVars | Agda.TypeChecking.Conversion |
| intersectWith | Agda.Termination.SparseMatrix |
| intersperse | Agda.Utils.List1 |
| Interval | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| interval | Agda.Syntax.Parser.Literate |
| Interval' | Agda.Syntax.Position |
| intervalInvariant | Agda.Syntax.Position |
| intervalsToRange | Agda.Syntax.Position |
| intervalToRange | Agda.Syntax.Position |
| intervalUnview | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| intervalUnview' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| IntervalView | Agda.Syntax.Internal |
| intervalView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| intervalView' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| IntervalWithoutFile | Agda.Syntax.Position |
| intFilePath | Agda.Interaction.FindFile |
| intMap | Agda.Utils.Warshall |
| inTopContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| Intro | Agda.Interaction.InteractionTop |
| intros | Agda.Compiler.MAlonzo.Compiler |
| introTactic | Agda.Interaction.BasicOps |
| intSemiring | Agda.Termination.Semiring |
| IntSet | Agda.Utils.IntSet.Infinite |
| intSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| intToDouble | Agda.Utils.Float |
| intView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidCatchallPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidCatchallPragma_ | Agda.Interaction.Options.Warnings |
| InvalidConstructor | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidConstructorBlock | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidConstructorBlock_ | Agda.Interaction.Options.Warnings |
| InvalidConstructor_ | Agda.Interaction.Options.Warnings |
| InvalidCoverageCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidCoverageCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidExtensionError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions.Errors |
| InvalidName | Agda.Syntax.Concrete.Definitions.Errors |
| InvalidNoPositivityCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidNoPositivityCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidNoUniverseCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidNoUniverseCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InvalidRecordDirective | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidRecordDirective_ | Agda.Interaction.Options.Warnings |
| InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidTerminationCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Invariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| invariant | |
| 1 (Function) | Agda.Utils.IntSet.Infinite |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| Inverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| inverseApplyCohesion | Agda.Syntax.Common |
| inverseApplyModalityButNotQuantity | Agda.Syntax.Common |
| inverseApplyQuantity | Agda.Syntax.Common |
| inverseApplyRelevance | Agda.Syntax.Common |
| inverseCompose | Agda.Utils.POMonoid |
| inverseComposeCohesion | Agda.Syntax.Common |
| inverseComposeModality | Agda.Syntax.Common |
| inverseComposeQuantity | Agda.Syntax.Common |
| inverseComposeRelevance | Agda.Syntax.Common |
| InversePermute | Agda.Utils.Permutation |
| inversePermute | Agda.Utils.Permutation |
| InverseScopeLookup | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| inverseScopeLookupModule | Agda.Syntax.Scope.Base |
| inverseScopeLookupModule' | Agda.Syntax.Scope.Base |
| inverseScopeLookupName | Agda.Syntax.Scope.Base |
| inverseScopeLookupName' | Agda.Syntax.Scope.Base |
| inverseScopeLookupName'' | Agda.Syntax.Scope.Base |
| inverseSubst | Agda.TypeChecking.MetaVars |
| InversionDepthReached | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| InversionDepthReached_ | Agda.Interaction.Options.Warnings |
| InversionMap | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Invert | Agda.Syntax.Common |
| InvertExcept | Agda.TypeChecking.MetaVars |
| invertFunction | Agda.TypeChecking.Injectivity |
| invertP | Agda.Utils.Permutation |
| invLookup | Agda.Utils.BiMap |
| InvView | Agda.TypeChecking.Injectivity |
| io | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| IOException | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IOne | Agda.Syntax.Internal |
| iOptionsUsed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IORef | Agda.Utils.IORef |
| iotapossmeta | Agda.Auto.Typecheck |
| iotastep | Agda.Auto.Typecheck |
| IOTCM | |
| 1 (Data Constructor) | Agda.Interaction.Base |
| 2 (Type/Class) | Agda.Interaction.Base |
| IOTCM' | Agda.Interaction.Base |
| iPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iPatternSyns | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipbEquations | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipbMetaApp | Agda.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 |
| ipbOverapplied | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipbValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcBoundary | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcClauseNo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcClosure | Agda.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 |
| ipClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcQName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipcWithSub | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipMeta | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IPNoClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ipSolved | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Irrelevant | Agda.Syntax.Common |
| irrToNonStrict | Agda.Syntax.Common |
| IsAbstract | Agda.Syntax.Common |
| isAbsurdBody | Agda.Syntax.Internal |
| isAbsurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isAbsurdP | Agda.Syntax.Concrete |
| isAbsurdPatternName | Agda.Syntax.Internal |
| isAHole | Agda.Syntax.Notation |
| isAlias | Agda.TypeChecking.Rules.Def |
| isAmbiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isAnonymousModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| IsApply | Agda.TypeChecking.Coverage.Match |
| isApplyElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| isApplyElim' | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| IsBase | Agda.Utils.TypeLevel |
| IsBasicRangeMap | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| isBelow | Agda.Utils.Warshall |
| isBenchmarkOn | Agda.Utils.Benchmark |
| isBinderP | Agda.Syntax.Concrete |
| isBinderUsed | Agda.TypeChecking.Free |
| isBindingHole | Agda.Syntax.Notation |
| isBlocked | Agda.TypeChecking.Reduce |
| isBlockedTerm | Agda.TypeChecking.MetaVars |
| isBounded | Agda.TypeChecking.SizedTypes |
| isBoundedProjVar | Agda.TypeChecking.SizedTypes |
| isBoundedSizeType | Agda.TypeChecking.SizedTypes |
| isBuiltin | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| isBuiltinModule | Agda.Interaction.Options.Lenses |
| isBuiltinModuleWithSafePostulates | Agda.Interaction.Options.Lenses |
| isBuiltinNoDef | Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| isCanonical | Agda.TypeChecking.Conversion |
| isClosed | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open |
| isCode | Agda.Syntax.Parser.Literate |
| isCodeLayer | Agda.Syntax.Parser.Literate |
| isCoFibrantSort | Agda.TypeChecking.Irrelevance |
| isCoinductive | Agda.TypeChecking.Rules.Data |
| isCoinductiveProjection | Agda.Termination.Monad |
| isCon | Agda.TypeChecking.Unquote |
| isConName | Agda.Syntax.Scope.Base |
| isCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isCovered | Agda.TypeChecking.Coverage |
| IsData | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS |
| IsDataModule | Agda.Syntax.Scope.Base |
| isDataOrRecord | Agda.TypeChecking.Datatypes |
| isDataOrRecordType | Agda.TypeChecking.Datatypes |
| isDatatype | Agda.TypeChecking.Datatypes |
| isDatatypeModule | Agda.Syntax.Scope.Monad |
| isDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isDecr | Agda.Termination.Order |
| isDef | Agda.TypeChecking.Unquote |
| isDefAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| isDefaultImportDir | Agda.Syntax.Common |
| isDefName | Agda.Syntax.Scope.Base |
| IsDominated | Agda.Utils.Favorites |
| isDontExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IsEllipsis | Agda.Syntax.Concrete.Pattern |
| isEllipsis | Agda.Syntax.Concrete.Pattern |
| IsEmpty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isEmpty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Termination.SparseMatrix |
| isEmptyFunction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isEmptyObject | Agda.Compiler.JS.Compiler |
| isEmptyTel | Agda.TypeChecking.Empty |
| IsEmptyType | Agda.Interaction.Base |
| isEmptyType | Agda.TypeChecking.Empty |
| isEnabled | Agda.Compiler.Backend |
| isEqualityType | Agda.Syntax.Internal |
| isErasable | Agda.Compiler.Treeless.Erase |
| isErased | Agda.Syntax.Common |
| isEtaCon | Agda.TypeChecking.Records |
| isEtaExpandable | Agda.TypeChecking.MetaVars |
| isEtaOrCoinductiveRecordConstructor | Agda.TypeChecking.Records |
| isEtaRecord | Agda.TypeChecking.Records |
| isEtaRecordType | Agda.TypeChecking.Records |
| isEtaVar | Agda.TypeChecking.Records |
| IsExpr | Agda.Syntax.Concrete.Operators.Parser |
| isExtendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IsFam | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| IsFibrant | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| isFibrant | Agda.TypeChecking.Irrelevance |
| isFlexible | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| IsFlexiblePattern | Agda.TypeChecking.Rules.LHS |
| isFlexiblePattern | Agda.TypeChecking.Rules.LHS |
| isFlexNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| IsForced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isForced | Agda.TypeChecking.Forcing |
| IsFree | Agda.TypeChecking.Free.Reduce |
| isFrozen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isFullyInstantiatedMeta | Agda.TypeChecking.Reduce |
| isFunName | Agda.Syntax.Concrete.Definitions.Types |
| isGeneralizableMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isGeneratedRecordConstructor | Agda.TypeChecking.Records |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsIApply | Agda.TypeChecking.Coverage.Match |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isImported | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| IsIndex | Agda.TypeChecking.Positivity.Occurrence |
| isInductiveRecord | Agda.TypeChecking.Records |
| IsInfix | Agda.Syntax.Common |
| isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isInftyNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| isInlineFun | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isInsertedHidden | Agda.Syntax.Common |
| isInsideDotPattern | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| IsInstance | Agda.Syntax.Common |
| isInstance | Agda.Syntax.Common |
| isInstanceConstraint | Agda.TypeChecking.InstanceArguments |
| IsInstantiatedMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isInstantiatedMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isInstantiatedMeta' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isInteractionMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isInterleavedData | Agda.Syntax.Concrete.Definitions.Types |
| isInterleavedFun | Agda.Syntax.Concrete.Definitions.Types |
| isInternalAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| isInterval | Agda.TypeChecking.Telescope.Path |
| isIOne | Agda.Syntax.Internal |
| isIrrelevant | Agda.Syntax.Common |
| isIrrelevantOrPropM | Agda.TypeChecking.Irrelevance |
| isJust | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| isLabeled | Agda.Syntax.Concrete.Pretty |
| isLambdaHole | Agda.Syntax.Notation |
| isLeChildModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isLeft | Agda.Utils.Either |
| isLeParentModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isLevelType | Agda.TypeChecking.Level |
| IsLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isLocal | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| IsLock | Agda.Syntax.Common |
| isLtChildModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isLtParentModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| IsMacro | Agda.Syntax.Common |
| isMacro | Agda.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 |
| IsMeta | Agda.TypeChecking.Reduce |
| isMeta | Agda.TypeChecking.Reduce |
| isMetaTCWarning | Agda.TypeChecking.Warnings |
| isMetaWarning | Agda.TypeChecking.Warnings |
| isModChar | Agda.Compiler.MAlonzo.Misc |
| isModuleAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| isModuleFreeVar | Agda.TypeChecking.Rules.Term |
| isName | Agda.Interaction.BasicOps |
| isNameInScope | Agda.Syntax.Scope.Base |
| isNameInScopeUnqualified | Agda.Syntax.Scope.Base |
| isNegInf | Agda.Utils.Float |
| isNegZero | Agda.Utils.Float |
| isNeutral | Agda.TypeChecking.MetaVars.Occurs |
| isNewerThan | Agda.Utils.FileName |
| IsNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Concrete, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNonStrict | Agda.Syntax.Common |
| isNormalHole | Agda.Syntax.Notation |
| IsNot | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical |
| isNothing | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| IsNotLock | Agda.Syntax.Common |
| isolatedNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| isOpenMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isOpenMixfix | Agda.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 |
| isOrder | Agda.Termination.Order |
| iSource | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| iSourceHash | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isOverlappable | Agda.Syntax.Common |
| isPath | Agda.TypeChecking.Telescope |
| IsPathCons | Agda.TypeChecking.Rules.Data |
| isPathType | Agda.Syntax.Internal |
| IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isPattern | Agda.Syntax.Concrete |
| isPosInf | Agda.Utils.Float |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isPosZero | Agda.Utils.Float |
| isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsPrefixOf | Agda.TypeChecking.Abstract |
| isPrefixOf | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.TypeChecking.Abstract |
| isPrimEq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| isPrimitive | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| isPrimitiveModule | Agda.Interaction.Options.Lenses |
| isProblemSolved | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| isProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| isProjectionButNotCoinductive | Agda.Termination.Monad |
| isProjection_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| IsProjElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| isProjElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| IsProjP | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isProjP | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isPropEnabled | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isProperProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| isPropM | Agda.TypeChecking.Irrelevance |
| isQName | Agda.Interaction.BasicOps |
| isQualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isQuantityAttribute | Agda.Syntax.Concrete.Attribute |
| isReconstructed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IsRecord | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS |
| isRecord | Agda.TypeChecking.Records |
| isRecordConstructor | Agda.TypeChecking.Records |
| isRecordDirective | Agda.Syntax.Concrete |
| IsRecordModule | Agda.Syntax.Scope.Base |
| isRecordType | Agda.TypeChecking.Records |
| isRecursiveRecord | Agda.TypeChecking.Records |
| IsReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isRelevanceAttribute | Agda.Syntax.Concrete.Attribute |
| isRelevant | Agda.Syntax.Common |
| isRelevantProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| isRelevantProjection_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| isRight | Agda.Utils.Either |
| isSafeInteger | Agda.Utils.Float |
| isSingleIdentifierP | Agda.Syntax.Concrete |
| isSingleton | Agda.Termination.SparseMatrix |
| isSingletonRecord | Agda.TypeChecking.Records |
| isSingletonRecord' | Agda.TypeChecking.Records |
| isSingletonRecordModuloRelevance | Agda.TypeChecking.Records |
| isSingletonType | Agda.TypeChecking.Records |
| isSingletonType' | Agda.TypeChecking.Records |
| isSingletonTypeModuloRelevance | Agda.TypeChecking.Records |
| isSizeConstraint | Agda.TypeChecking.SizedTypes |
| isSizeConstraint_ | Agda.TypeChecking.SizedTypes |
| isSizeNameTest | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| isSizeNameTestRaw | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| isSizeProblem | Agda.TypeChecking.SizedTypes |
| IsSizeType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| isSizeType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| isSizeTypeTest | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| isSmallSort | Agda.TypeChecking.Substitute |
| isSolvingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| IsSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isSort | Agda.Syntax.Internal |
| isSortMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isSortMeta_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| isStaticFun | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| IsStrict | Agda.Syntax.Internal |
| isStronglyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| isSublistOf | Agda.Utils.List |
| isSubscriptDigit | Agda.Utils.Suffix |
| isSubsetOf | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.SmallSet |
| isSurrogateCodePoint | Agda.Utils.Char |
| isTacticAttribute | Agda.Syntax.Concrete.Attribute |
| iStart | Agda.Syntax.Position |
| isTimeless | Agda.TypeChecking.Lock |
| isTop | Agda.TypeChecking.SizedTypes.Utils |
| isTopLevelValue | Agda.Compiler.JS.Compiler |
| isTrivialPattern | Agda.TypeChecking.Coverage.Match |
| isTwoLevelEnabled | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isType | Agda.TypeChecking.Rules.Term |
| isType' | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isTypeEqualTo | Agda.TypeChecking.Rules.Term |
| IsType_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| isType_ | Agda.TypeChecking.Rules.Term |
| isUnderscore | Agda.Syntax.Common |
| isUnguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| isUnnamed | Agda.Syntax.Common |
| isUnqualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| isUnsolvedWarning | Agda.TypeChecking.Warnings |
| isUntypedBuiltin | Agda.TypeChecking.Rules.Builtin |
| isValidJSIdent | Agda.Compiler.JS.Pretty |
| isVar | Agda.TypeChecking.CompiledClause.Compile |
| IsVarSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| isWeaklyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| IsWithP | Agda.Syntax.Concrete.Pattern |
| isWithP | Agda.Syntax.Concrete.Pattern |
| isWithPattern | Agda.Syntax.Concrete.Pattern |
| isZeroNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Item | Agda.TypeChecking.Positivity |
| iterate | Agda.Utils.List1 |
| iterate' | Agda.Utils.Function |
| iterateSolver | Agda.TypeChecking.SizedTypes.WarshallSolver |
| iterateUntil | Agda.Utils.Function |
| iterateUntilM | Agda.Utils.Function |
| iterWhile | Agda.Utils.Function |
| iUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| IVar | Agda.Utils.Haskell.Syntax |
| iWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| Ix | Agda.Utils.SmallSet |
| IZero | Agda.Syntax.Internal |