Index - I
| IApply | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| IApplyP | Agda.Syntax.Internal |
| IApplyVars | Agda.TypeChecking.Telescope.Path |
| iApplyVars | Agda.TypeChecking.Telescope.Path |
| IArray | Agda.Utils.IArray |
| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| icodeList | Agda.TypeChecking.Serialise.Instances.General |
| icodeListPair | Agda.TypeChecking.Serialise.Instances.General |
| icodeLText | Agda.TypeChecking.Serialise.Base |
| icodeMemo | Agda.TypeChecking.Serialise.Base |
| icodeN | Agda.TypeChecking.Serialise.Base |
| icodeN' | Agda.TypeChecking.Serialise.Base |
| icodeNode | Agda.TypeChecking.Serialise.Base |
| icodeSText | Agda.TypeChecking.Serialise.Base |
| icodeString | Agda.TypeChecking.Serialise.Base |
| icodeVarSet | Agda.TypeChecking.Serialise.Base |
| icodRM | Agda.TypeChecking.Serialise.Instances.Highlighting |
| icod_ | Agda.TypeChecking.Serialise.Base |
| ICOption | Agda.Interaction.Options |
| icOptionActive | Agda.Interaction.Options |
| icOptionDescription | Agda.Interaction.Options |
| icOptionKind | Agda.Interaction.Options |
| icOptionOK | Agda.Interaction.Options |
| icOptionWarning | Agda.Interaction.Options |
| Id | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| iDefaultPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| idFromFile | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IdiomBracketError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IdiomBracketError_ | Agda.Interaction.Options.Errors |
| IdiomBrackets | Agda.Syntax.Concrete |
| IdiomType | Agda.Syntax.Internal |
| iDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| idP | Agda.Utils.Permutation |
| IdPart | Agda.Syntax.Common |
| IdS | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| idS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| IdToFile | Agda.Utils.FileId |
| idToFile | Agda.Utils.FileId |
| iEnd | Agda.Syntax.Position |
| iEnd' | Agda.Syntax.Position |
| If | |
| 1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| 2 (Type/Class) | Agda.Utils.TypeLevel |
| 3 (Data Constructor) | Agda.Compiler.JS.Syntax |
| ifBlocked | Agda.TypeChecking.Reduce |
| ifDirty | Agda.Utils.Update |
| iFilePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iFileType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| ifNotPathB | Agda.TypeChecking.Telescope |
| ifNotPi | Agda.TypeChecking.Telescope |
| ifNotPiOrPathB | Agda.TypeChecking.Telescope |
| ifNotPiOrPathType | Agda.TypeChecking.Telescope |
| ifNotPiType | Agda.TypeChecking.Telescope |
| ifNotSort | Agda.TypeChecking.Sort |
| ifNull | |
| 1 (Function) | Agda.Utils.Map1 |
| 2 (Function) | Agda.Utils.Set1 |
| 3 (Function) | Agda.Utils.Null |
| 4 (Function) | Agda.Utils.List1 |
| ifNullM | Agda.Utils.Null |
| iForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ifPath | Agda.TypeChecking.Telescope |
| ifPathB | Agda.TypeChecking.Telescope |
| ifPi | Agda.TypeChecking.Telescope |
| ifPiB | Agda.TypeChecking.Telescope |
| ifPiOrPathB | Agda.TypeChecking.Telescope |
| ifPiType | Agda.TypeChecking.Telescope |
| ifPiTypeB | Agda.TypeChecking.Telescope |
| ifThenElse | Agda.Utils.Boolean |
| ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ifTopLevelAndHighlightingLevelIsOr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iFullHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IgnoreAbstract | Agda.Interaction.Base |
| IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| IgnoreSorts | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| IgnoreUnused | Agda.Compiler.ToTreeless |
| iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ihname | Agda.Compiler.MAlonzo.Misc |
| iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iImportWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IInfo | Agda.TypeChecking.Coverage.SplitClause |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ilam | Agda.TypeChecking.Names |
| iLength | Agda.Syntax.Position |
| Illegal | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
| IllegalAmbiguity | Agda.Syntax.Scope.Base |
| IllegalDeclarationBeforeTopLevelModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalDeclarationBeforeTopLevelModule_ | Agda.Interaction.Options.Errors |
| IllegalDeclarationInDataDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalDeclarationInDataDefinition_ | Agda.Interaction.Options.Errors |
| IllegalHidingInPostfixProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalHidingInPostfixProjection_ | Agda.Interaction.Options.Errors |
| IllegalInstanceVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalInstanceVariableInPatternSynonym_ | Agda.Interaction.Options.Errors |
| IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalLetInTelescope_ | Agda.Interaction.Options.Errors |
| IllegalPatternInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalPatternInTelescope_ | Agda.Interaction.Options.Errors |
| IllegalRewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalRewriteRuleReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| illegalRewriteWarningName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllformedAsClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllformedAsClause_ | Agda.Interaction.Options.Warnings |
| IllformedProjectionPatternAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllformedProjectionPatternAbstract_ | Agda.Interaction.Options.Errors |
| IllformedProjectionPatternConcrete | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllformedProjectionPatternConcrete_ | Agda.Interaction.Options.Errors |
| illiterate | Agda.Syntax.Parser.Literate |
| IllTypedPatternAfterWithAbstraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllTypedPatternAfterWithAbstraction_ | Agda.Interaction.Options.Errors |
| IM | Agda.Interaction.Monad |
| IMax | Agda.Syntax.Internal |
| imax | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| iMetaBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IMin | Agda.Syntax.Internal |
| imin | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| imoduleMap | Agda.Syntax.Scope.Monad |
| iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ImpInsert | Agda.TypeChecking.Implicit |
| implicitArgs | Agda.TypeChecking.Implicit |
| implicitCheckedArgs | Agda.TypeChecking.Implicit |
| ImplicitFlex | Agda.TypeChecking.Rules.LHS.Problem |
| ImplicitInsertion | Agda.TypeChecking.Implicit |
| implicitNamedArgs | Agda.TypeChecking.Implicit |
| implicitP | Agda.TypeChecking.Rules.LHS.Implicit |
| ImpliedPragmaOption | Agda.Interaction.Options |
| impliedPragmaOptions | Agda.Interaction.Options |
| implies | |
| 1 (Function) | Agda.Utils.Boolean |
| 2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| ImpliesPragmaOption | Agda.Interaction.Options |
| 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 |
| ImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| ImportMayOpen | Agda.Syntax.Concrete.Definitions.Errors |
| importModule | Agda.Utils.Haskell.Syntax |
| importPrimitiveModules | Agda.Interaction.Imports |
| importPrimitives | Agda.Syntax.Translation.ConcreteToAbstract |
| importQualified | Agda.Utils.Haskell.Syntax |
| ImportS | Agda.Syntax.Abstract |
| imports | Agda.Compiler.JS.Syntax |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| impossibleConstructorErrorName | Agda.TypeChecking.Errors.Names |
| ImpossibleConstructor_ | Agda.Interaction.Options.Errors |
| ImpossibleError | Agda.Interaction.ExitCode |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impossibleTest | Agda.ImpossibleTest |
| impossibleTestReduceM | Agda.ImpossibleTest |
| impRenaming | Agda.Syntax.Common |
| ImproperInstHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ImproperInstTele | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inameMap | Agda.Syntax.Scope.Monad |
| incCompGen | Agda.Mimer.Types |
| incCompHit | Agda.Mimer.Types |
| incCompNoRegen | Agda.Mimer.Types |
| incCompRegen | Agda.Mimer.Types |
| 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 |
| incMetasCreated | Agda.Mimer.Types |
| Incoherent | Agda.Syntax.Common |
| incoming | Agda.TypeChecking.SizedTypes.WarshallSolver |
| inCompilerEnv | Agda.Compiler.Common |
| incompleteMatchWarnings | Agda.Interaction.Options.Warnings |
| IncompletePattern | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inConcreteOrAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IncorrectTypeForRewriteRelation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IncorrectTypeForRewriteRelationReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IncorrectTypeForRewriteRelation_ | Agda.Interaction.Options.Errors |
| increase | Agda.Termination.Order |
| incRefineFail | Agda.Mimer.Types |
| incRefineSuccess | Agda.Mimer.Types |
| incTypeEqChecks | Agda.Mimer.Types |
| 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 |
| index | |
| 1 (Function) | Agda.Utils.IArray |
| 2 (Function) | Agda.Utils.MinimalArray.Prim |
| 3 (Function) | Agda.Utils.MinimalArray.Lifted |
| IndexedClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IndexedClauseArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| indexWithDefault | Agda.Utils.List |
| indices | Agda.Utils.IArray |
| Indirect | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Induction | |
| 1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| InductionAndEta | |
| 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 |
| Inductive | Agda.Syntax.Common.Aspect, Agda.Syntax.Common |
| INeg | Agda.Syntax.Internal |
| ineg | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| Inf | Agda.Syntax.Internal |
| inf | Agda.TypeChecking.Positivity |
| infallibleSortKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Infective | Agda.Interaction.Options |
| InfectiveCoinfective | Agda.Interaction.Options |
| InfectiveCoinfectiveOption | Agda.Interaction.Options |
| infectiveCoinfectiveOptions | Agda.Interaction.Options |
| InfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InfectiveImport_ | Agda.Interaction.Options.Warnings |
| infer | Agda.TypeChecking.CheckInternal |
| inferApplication | Agda.TypeChecking.Rules.Application |
| InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inferExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
| inferExpr' | Agda.TypeChecking.Rules.Term |
| inferExprForWith | Agda.TypeChecking.Rules.Term |
| inferFunSort | Agda.TypeChecking.Sort |
| inferInternal | Agda.TypeChecking.CheckInternal |
| inferInternal' | Agda.TypeChecking.CheckInternal |
| inferMeta | Agda.TypeChecking.Rules.Term |
| inferNeutral | Agda.TypeChecking.ProjectionLike |
| inferPiSort | Agda.TypeChecking.Sort |
| Inferred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| inferUnivSort | Agda.TypeChecking.Sort |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| infimum | Agda.Termination.Order |
| 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 |
| infoEqLHS | Agda.TypeChecking.Coverage.SplitClause |
| infoEqRHS | Agda.TypeChecking.Coverage.SplitClause |
| infoEqTel | Agda.TypeChecking.Coverage.SplitClause |
| infoLeftInv | Agda.TypeChecking.Coverage.SplitClause |
| infoRho | Agda.TypeChecking.Coverage.SplitClause |
| inform | Agda.Setup.EmacsMode |
| infoTau | Agda.TypeChecking.Coverage.SplitClause |
| infoTel | Agda.TypeChecking.Coverage.SplitClause |
| infoTel0 | Agda.TypeChecking.Coverage.SplitClause |
| Info_AllGoalsWarnings | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Auto | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_CompilationError | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_CompilationOk | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Constraints | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Context | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Error | |
| 1 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| 2 (Type/Class) | Agda.Interaction.Response |
| Info_Error_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_GenericError | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_GoalSpecific | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_HighlightingParseError | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_HighlightingScopeCheckError | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_InferredType | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Intro_ConstructorUnknown | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Intro_NotFound | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_ModuleContents | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_NormalForm | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_SearchAbout | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Time | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_Version | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| Info_WhyInScope | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| inFreshModuleIfFreeParams | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InfS | Agda.Syntax.Reflected |
| Infty | Agda.TypeChecking.SizedTypes.Syntax |
| inGoalEnv | Agda.Mimer.Monad |
| INice | Agda.Syntax.Concrete.Definitions.Monad |
| init | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.List2 |
| init1 | Agda.Utils.List |
| initCommandState | Agda.Interaction.Base |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initFileDict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initFreeEnv | Agda.TypeChecking.Free.Lazy |
| InitialCandidates | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| initialiseCommandQueue | Agda.Interaction.InteractionTop |
| initialMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initLast | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.List1 |
| initLast1 | Agda.Utils.List |
| initLHSState | Agda.TypeChecking.Rules.LHS.ProblemRest |
| initMaybe | Agda.Utils.List |
| initNiceState | Agda.Syntax.Concrete.Definitions.Monad |
| initOccursCheck | Agda.TypeChecking.MetaVars.Occurs |
| initPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initPersistentStateFromSessionState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inits | Agda.Utils.List1 |
| inits1 | Agda.Utils.List1 |
| initSessionState | Agda.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 |
| initStateFromPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initStateFromSessionState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initStateIO | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initUnifyState | Agda.TypeChecking.Rules.LHS.Unify.Types |
| initWithDefault | Agda.Utils.List |
| injectAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
| injectConstructor | Agda.TypeChecking.Rules.LHS.Unify.Types |
| injectDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types |
| injectIndices | Agda.TypeChecking.Rules.LHS.Unify.Types |
| InjectiveForInferencePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| InjectivePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Injectivity | |
| 1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
| injectParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
| injectType | Agda.TypeChecking.Rules.LHS.Unify.Types |
| InlineNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InlineNoExactSplit_ | Agda.Interaction.Options.Warnings |
| InlinePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| InlineReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InMutual | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
| inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inNameSpace | Agda.Syntax.Scope.Base |
| inOriginalContext | Agda.TypeChecking.Unquote |
| inplaceS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| inputFlag | Agda.Interaction.Options |
| inRange | |
| 1 (Function) | Agda.Utils.IArray |
| 2 (Function) | Agda.Utils.VarSet |
| 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.Set1 |
| 3 (Function) | Agda.Utils.Map1 |
| 4 (Function) | Agda.Utils.Bag |
| 5 (Function) | Agda.Utils.BoolSet |
| 6 (Function) | Agda.Utils.AssocList |
| 7 (Function) | Agda.Utils.VarSet |
| 8 (Function) | Agda.Utils.SmallSet |
| 9 (Function) | Agda.Utils.Trie |
| 10 (Function) | Agda.Utils.RangeMap |
| 11 (Function) | Agda.Utils.HashTable |
| 12 (Function) | Agda.Utils.Favorites |
| 13 (Function) | Agda.Utils.BiMap |
| 14 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 15 (Function) | Agda.Termination.CallMatrix |
| 16 (Function) | Agda.Termination.CallGraph |
| insertAfter | Agda.Compiler.JS.Compiler |
| insertCompared | Agda.Utils.Favorites |
| insertDT | Agda.TypeChecking.DiscrimTree |
| Inserted | Agda.Syntax.Common |
| insertedBinder | Agda.Syntax.Abstract |
| InsertedBinderName | Agda.Syntax.Common |
| insertedBinder_ | Agda.Syntax.Abstract |
| 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 |
| insertImplicitPatSynArgs | Agda.Syntax.Abstract |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitPatternsT | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitSizeLtPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertingIfAbsent | Agda.Utils.HashTable |
| insertInspects | Agda.TypeChecking.Rules.Def |
| insertLookupWithKey | |
| 1 (Function) | Agda.Utils.Map1 |
| 2 (Function) | Agda.Utils.BiMap |
| insertLookupWithKeyPrecondition | Agda.Utils.BiMap |
| insertMap | Agda.Utils.Map1 |
| insertMapMax | Agda.Utils.Map1 |
| insertMapMin | Agda.Utils.Map1 |
| insertMapWith | Agda.Utils.Map1 |
| insertMapWithKey | Agda.Utils.Map1 |
| insertMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| insertMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| insertMissingFields | Agda.TypeChecking.Records |
| insertMissingFieldsFail | Agda.TypeChecking.Records |
| insertMissingFieldsWarn | Agda.TypeChecking.Records |
| insertMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| insertNames | Agda.TypeChecking.Rules.Def |
| insertOldInteractionScope | Agda.Interaction.InteractionTop |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertPatternsLHSCore | Agda.TypeChecking.Rules.Def |
| insertPrecondition | Agda.Utils.BiMap |
| inserts | Agda.Utils.VarSet |
| insertsDesc | Agda.Utils.VarSet |
| insertSet | Agda.Utils.Set1 |
| insertSetMax | Agda.Utils.Set1 |
| insertSetMin | Agda.Utils.Set1 |
| insertTrailingArgs | Agda.TypeChecking.Coverage |
| insertWith | |
| 1 (Function) | Agda.Utils.Map1 |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| insertWithGood | Agda.Utils.Map |
| insertWithKey | Agda.Utils.Map1 |
| insideAndOutside | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
| insideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InsideOperandCtx | Agda.Syntax.Fixity |
| Instance | Agda.Syntax.Common |
| InstanceArg | Agda.Syntax.Concrete |
| InstanceArgV | Agda.Syntax.Concrete.Operators.Parser |
| InstanceArgWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceArgWithExplicitArg_ | Agda.Interaction.Options.Warnings |
| InstanceB | Agda.Syntax.Concrete |
| instanceClass | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceDef | Agda.Syntax.Common |
| InstanceInfo | |
| 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 |
| InstanceMeta | Agda.Syntax.Info |
| InstanceNoCandidate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceNoCandidate_ | Agda.Interaction.Options.Errors |
| InstanceNoOutputTypeName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceNoOutputTypeName_ | Agda.Interaction.Options.Warnings |
| InstanceNotInArgumentPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceNotInArgumentPosition_ | Agda.Interaction.Options.Warnings |
| instanceOverlap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceP | Agda.Syntax.Concrete |
| InstanceProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| Instances | Agda.Interaction.Options.ProfileOptions |
| InstanceSearch | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InstanceSearchDepthExhausted | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceSearchDepthExhausted_ | Agda.Interaction.Options.Errors |
| InstanceTable | |
| 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 |
| InstanceWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceWithExplicitArg_ | Agda.Interaction.Options.Warnings |
| Instantiable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Instantiate | Agda.TypeChecking.Reduce |
| instantiate | Agda.TypeChecking.Reduce |
| instantiate' | Agda.TypeChecking.Reduce |
| Instantiated | Agda.Interaction.Base |
| instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| instantiateDefinitionType | Agda.TypeChecking.Rules.Decl |
| InstantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull' | Agda.TypeChecking.Reduce |
| instantiateRewriteRule | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| instantiateRewriteRules | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| instantiateTelescope | Agda.TypeChecking.Telescope |
| instantiateVarHeads | Agda.TypeChecking.Injectivity |
| instantiateWhen | Agda.TypeChecking.Reduce |
| Instantiation | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inState | Agda.Syntax.Parser.LexActions |
| instBody | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| instTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Int | Agda.Utils.Haskell.Syntax |
| int | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| Integer | Agda.Compiler.JS.Syntax |
| integer | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Syntax.Parser.LexActions |
| integerA | Agda.TypeChecking.Serialise.Base |
| integerC | Agda.TypeChecking.Serialise.Base |
| integerD | Agda.TypeChecking.Serialise.Base |
| integerSemiring | Agda.Termination.Semiring |
| integerToChar | Agda.Utils.Char |
| Interaction | Agda.Interaction.Base |
| Interaction' | Agda.Interaction.Base |
| InteractionEmacs | Agda.Main |
| InteractionError | |
| 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 |
| interactionError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| interactionErrorName | Agda.TypeChecking.Errors.Names |
| interactionErrorNameString | Agda.Interaction.Options.Errors |
| InteractionError_ | |
| 1 (Type/Class) | Agda.Interaction.Options.Errors |
| 2 (Data Constructor) | Agda.Interaction.Options.Errors |
| InteractionFormat | Agda.Main |
| InteractionId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| interactionId | Agda.Syntax.Common |
| interactionIdToMetaId | Agda.Interaction.BasicOps |
| interactionInteractor | Agda.Main |
| InteractionJson | Agda.Main |
| InteractionMetaBoundaries | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InteractionMetaBoundaries_ | Agda.Interaction.Options.Warnings |
| InteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Interactive | |
| 1 (Data Constructor) | Agda.Interaction.Options.ProfileOptions |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Interactor | Agda.Main |
| interAssocWith | Agda.Termination.SparseMatrix |
| interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| interestingConstraint | Agda.TypeChecking.Pretty.Constraint |
| Interface | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InterfaceFile | Agda.Interaction.FindFile |
| InterfaceInstantiateFull | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InterfacePrefix | Agda.TypeChecking.Serialise |
| interleavedCurrentDeclNum | Agda.Syntax.Concrete.Definitions.Types |
| 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 |
| interleavedMutual | Agda.Syntax.Concrete.Definitions.Types |
| interleavedMutualChecks | Agda.Syntax.Concrete.Definitions.Types |
| InterleavedState | Agda.Syntax.Concrete.Definitions.Types |
| interleaveRanges | Agda.Syntax.Position |
| Internal | Agda.Interaction.Options.ProfileOptions |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InternalError_ | Agda.Interaction.Options.Errors |
| interpret | Agda.Interaction.InteractionTop |
| intersection | |
| 1 (Function) | Agda.Utils.Set1 |
| 2 (Function) | Agda.Utils.Map1 |
| 3 (Function) | Agda.Utils.BoolSet |
| 4 (Function) | Agda.Utils.VarSet |
| 5 (Function) | Agda.Utils.SmallSet |
| intersectionWith | Agda.Utils.Map1 |
| intersectionWithKey | Agda.Utils.Map1 |
| 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 |
| intervalSort | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| intervalsToRange | Agda.Syntax.Position |
| intervalToRange | Agda.Syntax.Position |
| IntervalUniv | Agda.Syntax.Internal |
| intervalUnview | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| intervalUnview' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IntervalView | Agda.Syntax.Internal |
| intervalView | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| intervalView' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IntervalWithoutFile | Agda.Syntax.Position |
| intFilePath | Agda.Interaction.FindFile |
| inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Intro | Agda.Interaction.InteractionTop |
| introTactic | Agda.Interaction.BasicOps |
| intSemiring | Agda.Termination.Semiring |
| IntSet | Agda.Utils.IntSet.Infinite |
| intSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| intToDouble | Agda.Utils.Float |
| intView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidBuiltin_ | Agda.Interaction.Options.Errors |
| InvalidCatchallPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidCatchallPragma_ | Agda.Interaction.Options.Warnings |
| InvalidCharacterLiteral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidCharacterLiteral_ | Agda.Interaction.Options.Warnings |
| InvalidConstructorBlock | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidConstructorBlock_ | Agda.Interaction.Options.Warnings |
| InvalidCoverageCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidCoverageCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidDisplayForm_ | Agda.Interaction.Options.Warnings |
| InvalidDottedExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidDottedExpression_ | Agda.Interaction.Options.Errors |
| InvalidExtensionError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| InvalidFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidFileNameReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidFileName_ | Agda.Interaction.Options.Errors |
| InvalidInstanceHeadType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidInstanceHeadType_ | Agda.Interaction.Options.Errors |
| InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions.Errors |
| InvalidMeasureMutual_ | Agda.Interaction.Options.Errors |
| InvalidModalTelescopeUse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidModalTelescopeUse_ | Agda.Interaction.Options.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.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidPattern_ | Agda.Interaction.Options.Errors |
| InvalidProjectionParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidProjectionParameter_ | Agda.Interaction.Options.Errors |
| InvalidPun | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidPun_ | Agda.Interaction.Options.Errors |
| InvalidTacticAttribute | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidTacticAttribute_ | Agda.Interaction.Options.Warnings |
| InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| InvalidTerminationCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidTypeSort_ | Agda.Interaction.Options.Errors |
| Invariant | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| invariant | |
| 1 (Function) | Agda.Utils.IntSet.Infinite |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inverseApplyCohesion | Agda.Syntax.Common |
| inverseApplyModalityButNotQuantity | Agda.Syntax.Common |
| inverseApplyPolarity | Agda.Syntax.Common |
| inverseApplyQuantity | Agda.Syntax.Common |
| inverseApplyRelevance | Agda.Syntax.Common |
| inverseCompose | Agda.Utils.POMonoid |
| inverseComposeCohesion | Agda.Syntax.Common |
| inverseComposeModality | Agda.Syntax.Common |
| inverseComposePolarity | Agda.Syntax.Common |
| inverseComposePolarity' | Agda.Syntax.Common |
| inverseComposeQuantity | Agda.Syntax.Common |
| inverseComposeRelevance | Agda.Syntax.Common |
| InverseInScope | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InverseInScopeRecompute | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InverseModuleLookup | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InverseNameLookup | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InverseNameModuleRecompute | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InversePermute | Agda.Utils.Permutation |
| inversePermute | Agda.Utils.Permutation |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| InversionDepthReached_ | Agda.Interaction.Options.Warnings |
| InversionMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Base, Agda.TypeChecking.Primitive |
| IOArray | |
| 1 (Type/Class) | Agda.Utils.MinimalArray.MutablePrim |
| 2 (Type/Class) | Agda.Utils.MinimalArray.MutableLifted |
| IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IOne | Agda.Syntax.Internal |
| iOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iOpaqueNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iOptionsUsed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IORef | |
| 1 (Type/Class) | Agda.Utils.IORef |
| 2 (Type/Class) | Agda.Utils.IORef.Strict |
| IOTCM | |
| 1 (Data Constructor) | Agda.Interaction.Base |
| 2 (Type/Class) | Agda.Interaction.Base |
| IOTCM' | Agda.Interaction.Base |
| iPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iPatternSyns | Agda.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 |
| IPBoundary' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcClauseNo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcClosure | Agda.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 |
| ipClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcQName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcWithSub | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IPFace' | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IPNoClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipSolved | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Irrelevant | Agda.Syntax.Common |
| irrelevant | Agda.Syntax.Common |
| irrelevantToShapeIrrelevant | Agda.Syntax.Common |
| IsAbstract | Agda.Syntax.Common |
| isAbsurdBody | Agda.Syntax.Internal |
| isAbsurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isAbsurdP | Agda.Syntax.Concrete |
| isAbsurdPatternName | Agda.Syntax.Internal |
| isAccessibleDef | Agda.TypeChecking.Opacity |
| isAHole | Agda.Syntax.Notation |
| isAlias | Agda.TypeChecking.Rules.Def |
| IsAmbiguous | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| isBenchmarkOn | Agda.Utils.Benchmark |
| isBinder | Agda.Syntax.Notation |
| isBinderP | Agda.Syntax.Concrete |
| isBinderUsed | Agda.TypeChecking.Free |
| isBlocked | Agda.TypeChecking.Reduce |
| isBlockedTerm | Agda.TypeChecking.MetaVars |
| isBlockingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsBool | Agda.Utils.Boolean |
| isBounded | Agda.TypeChecking.SizedTypes |
| isBoundedProjVar | Agda.TypeChecking.SizedTypes |
| isBoundedSizeType | Agda.TypeChecking.SizedTypes |
| IsBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isBuiltin | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| IsBuiltinModule | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isBuiltinModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsBuiltinModuleWithSafePostulates | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isBuiltinModuleWithSafePostulates | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isBuiltinNoDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isCanonical | Agda.TypeChecking.Conversion |
| isClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| IsConstructor | Agda.Syntax.Common |
| isConstructor | Agda.TypeChecking.Datatypes |
| isContinuous | Agda.Syntax.Common |
| isCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isCovered | Agda.TypeChecking.Coverage |
| isCubicalSubtype | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| IsData | Agda.Syntax.Internal |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| IsEllipsis | Agda.Syntax.Concrete.Pattern |
| isEllipsis | Agda.Syntax.Concrete.Pattern |
| IsEmpty | |
| 1 (Data Constructor) | Agda.Utils.Set1 |
| 2 (Data Constructor) | Agda.Utils.Map1 |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isEmpty | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.Termination.SparseMatrix |
| isEmptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isEmptyObject | Agda.Compiler.JS.Compiler |
| isEmptyTel | Agda.TypeChecking.Empty |
| IsEmptyType | Agda.Interaction.Base |
| isEmptyType | Agda.TypeChecking.Empty |
| isEnabled | Agda.Compiler.Backend.Base, 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 |
| isEtaRecordConstructor | Agda.TypeChecking.Records |
| isEtaRecordDef | Agda.TypeChecking.Records |
| isEtaRecordType | Agda.TypeChecking.Records |
| isEtaVar | Agda.TypeChecking.Records |
| isExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsExpr | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser |
| isExtendedLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isExtendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isFaceConstraint | Agda.TypeChecking.MetaVars |
| IsFam | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| IsFibrant | |
| 1 (Type/Class) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
| isFibrant | Agda.TypeChecking.Irrelevance |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| isForced | Agda.TypeChecking.Forcing |
| IsFree | Agda.TypeChecking.Free.Reduce |
| isFrozen | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isFunName | Agda.Syntax.Concrete.Definitions.Types |
| isGeneralizableMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isGeneralizedVarName | Agda.Interaction.MakeCase |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsIApply | Agda.TypeChecking.Coverage.Match |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isIncoherent | Agda.Syntax.Common |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsInstance | Agda.Syntax.Common |
| isInstance | Agda.Syntax.Common |
| isInstanceConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend |
| IsInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isInstantiatedMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isInteractionMetaB | Agda.TypeChecking.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 |
| isLambdaNotation | 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 |
| isLevelUniverseEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsList | Agda.Utils.List1 |
| isLocal | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| IsMain | |
| 1 (Type/Class) | Agda.Syntax.Common, Agda.Compiler.Common, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Syntax.Common, Agda.Compiler.Common, Agda.Compiler.Backend |
| 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 |
| isModuleAlive | Agda.Syntax.Scope.Base |
| isModuleFreeVar | Agda.TypeChecking.Rules.Term |
| isName | Agda.Interaction.BasicOps |
| isNameAlive | Agda.Syntax.Scope.Base |
| isNameInScope | Agda.Syntax.Scope.Base |
| isNameInScopeUnqualified | Agda.Syntax.Scope.Base |
| isNameOfUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isNegInf | Agda.Utils.Float |
| isNegZero | Agda.Utils.Float |
| isNeutral | Agda.TypeChecking.MetaVars.Occurs |
| isNewerThan | Agda.Utils.FileName |
| isNoAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| IsNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| IsNonEmpty | |
| 1 (Data Constructor) | Agda.Utils.Set1 |
| 2 (Data Constructor) | Agda.Utils.Map1 |
| isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNoResult | Agda.Mimer.Types |
| IsNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| isNothing | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| IsNotLock | Agda.Syntax.Common |
| iso | Agda.Utils.Lens |
| isolatedNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| IsOpaque | Agda.Syntax.Common |
| isOpenMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| iSourceHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isOverlappable | Agda.Syntax.Common |
| isOverlapping | Agda.Syntax.Common |
| isPath | Agda.TypeChecking.Telescope |
| IsPathCons | Agda.TypeChecking.Rules.Data |
| isPathCons | Agda.TypeChecking.Datatypes |
| isPathType | Agda.Syntax.Internal |
| IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsPattern | Agda.Syntax.Common |
| isPattern | Agda.Syntax.Concrete |
| IsPatternSynonym | Agda.Syntax.Common |
| isPosInf | Agda.Utils.Float |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isPosZero | Agda.Utils.Float |
| isPragma | Agda.Syntax.Concrete |
| 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.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsPrimitiveModule | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isPrimitiveModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProblemCompletelySolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProblemSolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProblemSolved' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProjectionButNotCoinductive | Agda.Termination.Monad |
| isProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| isProp | Agda.Syntax.Internal |
| isPropEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProperApplyElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| isProperProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isProperSubmapOf | Agda.Utils.Map1 |
| isProperSubmapOfBy | Agda.Utils.Map1 |
| isProperSubsetOf | Agda.Utils.Set1 |
| isPropM | Agda.TypeChecking.Irrelevance |
| isQName | Agda.Interaction.BasicOps |
| isQualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isQuantity0 | Agda.Syntax.Common |
| isQuantityAttribute | Agda.Syntax.Concrete.Attribute |
| isQuantityω | Agda.Syntax.Common |
| isReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsRecord | Agda.Syntax.Internal |
| isRecord | Agda.TypeChecking.Records |
| isRecordConstructor | |
| 1 (Function) | Agda.Syntax.Scope.Monad |
| 2 (Function) | Agda.TypeChecking.Records |
| IsRecordModule | Agda.Syntax.Scope.Base |
| isRecordType | Agda.TypeChecking.Records |
| IsRecord_ | Agda.Syntax.Internal |
| isRecursiveRecord | Agda.TypeChecking.Records |
| IsReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isRelevanceAttribute | Agda.Syntax.Concrete.Attribute |
| isRelevant | Agda.Syntax.Common |
| isRelevantProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isRelevantProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isRemoteMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isRight | Agda.Utils.Either |
| isSafeInteger | Agda.Utils.Float |
| isShapeIrrelevant | Agda.Syntax.Common |
| isSingleBranch | Agda.Utils.CompressedTrie |
| isSingleIdentifierP | Agda.Syntax.Concrete |
| isSingleMap | Agda.Utils.Map |
| 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.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSizeNameTestRaw | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSizeProblem | Agda.TypeChecking.SizedTypes |
| IsSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSizeTypeTest | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSmallSort | Agda.TypeChecking.Substitute |
| isSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSort | Agda.Syntax.Internal |
| isSortJudgement | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSortMeta_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSourceCodeWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isStaticFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsStrict | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
| isStrictDataSort | Agda.Syntax.Internal |
| isStronglyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| isSubmapOf | Agda.Utils.Map1 |
| isSubmapOfBy | Agda.Utils.Map1 |
| isSubscriptDigit | Agda.Utils.Suffix |
| isSubsetOf | |
| 1 (Function) | Agda.Utils.Set1 |
| 2 (Function) | Agda.Utils.BoolSet |
| 3 (Function) | Agda.Utils.VarSet |
| isSurrogateCodePoint | Agda.Utils.Char |
| ISt | Agda.Syntax.Concrete.Definitions.Types |
| isTacticAttribute | Agda.Syntax.Concrete.Attribute |
| iStart | Agda.Syntax.Position |
| iStart' | Agda.Syntax.Position |
| isTimeless | Agda.TypeChecking.Lock |
| isTop | Agda.TypeChecking.SizedTypes.Utils |
| isTopLevelValue | Agda.Compiler.JS.Compiler |
| isTrivialPattern | Agda.TypeChecking.Coverage.SplitPattern |
| isTwoLevelEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isType | Agda.TypeChecking.Rules.Term |
| isType' | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isTypeDatatype | Agda.Mimer.Monad |
| isTypeEqualTo | Agda.TypeChecking.Rules.Term |
| IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isType_ | Agda.TypeChecking.Rules.Term |
| isUnderscore | Agda.Syntax.Common |
| isUnguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| isUnifyStateSolved | Agda.TypeChecking.Rules.LHS.Unify.Types |
| isUnnamed | Agda.Syntax.Common |
| isUnqualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| isUnsolvedWarning | Agda.TypeChecking.Warnings |
| isUnstableDef | Agda.TypeChecking.Injectivity |
| 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 |
| isWithFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IsWithP | Agda.Syntax.Concrete.Pattern |
| isWithP | Agda.Syntax.Concrete.Pattern |
| isWithPattern | Agda.Syntax.Concrete.Pattern |
| isYesOverlap | Agda.Syntax.Common |
| IsZero | Agda.Utils.TypeLevel |
| isZeroNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| itableCounts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| itableTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Item | |
| 1 (Type/Class) | Agda.Utils.List1, Agda.Utils.List1 |
| 2 (Type/Class) | Agda.TypeChecking.Positivity |
| iterate | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Utils.ListInf |
| iterate' | Agda.Utils.Function |
| iterateSolver | Agda.TypeChecking.SizedTypes.WarshallSolver |
| iterateUntil | Agda.Utils.Function |
| iterateUntilM | Agda.Utils.Function |
| iterWhile | Agda.Utils.Function |
| iTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IVar | Agda.Utils.Haskell.Syntax |
| iWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Ix | Agda.Utils.IArray, Agda.Utils.SmallSet |
| ixmap | Agda.Utils.IArray |
| IZero | Agda.Syntax.Internal |