| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| icnvh | Agda.Auto.Convert |
| Id | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| Ident | Agda.Syntax.Concrete |
| identifier | Agda.Syntax.Parser.LexActions |
| identity | Agda.Utils.TestHelpers |
| IdentP | Agda.Syntax.Concrete |
| idP | Agda.Utils.Permutation |
| idSub | Agda.TypeChecking.Substitute |
| iEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| ifM | Agda.Utils.Monad |
| IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| ignoreBlocking | Agda.Syntax.Internal |
| ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ihname | Agda.Compiler.MAlonzo.Misc |
| iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IM | Agda.Interaction.Monad |
| iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ImpInsert | Agda.TypeChecking.Implicit |
| impInsert | Agda.TypeChecking.Implicit |
| ImplicitInsertion | Agda.TypeChecking.Implicit |
| ImplicitP | Agda.Syntax.Abstract |
| Import | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| ImportDirective | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importDirRange | Agda.Syntax.Concrete |
| ImportedModule | Agda.Syntax.Concrete |
| ImportedName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importedName | Agda.Syntax.Concrete |
| importedNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ImportedNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ImportPragma | Agda.Syntax.Concrete |
| imports | Agda.Compiler.MAlonzo.Compiler |
| importsForPrim | Agda.Compiler.MAlonzo.Primitives |
| Impossible | |
| 1 (Type/Class) | Agda.Utils.Impossible |
| 2 (Data Constructor) | Agda.Utils.Impossible |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impRTP | Agda.Compiler.Alonzo.Haskell |
| impRTS | Agda.Compiler.Alonzo.Haskell |
| imp_dir | Agda.Syntax.Parser.Lexer |
| inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inc | Agda.Utils.Warshall |
| InClause | Agda.TypeChecking.Positivity |
| IncompletePattern | Agda.Interaction.Highlighting.Precise |
| IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| incPcnt | Agda.Compiler.Alonzo.PatternMonad |
| InDefOf | Agda.TypeChecking.Positivity |
| indent | Agda.Utils.String |
| Index | |
| 1 (Data Constructor) | Agda.Utils.Suffix |
| 2 (Type/Class) | Agda.Termination.CallGraph |
| Induction | Agda.Syntax.Common |
| Inductive | Agda.Syntax.Common |
| inductiveCheck | Agda.TypeChecking.Rules.Builtin |
| Inf | Agda.Syntax.Internal |
| InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferDef | Agda.TypeChecking.Rules.Term |
| InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
| inferHead | Agda.TypeChecking.Rules.Term |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Infinite | Agda.Utils.Warshall |
| infinite | Agda.Utils.Warshall |
| Infix | Agda.Syntax.Concrete |
| InfixDef | Agda.Syntax.Common |
| infixlP | Agda.Syntax.Concrete.Operators.Parser |
| infixP | Agda.Syntax.Concrete.Operators.Parser |
| infixrP | Agda.Syntax.Concrete.Operators.Parser |
| Info | Agda.Syntax.Info |
| infoDecl | Agda.Compiler.Alonzo.Main |
| infodecl | Agda.Compiler.MAlonzo.Compiler |
| infoOnException | Agda.Interaction.GhciTop |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| initGraph | Agda.Utils.Warshall |
| initMapS | Agda.Auto.Convert |
| initPState | Agda.Compiler.Alonzo.PatternMonad |
| initState | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 3 (Function) | Agda.Interaction.GhciTop |
| inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| inNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| InScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| InScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| insert | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Termination.CallGraph |
| insertImplicit | Agda.TypeChecking.Implicit |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertWithKeyM | Agda.Utils.Map |
| InsideOperandCtx | Agda.Syntax.Fixity |
| insideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| Instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| Instantiated | Agda.Interaction.BasicOps |
| instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| InstantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiatePattern | Agda.TypeChecking.Rules.LHS |
| instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate |
| inState | Agda.Syntax.Parser.LexActions |
| InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| int | Agda.Utils.Pretty |
| integer | Agda.Utils.Pretty |
| integerSemiring | Agda.Termination.Semiring |
| Interaction | |
| 1 (Type/Class) | Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Interaction.GhciTop |
| interaction | Agda.Interaction.CommandLine.CommandLine |
| InteractionId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| interactionLoop | Agda.Interaction.CommandLine.CommandLine |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Interface | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Interval | |
| 1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| intervalInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| intMap | Agda.Utils.Warshall |
| introTactic | Agda.Interaction.BasicOps |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inverseScopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inverseScopeLookupModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inverseScopeLookupName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| invertP | Agda.Utils.Permutation |
| InvView | Agda.TypeChecking.Injectivity |
| io | Agda.TypeChecking.Primitive |
| IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iotastep | Agda.Auto.Typecheck |
| ioTCM | Agda.Interaction.GhciTop |
| ioTCM_ | Agda.Interaction.GhciTop |
| IsAbstract | Agda.Syntax.Common |
| isBelow | Agda.Utils.Warshall |
| isBlockedTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| isCoinductive | Agda.TypeChecking.Rules.Data |
| iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isDatatype | Agda.TypeChecking.Coverage |
| IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isEmpty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Termination.Matrix |
| IsEmptyType | Agda.Interaction.BasicOps |
| isEmptyType | Agda.TypeChecking.Empty |
| isEmptyTypeC | Agda.TypeChecking.Empty |
| IsExpr | Agda.Syntax.Concrete.Operators.Parser |
| isHaskellKind | Agda.Compiler.HaskellTypes |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isIndependent | Agda.Interaction.GhciTop |
| IsInfix | Agda.Syntax.Common |
| isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isJust | Agda.Utils.Maybe |
| isLeft | Agda.Utils.Either |
| isLiterate | Agda.Interaction.Options |
| isMain | Agda.Compiler.Alonzo.Main |
| isNewerThan | Agda.Interaction.Imports |
| isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNothing | Agda.Utils.Maybe |
| isntTypeConf | Agda.TypeChecking.Test.Generators |
| isOperator | |
| 1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isRecord | Agda.TypeChecking.Records |
| isRight | Agda.Utils.Either |
| isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSolvedProblem | Agda.TypeChecking.Rules.LHS |
| IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isString | Agda.Utils.Generics |
| isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isSuccess | Agda.Utils.QuickCheck |
| iStart | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| isType | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isTypeConf | Agda.TypeChecking.Test.Generators |
| IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isType_ | Agda.TypeChecking.Rules.Term |
| isUnicodeId | Agda.Utils.Unicode |
| isVar | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isWellScoped | Agda.TypeChecking.Test.Generators |
| isZero | Agda.Utils.TestHelpers |
| Item | Agda.TypeChecking.Positivity |
| iterate' | Agda.Utils.Function |