iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ICArgList | Agda.Auto.Syntax |
ICExp | Agda.Auto.Syntax |
icnvh | Agda.Auto.Convert |
icode | Agda.TypeChecking.Serialise.Base |
icode0 | Agda.TypeChecking.Serialise.Base |
icode0' | Agda.TypeChecking.Serialise.Base |
icode1 | Agda.TypeChecking.Serialise.Base |
icode1' | Agda.TypeChecking.Serialise.Base |
icode10 | Agda.TypeChecking.Serialise.Base |
icode10' | Agda.TypeChecking.Serialise.Base |
icode11 | Agda.TypeChecking.Serialise.Base |
icode11' | Agda.TypeChecking.Serialise.Base |
icode12 | Agda.TypeChecking.Serialise.Base |
icode12' | Agda.TypeChecking.Serialise.Base |
icode13 | Agda.TypeChecking.Serialise.Base |
icode13' | Agda.TypeChecking.Serialise.Base |
icode14 | Agda.TypeChecking.Serialise.Base |
icode14' | Agda.TypeChecking.Serialise.Base |
icode15 | Agda.TypeChecking.Serialise.Base |
icode2 | Agda.TypeChecking.Serialise.Base |
icode2' | Agda.TypeChecking.Serialise.Base |
icode3 | Agda.TypeChecking.Serialise.Base |
icode3' | Agda.TypeChecking.Serialise.Base |
icode4 | Agda.TypeChecking.Serialise.Base |
icode4' | Agda.TypeChecking.Serialise.Base |
icode5 | Agda.TypeChecking.Serialise.Base |
icode5' | Agda.TypeChecking.Serialise.Base |
icode6 | Agda.TypeChecking.Serialise.Base |
icode6' | Agda.TypeChecking.Serialise.Base |
icode7 | Agda.TypeChecking.Serialise.Base |
icode7' | Agda.TypeChecking.Serialise.Base |
icode8 | Agda.TypeChecking.Serialise.Base |
icode8' | Agda.TypeChecking.Serialise.Base |
icode9 | Agda.TypeChecking.Serialise.Base |
icode9' | Agda.TypeChecking.Serialise.Base |
icodeDouble | Agda.TypeChecking.Serialise.Base |
icodeInteger | Agda.TypeChecking.Serialise.Base |
icodeMemo | Agda.TypeChecking.Serialise.Base |
icodeN | 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 | |
1 (Function) | Agda.Utils.TestHelpers |
2 (Function) | Agda.Termination.Termination |
Ident | Agda.Syntax.Concrete |
identifier | |
1 (Function) | Agda.Syntax.Parser.LexActions |
2 (Function) | Agda.Compiler.JS.Parser |
identity | Agda.Utils.TestHelpers |
IdentP | Agda.Syntax.Concrete |
iDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
idP | Agda.Utils.Permutation |
IdPart | Agda.Syntax.Notation |
IdS | Agda.Syntax.Internal, 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 |
ifDirty | Agda.Utils.Update |
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 |
ifNotPi | Agda.TypeChecking.Telescope |
ifNotPiType | Agda.TypeChecking.Telescope |
ifNull | Agda.Utils.Null |
ifNullM | Agda.Utils.Null |
ifPi | Agda.TypeChecking.Telescope |
ifPiType | Agda.TypeChecking.Telescope |
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 | |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
ignoreBlocking | Agda.Syntax.Internal |
ignoreForced | |
1 (Function) | Agda.Syntax.Common |
2 (Function) | Agda.Compiler.Epic.Erasure |
IgnoreInAnnotations | |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
IgnoreNot | |
1 (Data Constructor) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
2 (Data Constructor) | Agda.TypeChecking.Free.Old |
ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ignoreSharing | Agda.Syntax.Internal |
ignoreSharingType | Agda.Syntax.Internal |
IgnoreSorts | |
1 (Type/Class) | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
2 (Type/Class) | Agda.TypeChecking.Free.Old |
iHaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iHaskellImportsUHC | 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 |
IllformedProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Interaction.Monad |
imapClauseBody | Agda.Syntax.Internal |
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.TypeChecking.Rules.LHS.Implicit |
implies | Agda.TypeChecking.SizedTypes.WarshallSolver |
Import | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
3 (Data Constructor) | Agda.Syntax.Abstract |
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.Compiler.Epic.CompileState |
ImportedName | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
ImportedName' | Agda.Syntax.Common |
ImportedNS | Agda.Syntax.Scope.Base |
ImportPragma | Agda.Syntax.Concrete |
imports | Agda.Compiler.MAlonzo.Compiler |
importsForPrim | Agda.Compiler.MAlonzo.Primitives |
ImportUHCPragma | Agda.Syntax.Concrete |
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 |
impRenaming | Agda.Syntax.Common |
imp_dir | Agda.Syntax.Parser.Lexer |
In | Agda.Syntax.Concrete.Operators.Parser |
inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
inc | Agda.Utils.Warshall |
InClause | Agda.TypeChecking.Positivity |
includes | Agda.TypeChecking.Serialise.Base |
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 |
IncompletePattern | Agda.Interaction.Highlighting.Precise |
IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
inConcreteOrAbstractMode | 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 |
infer | Agda.TypeChecking.CheckInternal |
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.TheTypeChecker |
inferExpr' | Agda.TypeChecking.Rules.Term |
inferExprForWith | Agda.TypeChecking.Rules.Term |
inferHead | Agda.TypeChecking.Rules.Term |
inferHeadDef | Agda.TypeChecking.Rules.Term |
inferMeta | Agda.TypeChecking.Rules.Term |
Inferred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
InfixNotation | Agda.Syntax.Notation |
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_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 |
Infty | Agda.TypeChecking.SizedTypes.Syntax |
initCCEnv | Agda.Compiler.MAlonzo.Compiler |
initCommandState | Agda.Interaction.InteractionTop |
initCompileState | Agda.Compiler.Epic.CompileState |
initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
initFreeEnv | Agda.TypeChecking.Free.Lazy |
initGraph | Agda.Utils.Warshall |
initialDotState | Agda.Interaction.Highlighting.Dot |
initialIFSCandidates | 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 |
initPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
initPreScopeState | 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.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
Inline | Agda.Compiler.Epic.AuxAST |
InlinePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
InlineReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inlineWithClauses | Agda.Termination.Inlining |
inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
inNameSpace | Agda.Syntax.Scope.Base |
inOriginalContext | Agda.TypeChecking.Unquote |
inputFlag | Agda.Interaction.Options |
InScope | 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.HashMap |
2 (Function) | Agda.Utils.BiMap |
3 (Function) | Agda.Utils.Bag |
4 (Function) | Agda.Utils.Favorites |
5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
6 (Function) | Agda.Utils.Trie |
7 (Function) | Agda.Utils.AssocList |
8 (Function) | Agda.Termination.CallMatrix |
9 (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 |
insertHiddenLambdas | Agda.TypeChecking.Rules.Term |
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 |
insertImplicitSizeLtPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
insertMissingFields | Agda.TypeChecking.Records |
insertOldInteractionScope | Agda.Interaction.InteractionTop |
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 |
insidePi | Agda.TypeChecking.InstanceArguments |
Instance | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Auto.Syntax |
InstanceArg | Agda.Syntax.Concrete |
InstanceArgV | Agda.Syntax.Concrete.Operators.Parser |
InstanceB | Agda.Syntax.Concrete |
InstanceDef | Agda.Syntax.Common |
InstanceP | Agda.Syntax.Concrete |
InstanceTable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate |
instantiateTelescope | Agda.TypeChecking.Telescope |
inState | Agda.Syntax.Parser.LexActions |
InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
InsufficientCoverage | Agda.Utils.QuickCheck |
int | Agda.Utils.Pretty |
Integer | Agda.Compiler.JS.Syntax |
integer | Agda.Utils.Pretty |
integerC | Agda.TypeChecking.Serialise.Base |
integerD | Agda.TypeChecking.Serialise.Base |
integerE | Agda.TypeChecking.Serialise.Base |
integerSemiring | Agda.Termination.Semiring |
Interaction | Agda.Interaction.InteractionTop |
interaction | Agda.Interaction.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 |
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 | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
intersectionWith | Agda.Utils.HashMap |
intersectionWithKey | 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 |
intervalsToRange | Agda.Syntax.Position |
IntervalWithoutFile | Agda.Syntax.Position |
intLit | Agda.Compiler.JS.Parser |
intMap | Agda.Utils.Warshall |
inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
Intro | Agda.Interaction.InteractionTop |
intro1 | Agda.TypeChecking.Telescope |
intros | Agda.Compiler.MAlonzo.Compiler |
introTactic | Agda.Interaction.BasicOps |
intSemiring | Agda.Termination.Semiring |
intView | Agda.Syntax.Treeless |
Inv | Agda.TypeChecking.Injectivity |
InvalidCatchallPragma | Agda.Syntax.Concrete.Definitions |
InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions |
InvalidName | Agda.Syntax.Concrete.Definitions |
InvalidNoPositivityCheckPragma | Agda.Syntax.Concrete.Definitions |
InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions |
InvalidType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
inverseApplyRelevance | Agda.TypeChecking.Irrelevance |
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 |
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 |
IORef | Agda.Utils.IORef |
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 | |
1 (Data Constructor) | Agda.TypeChecking.Free.Old |
2 (Data Constructor) | Agda.TypeChecking.Free |
irrelevantOrUnused | Agda.Syntax.Common |
irrelevantVars | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
irrToNonStrict | Agda.Syntax.Common |
IsAbstract | Agda.Syntax.Common |
isAbsurdBody | Agda.Syntax.Internal |
isAbsurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isAbsurdPatternName | Agda.Syntax.Internal |
isAHole | Agda.Syntax.Notation |
isAlias | Agda.TypeChecking.Rules.Def |
IsAlpha | Agda.Utils.Char |
IsAlphaNum | Agda.Utils.Char |
isAnonymousModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
isApplyElim | Agda.Syntax.Internal |
isBelow | Agda.Utils.Warshall |
isBinderUsed | |
1 (Function) | Agda.TypeChecking.Free.Old |
2 (Function) | Agda.TypeChecking.Free |
isBindingHole | Agda.Syntax.Notation |
isBlockedTerm | Agda.TypeChecking.MetaVars |
IsBothfix | Agda.Utils.List |
isBounded | Agda.TypeChecking.SizedTypes |
isBuiltin | Agda.TypeChecking.Primitive |
isClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
isCoinductive | Agda.TypeChecking.Rules.Data |
isCoinductiveProjection | Agda.Termination.Monad |
isCon | Agda.TypeChecking.Unquote |
IsControl | Agda.Utils.Char |
isCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
IsData | Agda.TypeChecking.Datatypes |
isDataOrRecord | Agda.TypeChecking.Datatypes |
isDataOrRecordType | Agda.TypeChecking.Datatypes |
isDatatype | Agda.TypeChecking.Datatypes |
isDatatypeModule | Agda.Syntax.Scope.Monad |
isDecr | Agda.Termination.Order |
isDef | Agda.TypeChecking.Unquote |
isDefaultImportDir | Agda.Syntax.Common |
IsDigit | Agda.Utils.Char |
IsDominated | Agda.Utils.Favorites |
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isEmpty | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Termination.SparseMatrix |
isEmptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isEmptyObject | Agda.Compiler.JS.Compiler |
IsEmptyType | Agda.Interaction.BasicOps |
isEmptyType | Agda.TypeChecking.Empty |
isEqualityType | Agda.Syntax.Internal |
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 |
IsExpr | Agda.Syntax.Concrete.Operators.Parser |
IsFlexiblePattern | Agda.TypeChecking.Rules.LHS |
isFlexiblePattern | Agda.TypeChecking.Rules.LHS |
isFlexNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
isFrozen | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
isGeneratedRecordConstructor | Agda.TypeChecking.Records |
isHackReifyToMeta | Agda.Syntax.Internal |
IsHexDigit | Agda.Utils.Char |
isHidden | Agda.Syntax.Common |
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isIFSConstraint | Agda.TypeChecking.InstanceArguments |
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 |
isInlineFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
isInsideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
IsInstance | Agda.Syntax.Common |
IsInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, 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 |
isInt | Agda.Compiler.UHC.FromAgda |
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 |
IsLetter | Agda.Utils.Char |
IsLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
isLiterate | Agda.Interaction.Options |
IsLower | Agda.Utils.Char |
IsMacro | Agda.Syntax.Common |
IsMain | |
1 (Type/Class) | Agda.Compiler.Common |
2 (Data Constructor) | Agda.Compiler.Common |
IsMark | Agda.Utils.Char |
isModuleFreeVar | Agda.TypeChecking.Rules.Term |
isNameInScope | Agda.Syntax.Scope.Base |
isNat | Agda.Compiler.UHC.FromAgda |
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.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Concrete, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isNormalHole | Agda.Syntax.Notation |
isNothing | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
isntTypeConf | Agda.TypeChecking.Test.Generators |
IsNumber | Agda.Utils.Char |
IsOctDigit | Agda.Utils.Char |
isOperator | |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, 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 |
IsPrint | Agda.Utils.Char |
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 |
IsPunctuation | Agda.Utils.Char |
isQName | Agda.Interaction.BasicOps |
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 |
isRigid | Agda.TypeChecking.InstanceArguments |
IsSeparator | Agda.Utils.Char |
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 |
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 |
IsSpace | Agda.Utils.Char |
isStaticFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
isSublistOf | Agda.Utils.List |
isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Abstract, Agda.Syntax.Internal |
isSubscriptDigit | Agda.Utils.Suffix |
isSubsetOf | Agda.Utils.VarSet |
isSuccess | Agda.Utils.QuickCheck |
IsSuffix | Agda.Utils.List |
IsSymbol | Agda.Utils.Char |
IsTag | Agda.Compiler.Epic.Injection |
iStart | Agda.Syntax.Position |
isTop | Agda.TypeChecking.SizedTypes.Utils |
isTopLevelValue | Agda.Compiler.JS.Compiler |
isTrivialMPattern | Agda.TypeChecking.Coverage.Match |
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 |
isUnderscore | Agda.Syntax.Common |
isUnreachable | Agda.Syntax.Treeless |
isUntypedBuiltin | Agda.TypeChecking.Rules.Builtin |
IsUpper | Agda.Utils.Char |
isVar | Agda.TypeChecking.CompiledClause.Compile |
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 |
iterWhile | Agda.Utils.Function |