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.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
Ident | Agda.Syntax.Concrete |
identifier | Agda.Syntax.Parser.LexActions |
identity | Agda.Utils.TestHelpers |
IdentP | Agda.Syntax.Concrete |
idP | Agda.Utils.Permutation |
IdPart | Agda.Syntax.Notation |
idSub | Agda.TypeChecking.Substitute |
iEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop |
If | Agda.Compiler.Epic.AuxAST |
ifM | Agda.Utils.Monad |
IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
ignoreBlocking | Agda.Syntax.Internal |
ignoreForced | Agda.Syntax.Common |
ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ihname | Agda.Compiler.MAlonzo.Misc |
iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IM | Agda.Interaction.Monad |
iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ImpInsert | Agda.TypeChecking.Implicit |
impInsert | Agda.TypeChecking.Implicit |
ImplicitInsertion | Agda.TypeChecking.Implicit |
ImplicitP | Agda.Syntax.Abstract |
Import | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
ImportDirective | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
importDirRange | Agda.Syntax.Concrete |
ImportedModule | Agda.Syntax.Concrete |
ImportedName | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
importedName | Agda.Syntax.Concrete |
importedNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
ImportedNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
ImportPragma | Agda.Syntax.Concrete |
imports | Agda.Compiler.MAlonzo.Compiler |
importsForPrim | Agda.Compiler.MAlonzo.Primitives |
IMPOSSIBLE | 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 |
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 |
InDefOf | Agda.TypeChecking.Positivity |
indent | Agda.Utils.String |
Independence | Agda.Interaction.GhciTop |
independence | Agda.Interaction.GhciTop |
Independent | Agda.Interaction.GhciTop |
Index | |
1 (Data Constructor) | Agda.Utils.Suffix |
2 (Type/Class) | Agda.Termination.CallGraph |
IndexFreeInParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IndexVariablesNotDistinct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IndicesNotConstructorApplications | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Induction | Agda.Syntax.Common |
Inductive | Agda.Syntax.Common |
inductiveCheck | Agda.TypeChecking.Rules.Builtin |
Inf | Agda.Syntax.Internal |
InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inferDef | Agda.TypeChecking.Rules.Term |
InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
inferHead | Agda.TypeChecking.Rules.Term |
infertypevar | Agda.Auto.CaseSplit |
InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
infimum | Agda.Termination.CallGraph |
Infinite | Agda.Utils.Warshall |
infinite | Agda.Utils.Warshall |
Infix | Agda.Syntax.Concrete |
InfixDef | Agda.Syntax.Common |
infixlP | Agda.Syntax.Concrete.Operators.Parser |
infixP | Agda.Syntax.Concrete.Operators.Parser |
infixrP | Agda.Syntax.Concrete.Operators.Parser |
Info | Agda.Syntax.Info |
infodecl | Agda.Compiler.MAlonzo.Compiler |
infoOnException | Agda.Interaction.GhciTop |
initCompileState | Agda.Compiler.Epic.CompileState |
initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
initGraph | Agda.Utils.Warshall |
initiate | Agda.Compiler.Epic.Erasure |
initMapS | Agda.Auto.Convert |
initMeta | Agda.Auto.NarrowingSearch |
initState | |
1 (Function) | Agda.Syntax.Parser.Monad |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
3 (Function) | Agda.Interaction.GhciTop |
Inline | Agda.Compiler.Epic.AuxAST |
inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
inNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
InScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
InScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
inScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
insert | |
1 (Function) | Agda.Utils.Graph |
2 (Function) | Agda.Utils.Trie |
3 (Function) | Agda.Termination.CallGraph |
insertImplicit | Agda.TypeChecking.Implicit |
insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit |
insertPatterns | Agda.TypeChecking.Rules.Def |
insertTele | Agda.Compiler.Epic.Forcing |
insertWithKeyM | Agda.Utils.Map |
InsideOperandCtx | Agda.Syntax.Fixity |
insideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
Instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
Instantiated | Agda.Interaction.BasicOps |
instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
InstantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
instantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
instantiatePattern | Agda.TypeChecking.Rules.LHS |
instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate |
inState | Agda.Syntax.Parser.LexActions |
InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
int | Agda.Utils.Pretty |
integer | Agda.Utils.Pretty |
integerSemiring | Agda.Termination.Semiring |
Interaction | |
1 (Type/Class) | Agda.Interaction.GhciTop |
2 (Data Constructor) | Agda.Interaction.GhciTop |
interaction | Agda.Interaction.CommandLine.CommandLine |
InteractionId | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
interactionLoop | Agda.Interaction.CommandLine.CommandLine |
InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
intersectWith | Agda.Termination.SparseMatrix |
Interval | |
1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
intervalInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop |
intMap | Agda.Utils.Warshall |
introTactic | Agda.Interaction.BasicOps |
Inv | Agda.TypeChecking.Injectivity |
InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inverseScopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
inverseScopeLookupModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
inverseScopeLookupName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
invertP | Agda.Utils.Permutation |
InvView | Agda.TypeChecking.Injectivity |
io | Agda.TypeChecking.Primitive |
IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iotapossmeta | Agda.Auto.Typecheck |
iotastep | Agda.Auto.Typecheck |
ioTCM | Agda.Interaction.GhciTop |
ioTCM_ | Agda.Interaction.GhciTop |
iPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Irr | Agda.Compiler.Epic.Erasure |
irrBranch | Agda.Compiler.Epic.ConstructorIrrelevancy |
Irrelevant | Agda.Syntax.Common |
irrelevant | Agda.Syntax.Common |
IrrelevantDatatype | Agda.TypeChecking.Coverage |
irrExpr | Agda.Compiler.Epic.ConstructorIrrelevancy |
IrrFilter | Agda.Compiler.Epic.CompileState |
irrFilter | Agda.Compiler.Epic.ConstructorIrrelevancy |
irrFilters | Agda.Compiler.Epic.CompileState |
irrFun | Agda.Compiler.Epic.ConstructorIrrelevancy |
IsAbstract | Agda.Syntax.Common |
isAHole | Agda.Syntax.Notation |
isBelow | Agda.Utils.Warshall |
isBindingHole | Agda.Syntax.Notation |
isBlockedTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
isCoinductive | Agda.TypeChecking.Rules.Data |
iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isDatatype | |
1 (Function) | Agda.TypeChecking.Datatypes |
2 (Function) | Agda.TypeChecking.Coverage |
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isEmpty | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Termination.SparseMatrix |
3 (Function) | Agda.Termination.Matrix |
IsEmptyType | Agda.Interaction.BasicOps |
isEmptyType | Agda.TypeChecking.Empty |
isEmptyTypeC | Agda.TypeChecking.Empty |
isEtaExpandable | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
isEtaRecord | Agda.TypeChecking.Records |
IsExpr | Agda.Syntax.Concrete.Operators.Parser |
isGeneratedRecordConstructor | Agda.TypeChecking.Records |
isHaskellKind | Agda.Compiler.HaskellTypes |
isHiddenArg | Agda.Syntax.Common |
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
isIn | Agda.Compiler.Epic.Forcing |
isInCase | Agda.Compiler.Epic.Forcing |
isIndependent | Agda.Interaction.GhciTop |
IsInfix | Agda.Syntax.Common |
isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
isInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
isInTerm | Agda.Compiler.Epic.Forcing |
isIrr | Agda.Compiler.Epic.Erasure |
isJust | Agda.Utils.Maybe |
isLambdaHole | Agda.Syntax.Notation |
isLeft | Agda.Utils.Either |
isLevelConstraint | Agda.TypeChecking.UniversePolymorphism |
isLiterate | Agda.Interaction.Options |
isNewerThan | Agda.Interaction.Imports |
isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isNothing | Agda.Utils.Maybe |
isntTypeConf | Agda.TypeChecking.Test.Generators |
isOperator | |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
isRec | Agda.Compiler.Epic.NatDetection |
isRecord | Agda.TypeChecking.Records |
isRecordConstructor | Agda.TypeChecking.Records |
IsReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isRel | Agda.Compiler.Epic.Erasure |
isRight | Agda.Utils.Either |
isSingleton | Agda.Termination.SparseMatrix |
isSingletonRecord | Agda.TypeChecking.Records |
isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
isSolvedProblem | Agda.TypeChecking.Rules.LHS |
IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
isString | Agda.Utils.Generics |
isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
isSuccess | Agda.Utils.QuickCheck |
iStart | Agda.Syntax.Position, Agda.Interaction.GhciTop |
isType | Agda.TypeChecking.Rules.Term |
IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isTypeConf | Agda.TypeChecking.Test.Generators |
IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isType_ | Agda.TypeChecking.Rules.Term |
isUnicodeId | Agda.Utils.Unicode |
isVar | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
isWellScoped | Agda.TypeChecking.Test.Generators |
isZero | Agda.Utils.TestHelpers |
Item | Agda.TypeChecking.Positivity |
iterate' | Agda.Utils.Function |