| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ICArgList | Agda.Auto.Syntax |
| ICExp | Agda.Auto.Syntax |
| icnvh | Agda.Auto.Convert |
| Id | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| idempotent | Agda.Termination.Termination |
| Ident | Agda.Syntax.Concrete |
| identifier | |
| 1 (Function) | Agda.Compiler.JS.Parser |
| 2 (Function) | Agda.Syntax.Parser.LexActions |
| identity | Agda.Utils.TestHelpers |
| IdentP | Agda.Syntax.Concrete |
| idP | Agda.Utils.Permutation |
| IdPart | Agda.Syntax.Notation |
| IdS | Agda.TypeChecking.Substitute |
| idS | Agda.TypeChecking.Substitute |
| iEnd | Agda.Syntax.Position |
| If | |
| 1 (Data Constructor) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| ifBlock | Agda.Compiler.JS.Parser |
| ifBlocked | Agda.TypeChecking.Reduce |
| ifBlockedType | Agda.TypeChecking.Reduce |
| ifClean | Agda.TypeChecking.Rules.LHS.Unify |
| ifDirty | Agda.Utils.Update |
| ifJustM | |
| 1 (Function) | Agda.Utils.Maybe.Strict |
| 2 (Function) | Agda.Utils.Maybe |
| ifLe | Agda.TypeChecking.SizedTypes.Syntax |
| ifM | Agda.Utils.Monad |
| ifNoConstraints | Agda.TypeChecking.Constraints |
| ifNoConstraints_ | Agda.TypeChecking.Constraints |
| ifNotM | Agda.Utils.Monad |
| IFSNoCandidateInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iFullHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| IgnoreAll | Agda.TypeChecking.Free |
| ignoreBlocking | Agda.Syntax.Internal |
| ignoreForced | |
| 1 (Function) | Agda.TypeChecking.Irrelevance |
| 2 (Function) | Agda.Compiler.Epic.Erasure |
| IgnoreInAnnotations | Agda.TypeChecking.Free |
| ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| IgnoreNot | Agda.TypeChecking.Free |
| ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ignoreSharing | Agda.Syntax.Internal |
| ignoreSharingType | Agda.Syntax.Internal |
| IgnoreSorts | Agda.TypeChecking.Free |
| iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ihname | Agda.Compiler.MAlonzo.Misc |
| iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IM | Agda.Interaction.Monad |
| iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ImpInsert | Agda.TypeChecking.Implicit |
| impInsert | Agda.TypeChecking.Implicit |
| implicitArgs | Agda.TypeChecking.Implicit |
| ImplicitFlex | Agda.TypeChecking.Rules.LHS.Problem |
| ImplicitInsertion | Agda.TypeChecking.Implicit |
| implicitNamedArgs | Agda.TypeChecking.Implicit |
| ImplicitP | Agda.Syntax.Abstract |
| implicitP | Agda.TypeChecking.Rules.LHS.Implicit |
| implies | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Import | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| ImportDirective | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importDirRange | Agda.Syntax.Concrete |
| ImportedModule | Agda.Syntax.Concrete |
| importedModules | Agda.Compiler.Epic.CompileState |
| ImportedName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importedName | Agda.Syntax.Concrete |
| ImportedNS | Agda.Syntax.Scope.Base |
| ImportPragma | Agda.Syntax.Concrete |
| imports | Agda.Compiler.MAlonzo.Compiler |
| importsForPrim | Agda.Compiler.MAlonzo.Primitives |
| IMPOSSIBLE | Agda.Compiler.Epic.AuxAST |
| Impossible | |
| 1 (Type/Class) | Agda.Utils.Impossible |
| 2 (Data Constructor) | Agda.Utils.Impossible |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impossibleTest | Agda.ImpossibleTest |
| imp_dir | Agda.Syntax.Parser.Lexer |
| inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inc | Agda.Utils.Warshall |
| InClause | Agda.TypeChecking.Positivity |
| IncludeDirs | Agda.Interaction.Options |
| Inclusion | |
| 1 (Type/Class) | Agda.Utils.PartialOrd |
| 2 (Data Constructor) | Agda.Utils.PartialOrd |
| inclusion | Agda.Utils.PartialOrd |
| incoming | Agda.TypeChecking.SizedTypes.WarshallSolver |
| IncompletePattern | Agda.Interaction.Highlighting.Precise |
| IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| increase | Agda.Termination.Order |
| IndArgType | Agda.TypeChecking.Positivity |
| InDefOf | Agda.TypeChecking.Positivity |
| indent | Agda.Utils.String |
| independent | Agda.Interaction.InteractionTop |
| Index | Agda.Utils.Suffix |
| IndexVariablesNotDistinct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IndicesFreeInParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IndicesNotConstructorApplications | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Indirect | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Induction | Agda.Syntax.Common |
| Inductive | Agda.Syntax.Common |
| Inf | Agda.Syntax.Internal |
| inf | Agda.TypeChecking.Positivity |
| inferable | Agda.Compiler.Epic.Smashing |
| inferableTerm | Agda.Compiler.Epic.Smashing |
| InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferDef | Agda.TypeChecking.Rules.Term |
| InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker |
| inferExprForWith | Agda.TypeChecking.Rules.Term |
| inferHead | Agda.TypeChecking.Rules.Term |
| inferMeta | Agda.TypeChecking.Rules.Term |
| infertypevar | Agda.Auto.CaseSplit |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| infimum | Agda.Termination.Order |
| Infinite | Agda.Utils.Warshall |
| infinite | Agda.Utils.Warshall |
| infiniteList | Agda.Utils.QuickCheck |
| infiniteListOf | Agda.Utils.QuickCheck |
| Infinity | Agda.TypeChecking.SizedTypes.WarshallSolver |
| infinityFlexs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Infix | Agda.Syntax.Concrete |
| InfixDef | Agda.Syntax.Common |
| infixlP | Agda.Syntax.Concrete.Operators.Parser |
| infixP | Agda.Syntax.Concrete.Operators.Parser |
| infixrP | Agda.Syntax.Concrete.Operators.Parser |
| infodecl | Agda.Compiler.MAlonzo.Compiler |
| Info_AllGoals | Agda.Interaction.Response |
| Info_Auto | Agda.Interaction.Response |
| Info_CompilationOk | Agda.Interaction.Response |
| Info_Constraints | Agda.Interaction.Response |
| Info_Context | Agda.Interaction.Response |
| Info_CurrentGoal | Agda.Interaction.Response |
| Info_Error | Agda.Interaction.Response |
| Info_GoalType | Agda.Interaction.Response |
| Info_HelperFunction | Agda.Interaction.Response |
| Info_InferredType | Agda.Interaction.Response |
| Info_Intro | Agda.Interaction.Response |
| Info_ModuleContents | Agda.Interaction.Response |
| Info_NormalForm | Agda.Interaction.Response |
| Info_WhyInScope | Agda.Interaction.Response |
| Infty | Agda.TypeChecking.SizedTypes.Syntax |
| initCommandState | Agda.Interaction.InteractionTop |
| initCompileState | Agda.Compiler.Epic.CompileState |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| initGraph | Agda.Utils.Warshall |
| initialDotState | Agda.Interaction.Highlighting.Dot |
| initialIFSCandidates | Agda.TypeChecking.InstanceArguments |
| initializeIFSMeta | Agda.TypeChecking.InstanceArguments |
| initialPrims | Agda.Compiler.Epic.Primitive |
| initialRels | Agda.Compiler.Epic.Erasure |
| initialTags | Agda.Compiler.Epic.Injection |
| initiate | Agda.Compiler.Epic.Erasure |
| initLast | Agda.Utils.List |
| initMapS | Agda.Auto.Convert |
| initMeta | Agda.Auto.NarrowingSearch |
| initOccursCheck | Agda.TypeChecking.MetaVars.Occurs |
| initPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| initState | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| injArg | Agda.Compiler.Epic.Interface |
| injArity | Agda.Compiler.Epic.Interface |
| InjConstraints | Agda.Compiler.Epic.Injection |
| Injectible | Agda.Compiler.Epic.Injection |
| InjectiveFun | |
| 1 (Type/Class) | Agda.Compiler.Epic.Interface |
| 2 (Data Constructor) | Agda.Compiler.Epic.Interface |
| injectiveFuns | Agda.Compiler.Epic.Interface |
| Injectivity | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| Inline | Agda.Compiler.Epic.AuxAST |
| inlineWithClauses | Agda.Termination.Inlining |
| inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| inNameSpace | Agda.Syntax.Scope.Base |
| InScope | Agda.Syntax.Scope.Base |
| inScopeBecause | Agda.Syntax.Scope.Base |
| InScopeTag | Agda.Syntax.Scope.Base |
| inScopeTag | Agda.Syntax.Scope.Base |
| insert | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Utils.Graph.AdjacencyMap |
| 4 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 5 (Function) | Agda.Utils.Favorites |
| 6 (Function) | Agda.Utils.Trie |
| 7 (Function) | Agda.Termination.CallMatrix |
| 8 (Function) | Agda.Termination.CallGraph |
| insertAfter | Agda.Compiler.JS.Compiler |
| insertAt | Agda.Compiler.Epic.Injection |
| insertCompared | Agda.Utils.Favorites |
| insertEdge | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| insertEdgeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| insertImplicit | Agda.TypeChecking.Implicit |
| insertImplicitPatSynArgs | Agda.Syntax.Abstract |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitPatternsT | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertTele | Agda.Compiler.Epic.Forcing |
| insertWith | |
| 1 (Function) | Agda.Utils.HashMap |
| 2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 3 (Function) | Agda.Utils.Trie |
| insertWithKeyM | Agda.Utils.Map |
| insideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| InsideOperandCtx | Agda.Syntax.Fixity |
| insideScope | Agda.Syntax.Translation.ConcreteToAbstract |
| Instance | |
| 1 (Data Constructor) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| InstanceArg | Agda.Syntax.Concrete |
| InstanceArgV | Agda.Syntax.Concrete.Operators.Parser |
| InstanceP | Agda.Syntax.Concrete |
| instanceTransformBiMT' | Agda.Utils.Geniplate |
| instanceUniverseBiT' | Agda.Utils.Geniplate |
| Instantiable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Instantiate | Agda.TypeChecking.Reduce |
| instantiate | Agda.TypeChecking.Reduce |
| instantiate' | Agda.TypeChecking.Reduce |
| Instantiated | Agda.Interaction.BasicOps |
| instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| instantiateDefinitionType | Agda.TypeChecking.Rules.Decl |
| InstantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull | Agda.TypeChecking.Reduce |
| instantiateFull' | Agda.TypeChecking.Reduce |
| instantiatePattern | Agda.TypeChecking.Rules.LHS |
| instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate |
| inState | Agda.Syntax.Parser.LexActions |
| InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| int | Agda.Utils.Pretty |
| Integer | Agda.Compiler.JS.Syntax |
| integer | Agda.Utils.Pretty |
| integerSemiring | Agda.Termination.Semiring |
| Interaction | Agda.Interaction.InteractionTop |
| interaction | Agda.Interaction.CommandLine.CommandLine |
| Interaction' | Agda.Interaction.InteractionTop |
| InteractionId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| interactionId | Agda.Syntax.Common |
| interactionLoop | Agda.Interaction.CommandLine.CommandLine |
| InteractionOutputCallback | Agda.Interaction.Response |
| InteractionPoint | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Interactive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| Interface | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| interpret | Agda.Interaction.InteractionTop |
| intersection | Agda.Utils.HashMap |
| intersectionWith | Agda.Utils.HashMap |
| intersectVars | Agda.TypeChecking.Conversion |
| intersectWith | Agda.Termination.SparseMatrix |
| Interval | |
| 1 (Type/Class) | Agda.Syntax.Position |
| 2 (Data Constructor) | Agda.Syntax.Position |
| Interval' | Agda.Syntax.Position |
| intervalInvariant | Agda.Syntax.Position |
| intLit | Agda.Compiler.JS.Parser |
| intMap | Agda.Utils.Warshall |
| inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| introTactic | Agda.Interaction.BasicOps |
| intSemiring | Agda.Termination.Semiring |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidNoTerminationCheckPragma | Agda.Syntax.Concrete.Definitions |
| InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InvalidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| invariant | Agda.Utils.Graph.AdjacencyMap |
| Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inverseApplyRelevance | Agda.TypeChecking.Irrelevance |
| inverseComposeRelevance | Agda.TypeChecking.Irrelevance |
| inverseScopeLookup | Agda.Syntax.Scope.Base |
| inverseScopeLookupModule | Agda.Syntax.Scope.Base |
| inverseScopeLookupName | Agda.Syntax.Scope.Base |
| inverseSubst | Agda.TypeChecking.MetaVars |
| InvertExcept | Agda.TypeChecking.MetaVars |
| invertP | Agda.Utils.Permutation |
| invLookup | Agda.Utils.BiMap |
| InvView | Agda.TypeChecking.Injectivity |
| io | Agda.TypeChecking.Primitive |
| IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ioProperty | Agda.Utils.QuickCheck |
| iotapossmeta | Agda.Auto.Typecheck |
| iotastep | Agda.Auto.Typecheck |
| IOTCM | |
| 1 (Data Constructor) | Agda.Interaction.InteractionTop |
| 2 (Type/Class) | Agda.Interaction.InteractionTop |
| IOTCM' | Agda.Interaction.InteractionTop |
| iPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ipMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ipRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Irr | Agda.Compiler.Epic.Interface |
| Irrel | Agda.TypeChecking.MetaVars.Occurs |
| Irrelevant | Agda.Syntax.Common |
| IrrelevantDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Irrelevantly | Agda.TypeChecking.Free |
| irrelevantOrUnused | Agda.TypeChecking.Irrelevance |
| irrelevantVars | Agda.TypeChecking.Free |
| irrToNonStrict | Agda.TypeChecking.Irrelevance |
| IsAbstract | Agda.Syntax.Common |
| isAbsurdBody | Agda.Syntax.Internal |
| isAbsurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isAHole | Agda.Syntax.Notation |
| isAlias | Agda.TypeChecking.Rules.Def |
| isAnonymousModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| isApplyElim | Agda.Syntax.Internal |
| isBelow | Agda.Utils.Warshall |
| isBinderUsed | Agda.TypeChecking.Free |
| isBindingHole | Agda.Syntax.Notation |
| isBlockedTerm | Agda.TypeChecking.MetaVars |
| IsBothfix | Agda.Utils.List |
| isBounded | Agda.TypeChecking.SizedTypes |
| isCoinductive | Agda.TypeChecking.Rules.Data |
| isCon | Agda.TypeChecking.Quote |
| iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IsData | Agda.TypeChecking.Datatypes |
| isDataOrRecord | Agda.TypeChecking.Datatypes |
| isDataOrRecordType | Agda.TypeChecking.Datatypes |
| isDatatype | |
| 1 (Function) | Agda.TypeChecking.Datatypes |
| 2 (Function) | Agda.TypeChecking.Coverage |
| isDatatypeModule | Agda.Syntax.Scope.Monad |
| isDecr | Agda.Termination.Order |
| IsDominated | Agda.Utils.Favorites |
| IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isEmpty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Termination.SparseMatrix |
| isEmptyObject | Agda.Compiler.JS.Compiler |
| IsEmptyType | Agda.Interaction.BasicOps |
| isEmptyType | Agda.TypeChecking.Empty |
| ISet | |
| 1 (Type/Class) | Agda.Utils.PartialOrd |
| 2 (Data Constructor) | Agda.Utils.PartialOrd |
| iset | Agda.Utils.PartialOrd |
| isEtaCon | Agda.TypeChecking.Records |
| isEtaExpandable | Agda.TypeChecking.MetaVars |
| isEtaRecord | Agda.TypeChecking.Records |
| isEtaRecordType | Agda.TypeChecking.Records |
| isEtaRecordTypeHH | Agda.TypeChecking.Rules.LHS.Unify |
| IsExpr | Agda.Syntax.Concrete.Operators.Parser |
| isFlexNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| isFrozen | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isGeneratedRecordConstructor | Agda.TypeChecking.Records |
| isHaskellKind | Agda.Compiler.HaskellTypes |
| isHidden | Agda.Syntax.Common |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isHom | Agda.TypeChecking.Rules.LHS.Unify |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isInductiveRecord | Agda.TypeChecking.Records |
| IsInfix | Agda.Syntax.Common |
| isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isInftyNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| isInjective | Agda.Compiler.Epic.Injection |
| isInjectiveHere | Agda.Compiler.Epic.Injection |
| isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| isInsideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| isInstantiatedMeta | |
| 1 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.TypeChecking.Reduce.Monad |
| isInstantiatedMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isIrr | Agda.Compiler.Epic.Erasure |
| isIrrelevant | Agda.Syntax.Common |
| isJust | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| isLambdaHole | Agda.Syntax.Notation |
| isLeft | Agda.Utils.Either |
| IsLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isLiterate | Agda.Interaction.Options |
| isNatish | Agda.Compiler.Epic.NatDetection |
| isNeutral | Agda.TypeChecking.MetaVars.Occurs |
| isNewerThan | Agda.Interaction.Imports |
| IsNofix | Agda.Utils.List |
| IsNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNothing | |
| 1 (Function) | Agda.Utils.Maybe |
| 2 (Function) | Agda.Utils.Maybe.Strict |
| isntTypeConf | Agda.TypeChecking.Test.Generators |
| isOperator | |
| 1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| iSourceHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsPrefix | Agda.Utils.List |
| isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| IsPrefixOf | Agda.TypeChecking.Abstract |
| isPrefixOf | Agda.TypeChecking.Abstract |
| isProblemSolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| isProjectionButNotCoinductive | Agda.Termination.Monad |
| isProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| IsProjElim | Agda.Syntax.Internal |
| isProjElim | Agda.Syntax.Internal |
| IsProjP | Agda.Syntax.Abstract |
| isProjP | Agda.Syntax.Abstract |
| isProperProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| isRec | Agda.Compiler.Epic.NatDetection |
| IsRecord | Agda.TypeChecking.Datatypes |
| isRecord | Agda.TypeChecking.Records |
| isRecordConstructor | Agda.TypeChecking.Records |
| isRecordType | Agda.TypeChecking.Records |
| isRecursiveRecord | Agda.TypeChecking.Records |
| IsReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isRel | Agda.Compiler.Epic.Erasure |
| isRelevant | Agda.Syntax.Common |
| isRight | Agda.Utils.Either |
| isSet | Agda.Syntax.Abstract.Views |
| isSingleton | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Compiler.JS.Compiler |
| 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 |
| isSizeNameTest | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSizeNameTestRaw | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSizeProblem | Agda.TypeChecking.SizedTypes |
| isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSizeTypeTest | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSolvedProblem | Agda.TypeChecking.Rules.LHS |
| isSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isSortMeta_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isSublistOf | Agda.Utils.List |
| isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Abstract, Agda.Syntax.Internal |
| isSubscriptDigit | Agda.Utils.Suffix |
| isSubsetOf | Agda.Utils.VarSet |
| isSuccess | Agda.Utils.QuickCheck |
| IsSuffix | Agda.Utils.List |
| IsTag | Agda.Compiler.Epic.Injection |
| iStart | Agda.Syntax.Position |
| isTop | Agda.TypeChecking.SizedTypes.Utils |
| isTopLevelValue | Agda.Compiler.JS.Compiler |
| isType | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isTypeConf | Agda.TypeChecking.Test.Generators |
| isTypeEqualTo | Agda.TypeChecking.Rules.Term |
| IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isType_ | Agda.TypeChecking.Rules.Term |
| isUnicodeId | Agda.Utils.Unicode |
| isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isWellScoped | Agda.TypeChecking.Test.Generators |
| isWithFunction | Agda.Termination.Inlining |
| isZero | Agda.Utils.TestHelpers |
| isZeroNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Item | Agda.TypeChecking.Positivity |
| iterate' | Agda.Utils.Function |
| iterateUntil | Agda.Utils.Function |
| iterateUntilM | Agda.Utils.Function |