| IApply | Agda.Syntax.Internal |
| IApplyP | Agda.Syntax.Internal |
| iApplyVars | Agda.TypeChecking.Telescope.Path |
| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| 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 |
| 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 |
| idViewAsPath | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 | Agda.Utils.Null |
| ifNotNullM | Agda.Utils.Null |
| ifNotPi | Agda.TypeChecking.Telescope |
| ifNotPiOrPathType | Agda.TypeChecking.Telescope |
| ifNotPiType | Agda.TypeChecking.Telescope |
| ifNull | Agda.Utils.Null |
| ifNullM | Agda.Utils.Null |
| iForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ifPath | Agda.TypeChecking.Rules.Term |
| ifPi | Agda.TypeChecking.Telescope |
| ifPiType | Agda.TypeChecking.Telescope |
| 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 |
| ignoreAllInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ignoreBlocking | Agda.Syntax.Internal |
| IgnoreInAnnotations | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ilam | Agda.TypeChecking.Names |
| iLength | Agda.Syntax.Position |
| IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IllegalPatternInTelescope | 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 |
| IllformedProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| illiterate | Agda.Syntax.Parser.Literate |
| IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad, Agda.Compiler.Backend |
| IMax | Agda.Syntax.Internal |
| imax | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| IMin | Agda.Syntax.Internal |
| imin | 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 |
| 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 |
| importQualified | Agda.Utils.Haskell.Syntax |
| imports | 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 |
| ImpossibleConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impossibleTest | 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inameMap | Agda.Syntax.Scope.Monad |
| inc | Agda.Utils.Warshall |
| InClause | Agda.TypeChecking.Positivity.Occurrence |
| includes | Agda.TypeChecking.Serialise.Base |
| includeStateChanges | Agda.Interaction.Imports |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inConcreteOrAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| increase | Agda.Termination.Order |
| inCxt | Agda.TypeChecking.Names |
| IndArgType | Agda.TypeChecking.Positivity.Occurrence |
| InDefOf | Agda.TypeChecking.Positivity.Occurrence |
| indent | Agda.Utils.String |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| Induction | Agda.Syntax.Common |
| Inductive | Agda.Syntax.Common |
| INeg | Agda.Syntax.Internal |
| Inf | Agda.Syntax.Internal |
| inf | Agda.TypeChecking.Positivity |
| InfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InfectiveImport_ | Agda.Interaction.Options.Warnings |
| infectiveOptions | Agda.Interaction.Options |
| 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 |
| inferMeta | Agda.TypeChecking.Rules.Term |
| inferPiSort | Agda.TypeChecking.Sort |
| Inferred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| inferSort | Agda.TypeChecking.CheckInternal |
| infertypevar | Agda.Auto.CaseSplit |
| inferUnivSort | Agda.TypeChecking.Sort |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Infty | Agda.TypeChecking.SizedTypes.Syntax |
| initAutoOptions | Agda.Auto.Options |
| initCCEnv | Agda.Compiler.MAlonzo.Compiler |
| initCommandState | Agda.Interaction.Base |
| initCopyInfo | Agda.Syntax.Abstract |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| initExpRefInfo | Agda.Auto.SearchControl |
| initFreeEnv | Agda.TypeChecking.Free.Lazy |
| initGraph | Agda.Utils.Warshall |
| initialDotState | Agda.Interaction.Highlighting.Dot |
| initialiseCommandQueue | Agda.Interaction.InteractionTop |
| initLast | Agda.Utils.List |
| initLHSState | Agda.TypeChecking.Rules.LHS.ProblemRest |
| initMapS | Agda.Auto.Convert |
| initMaybe | Agda.Utils.List |
| initMeta | Agda.Auto.NarrowingSearch |
| initOccursCheck | Agda.TypeChecking.MetaVars.Occurs |
| initPersistentState | 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 |
| initState | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InjectivePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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.BiMap |
| 2 (Function) | Agda.Utils.Bag |
| 3 (Function) | Agda.Utils.SmallSet |
| 4 (Function) | Agda.Utils.Trie |
| 5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 6 (Function) | Agda.Utils.Favorites |
| 7 (Function) | Agda.Utils.AssocList |
| 8 (Function) | Agda.Termination.CallMatrix |
| 9 (Function) | Agda.Termination.CallGraph |
| 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 |
| insertImplicitPatSynArgs | Agda.Syntax.Abstract |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitPatternsT | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitSizeLtPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
| insertMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| insertMissingFields | Agda.TypeChecking.Records |
| insertMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| insertOldInteractionScope | Agda.Interaction.InteractionTop |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertPatternsLHSCore | Agda.TypeChecking.Rules.Def |
| insertTrailingArgs | Agda.TypeChecking.Coverage |
| insertWith | |
| 1 (Function) | Agda.Utils.Trie |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 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 |
| InstanceDef | Agda.Syntax.Common |
| InstanceNoCandidate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceNoOutputTypeName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceNoOutputTypeName_ | Agda.Interaction.Options.Warnings |
| InstanceP | Agda.Syntax.Concrete |
| InstanceSearch | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| InstanceSearchDepthExhausted | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InstanceTable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| instanceTransformBiMT' | Agda.Utils.Geniplate |
| instanceUniverseBiT' | Agda.Utils.Geniplate |
| 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 |
| inState | Agda.Syntax.Parser.LexActions |
| InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| Interaction | Agda.Interaction.Base |
| interaction | Agda.Interaction.CommandLine |
| Interaction' | Agda.Interaction.Base |
| InteractionId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| interactionId | Agda.Syntax.Common |
| interactionLoop | Agda.Interaction.CommandLine |
| InteractionOutputCallback | Agda.Interaction.Response |
| InteractionPoint | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Interactive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| interAssocWith | Agda.Termination.SparseMatrix |
| interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| interestingConstraint | Agda.TypeChecking.Pretty.Warning |
| Interface | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InterfaceFile | Agda.Interaction.FindFile |
| interleaveRanges | Agda.Syntax.Position |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| interpret | Agda.Interaction.InteractionTop |
| intersection | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.SmallSet |
| intersectVars | Agda.TypeChecking.Conversion |
| intersectWith | Agda.Termination.SparseMatrix |
| 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.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 |
| intMap | Agda.Utils.Warshall |
| inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Intro | Agda.Interaction.InteractionTop |
| intros | Agda.Compiler.MAlonzo.Compiler |
| introTactic | Agda.Interaction.BasicOps |
| intSemiring | Agda.Termination.Semiring |
| IntSet | Agda.Utils.IntSet.Infinite |
| intView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidCatchallPragma | Agda.Syntax.Concrete.Definitions |
| InvalidCatchallPragma_ | Agda.Interaction.Options.Warnings |
| InvalidCoverageCheckPragma | Agda.Syntax.Concrete.Definitions |
| InvalidCoverageCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidExtensionError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions |
| InvalidName | Agda.Syntax.Concrete.Definitions |
| InvalidNoPositivityCheckPragma | Agda.Syntax.Concrete.Definitions |
| InvalidNoPositivityCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidNoUniverseCheckPragma | Agda.Syntax.Concrete.Definitions |
| InvalidNoUniverseCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions |
| InvalidTerminationCheckPragma_ | Agda.Interaction.Options.Warnings |
| InvalidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Invariant | 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 |
| inverseApplyModality | 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 |
| inverseScopeLookup | Agda.Syntax.Scope.Base |
| inverseScopeLookup' | Agda.Syntax.Scope.Base |
| inverseScopeLookupModule | 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 |
| IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IOne | Agda.Syntax.Internal |
| iOptionsUsed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| iPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipbEquations | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipbMetaApp | 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 |
| ipbOverapplied | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipbValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ipcBoundary | 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 |
| ipMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| IPNoClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| iPragmaOptions | 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 |
| IrrelevantDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| irrToNonStrict | 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 |
| 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 |
| isApplyElim' | Agda.Syntax.Internal |
| IsBase | Agda.Utils.TypeLevel |
| 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 |
| isBuiltin | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| isBuiltinModule | Agda.Interaction.Options.Lenses |
| isBuiltinModuleWithSafePostulates | Agda.Interaction.Options.Lenses |
| isCached | Agda.Interaction.Imports |
| 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 |
| isCoinductive | Agda.TypeChecking.Rules.Data |
| isCoinductiveProjection | Agda.Termination.Monad |
| isCon | Agda.TypeChecking.Unquote |
| 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 |
| IsData | Agda.Syntax.Common |
| 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 | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isEmpty | |
| 1 (Function) | Agda.Utils.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 |
| isEqualityType | Agda.Syntax.Internal |
| isErasable | Agda.Compiler.Treeless.Erase |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| IsFam | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| 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 |
| isFullyInstantiatedMeta | Agda.TypeChecking.Reduce |
| isGeneralizableMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isGeneratedRecordConstructor | Agda.TypeChecking.Records |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsIApply | Agda.TypeChecking.Coverage.Match |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.InstanceArguments |
| 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 |
| isInternalAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| isLocal | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Compiler.Common, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Compiler.Common, Agda.Compiler.Backend |
| isMainFunction | Agda.Compiler.MAlonzo.Primitives |
| 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 |
| isNameInScope | Agda.Syntax.Scope.Base |
| isNeutral | Agda.TypeChecking.MetaVars.Occurs |
| isNewerThan | Agda.Interaction.Imports |
| 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.Cubical, Agda.TypeChecking.Primitive |
| isNothing | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| isolatedNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 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 |
| isPath | Agda.TypeChecking.Telescope |
| IsPathCons | Agda.TypeChecking.Rules.Data |
| isPathType | Agda.Syntax.Internal |
| IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isPattern | Agda.Syntax.Concrete |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsPrefixOf | Agda.TypeChecking.Abstract |
| isPrefixOf | Agda.TypeChecking.Abstract |
| isPrimEq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| isPrimitive | Agda.TypeChecking.Monad.Builtin, 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 |
| isProjElim | 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.TypeChecking.Monad, Agda.Compiler.Backend |
| isProperProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isPropM | Agda.TypeChecking.Irrelevance |
| isQName | Agda.Interaction.BasicOps |
| isQualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isQuantityAttribute | Agda.Syntax.Concrete.Attribute |
| IsRecord | Agda.Syntax.Common |
| isRecord | Agda.TypeChecking.Records |
| isRecordConstructor | Agda.TypeChecking.Records |
| isRecordType | Agda.TypeChecking.Records |
| 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 |
| isRight | Agda.Utils.Either |
| isSet | Agda.Syntax.Abstract.Views |
| 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.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 |
| 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 |
| isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isSortMeta_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| isStaticFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| isTacticAttribute | Agda.Syntax.Concrete.Attribute |
| iStart | Agda.Syntax.Position |
| isTop | Agda.TypeChecking.SizedTypes.Utils |
| isTopLevelValue | Agda.Compiler.JS.Compiler |
| isTrivialPattern | Agda.TypeChecking.Coverage.Match |
| isType | Agda.TypeChecking.Rules.Term |
| isType' | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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 |
| 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 |
| isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Function |
| iterateSolver | Agda.TypeChecking.SizedTypes.WarshallSolver |
| iterateUntil | Agda.Utils.Function |
| iterateUntilM | Agda.Utils.Function |
| iterWhile | Agda.Utils.Function |
| 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.SmallSet |
| IZero | Agda.Syntax.Internal |