IApply | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
IApplyP | Agda.Syntax.Internal |
IApplyVars | Agda.TypeChecking.Telescope.Path |
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 |
ICOption | Agda.Interaction.Options |
icOptionActive | Agda.Interaction.Options |
icOptionDescription | Agda.Interaction.Options |
icOptionKind | Agda.Interaction.Options |
icOptionOK | Agda.Interaction.Options |
icOptionWarning | Agda.Interaction.Options |
Id | |
1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Auto.Syntax |
iDefaultPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
idempotent | Agda.Termination.Termination |
Ident | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
identifier | Agda.Syntax.Parser.LexActions |
IdentP | Agda.Syntax.Concrete |
IdiomBrackets | Agda.Syntax.Concrete |
IdiomType | Agda.Syntax.Internal |
iDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
idP | Agda.Utils.Permutation |
IdPart | Agda.Syntax.Common |
IdS | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
idS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
idViewAsPath | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iEnd | Agda.Syntax.Position |
If | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Type/Class) | Agda.Utils.TypeLevel |
3 (Data Constructor) | Agda.Compiler.JS.Syntax |
ifBlocked | Agda.TypeChecking.Reduce |
ifDirty | Agda.Utils.Update |
iFilePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iFileType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ifIsSort | Agda.TypeChecking.Sort |
ifJust | Agda.Utils.Maybe |
ifJustM | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
ifLe | Agda.TypeChecking.SizedTypes.Syntax |
ifM | Agda.Utils.Monad |
ifNoConstraints | Agda.TypeChecking.Constraints |
ifNoConstraints_ | Agda.TypeChecking.Constraints |
ifNotM | Agda.Utils.Monad |
ifNotNull | |
1 (Function) | Agda.Utils.Null |
2 (Function) | Agda.Utils.List1 |
ifNotNullM | Agda.Utils.Null |
ifNotPathB | Agda.TypeChecking.Telescope |
ifNotPi | Agda.TypeChecking.Telescope |
ifNotPiOrPathB | Agda.TypeChecking.Telescope |
ifNotPiOrPathType | Agda.TypeChecking.Telescope |
ifNotPiType | Agda.TypeChecking.Telescope |
ifNotSort | Agda.TypeChecking.Sort |
ifNull | |
1 (Function) | Agda.Utils.Null |
2 (Function) | Agda.Utils.List1 |
ifNullM | Agda.Utils.Null |
iForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ifPath | Agda.TypeChecking.Telescope |
ifPathB | Agda.TypeChecking.Telescope |
ifPi | Agda.TypeChecking.Telescope |
ifPiB | Agda.TypeChecking.Telescope |
ifPiOrPathB | Agda.TypeChecking.Telescope |
ifPiType | Agda.TypeChecking.Telescope |
ifPiTypeB | Agda.TypeChecking.Telescope |
ifThenElse | Agda.Utils.Boolean |
ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ifTopLevelAndHighlightingLevelIsOr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iFullHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IgnoreAbstract | Agda.Interaction.Base |
IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IgnoreAll | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
ignoreBlocking | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
IgnoreInAnnotations | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
IgnoreNot | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IgnoreSorts | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ihname | Agda.Compiler.MAlonzo.Misc |
iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iImportWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IInfo | Agda.TypeChecking.Coverage.SplitClause |
iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ilam | Agda.TypeChecking.Names |
iLength | Agda.Syntax.Position |
Illegal | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse, Agda.TypeChecking.Rules.LHS.Unify |
IllegalDeclarationInDataDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllegalHidingInPostfixProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllegalPatternInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllegalRewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllegalRewriteRuleReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllformedAsClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllformedAsClause_ | Agda.Interaction.Options.Warnings |
IllformedProjectionPatternAbstract | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IllformedProjectionPatternConcrete | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
illiterate | Agda.Syntax.Parser.Literate |
IllTypedPatternAfterWithAbstraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IM | Agda.Interaction.Monad |
IMax | Agda.Syntax.Internal |
imax | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
iMetaBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IMin | Agda.Syntax.Internal |
imin | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
imoduleMap | Agda.Syntax.Scope.Monad |
iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ImpInsert | Agda.TypeChecking.Implicit |
implicitArgs | Agda.TypeChecking.Implicit |
ImplicitFlex | Agda.TypeChecking.Rules.LHS.Problem |
ImplicitInsertion | Agda.TypeChecking.Implicit |
implicitNamedArgs | Agda.TypeChecking.Implicit |
implicitP | Agda.TypeChecking.Rules.LHS.Implicit |
implies | |
1 (Function) | Agda.Utils.Boolean |
2 (Function) | 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 |
importPrimitives | Agda.Syntax.Translation.ConcreteToAbstract |
importQualified | Agda.Utils.Haskell.Syntax |
ImportS | Agda.Syntax.Abstract |
imports | Agda.Compiler.JS.Syntax |
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 |
impossible | Agda.Utils.Impossible |
ImpossibleConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ImpossibleError | Agda.Interaction.ExitCode |
ImpossiblePragma | Agda.Syntax.Concrete |
impossibleTerm | Agda.Syntax.Internal |
impossibleTest | Agda.ImpossibleTest |
impossibleTestReduceM | 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 |
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
inConcreteOrAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IncorrectTypeForRewriteRelation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IncorrectTypeForRewriteRelationReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
increase | Agda.Termination.Order |
inCxt | Agda.TypeChecking.Names |
IndArgType | Agda.TypeChecking.Positivity.Occurrence |
InDefOf | Agda.TypeChecking.Positivity.Occurrence |
Indent | Agda.Compiler.JS.Pretty |
indent | |
1 (Function) | Agda.Utils.String |
2 (Function) | Agda.Compiler.JS.Pretty |
indentBy | Agda.Compiler.JS.Pretty |
independent | Agda.Interaction.InteractionTop |
Index | |
1 (Type/Class) | Agda.Utils.IndexedList |
2 (Data Constructor) | Agda.Utils.Suffix |
IndexedClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IndexedClauseArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
indexWithDefault | Agda.Utils.List |
Indirect | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Induction | |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Concrete |
InductionAndEta | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Inductive | Agda.Syntax.Common.Aspect, Agda.Syntax.Common |
INeg | Agda.Syntax.Internal |
ineg | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
Inf | Agda.Syntax.Internal |
inf | Agda.TypeChecking.Positivity |
infallibleSortKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Infective | Agda.Interaction.Options |
InfectiveCoinfective | Agda.Interaction.Options |
InfectiveCoinfectiveOption | Agda.Interaction.Options |
infectiveCoinfectiveOptions | Agda.Interaction.Options |
InfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InfectiveImport_ | Agda.Interaction.Options.Warnings |
infer | Agda.TypeChecking.CheckInternal |
inferApplication | Agda.TypeChecking.Rules.Application |
InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
inferExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
inferExpr' | Agda.TypeChecking.Rules.Term |
inferExprForWith | Agda.TypeChecking.Rules.Term |
inferFunSort | Agda.TypeChecking.Sort |
inferInternal | Agda.TypeChecking.CheckInternal |
inferInternal' | Agda.TypeChecking.CheckInternal |
inferMeta | Agda.TypeChecking.Rules.Term |
inferNeutral | Agda.TypeChecking.ProjectionLike |
inferPiSort | Agda.TypeChecking.Sort |
Inferred | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
inferredBlock | Agda.Syntax.Concrete.Definitions.Types |
inferredChecks | Agda.Syntax.Concrete.Definitions.Types |
inferredLeftovers | Agda.Syntax.Concrete.Definitions.Types |
InferredMutual | |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
inferSpine | Agda.TypeChecking.CheckInternal |
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 |
infoEqLHS | Agda.TypeChecking.Coverage.SplitClause |
infoEqRHS | Agda.TypeChecking.Coverage.SplitClause |
infoEqTel | Agda.TypeChecking.Coverage.SplitClause |
infoLeftInv | Agda.TypeChecking.Coverage.SplitClause |
infoRho | Agda.TypeChecking.Coverage.SplitClause |
infoTau | Agda.TypeChecking.Coverage.SplitClause |
infoTel | Agda.TypeChecking.Coverage.SplitClause |
infoTel0 | Agda.TypeChecking.Coverage.SplitClause |
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 |
InfS | Agda.Syntax.Reflected |
Infty | Agda.TypeChecking.SizedTypes.Syntax |
init | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.List2 |
init1 | Agda.Utils.List |
initAutoOptions | Agda.Auto.Options |
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 |
initialiseCommandQueue | Agda.Interaction.InteractionTop |
initialMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
initLast | |
1 (Function) | Agda.Utils.List |
2 (Function) | Agda.Utils.List1 |
initLast1 | Agda.Utils.List |
initLHSState | Agda.TypeChecking.Rules.LHS.ProblemRest |
initMapS | Agda.Auto.Convert |
initMaybe | Agda.Utils.List |
initMeta | Agda.Auto.NarrowingSearch |
initNiceState | Agda.Syntax.Concrete.Definitions.Monad |
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 |
inits | Agda.Utils.List1 |
inits1 | Agda.Utils.List1 |
initState | |
1 (Function) | Agda.Syntax.Parser.Monad |
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
initUnifyState | Agda.TypeChecking.Rules.LHS.Unify.Types |
initWithDefault | Agda.Utils.List |
injectAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
injectConstructor | Agda.TypeChecking.Rules.LHS.Unify.Types |
injectDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types |
injectIndices | Agda.TypeChecking.Rules.LHS.Unify.Types |
InjectivePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
Injectivity | |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
injectParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
injectType | Agda.TypeChecking.Rules.LHS.Unify.Types |
InlineNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InlineNoExactSplit_ | Agda.Interaction.Options.Warnings |
InlinePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
InlineReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InMutual | |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types |
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types |
inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
inNameSpace | Agda.Syntax.Scope.Base |
inOriginalContext | Agda.TypeChecking.Unquote |
inplaceS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
inputFlag | Agda.Interaction.Options |
InScope | |
1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Scope.Base |
inScopeBecause | Agda.Syntax.Scope.Base |
InScopeSet | Agda.Syntax.Scope.Base |
InScopeTag | Agda.Syntax.Scope.Base |
inScopeTag | Agda.Syntax.Scope.Base |
InSeq | |
1 (Type/Class) | Agda.Compiler.Treeless.Subst |
2 (Data Constructor) | Agda.Compiler.Treeless.Subst |
inSeq | Agda.Compiler.Treeless.Subst |
insert | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.HashTable |
3 (Function) | Agda.Utils.BoolSet |
4 (Function) | Agda.Utils.Bag |
5 (Function) | Agda.Utils.SmallSet |
6 (Function) | Agda.Utils.Trie |
7 (Function) | Agda.Utils.BiMap |
8 (Function) | Agda.Utils.Favorites |
9 (Function) | Agda.Utils.AssocList |
10 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
11 (Function) | Agda.Termination.CallMatrix |
12 (Function) | Agda.Termination.CallGraph |
13 (Function) | Agda.Utils.RangeMap |
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 |
insertImplicitBindersT | Agda.TypeChecking.Implicit |
insertImplicitBindersT1 | 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 |
insertInspects | Agda.TypeChecking.Rules.Def |
insertLookupWithKey | Agda.Utils.BiMap |
insertLookupWithKeyPrecondition | Agda.Utils.BiMap |
insertMetaSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
insertMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
insertMissingFields | Agda.TypeChecking.Records |
insertMissingFieldsFail | Agda.TypeChecking.Records |
insertMissingFieldsWarn | Agda.TypeChecking.Records |
insertMutualBlockInfo | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
insertNames | Agda.TypeChecking.Rules.Def |
insertOldInteractionScope | Agda.Interaction.InteractionTop |
insertPatterns | Agda.TypeChecking.Rules.Def |
insertPatternsLHSCore | Agda.TypeChecking.Rules.Def |
insertPrecondition | Agda.Utils.BiMap |
insertTrailingArgs | Agda.TypeChecking.Coverage |
insertWith | |
1 (Function) | Agda.Utils.Trie |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
insideAndOutside | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
insideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InsideOperandCtx | Agda.Syntax.Fixity |
Instance | Agda.Syntax.Common |
InstanceArg | Agda.Syntax.Concrete |
InstanceArgV | Agda.Syntax.Concrete.Operators.Parser |
InstanceArgWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InstanceArgWithExplicitArg_ | Agda.Interaction.Options.Warnings |
InstanceB | Agda.Syntax.Concrete |
InstanceBlock | Agda.Syntax.Concrete.Definitions.Types |
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 |
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 |
instantiateFullExceptForDefinitions | Agda.TypeChecking.Reduce |
instantiateRewriteRule | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
instantiateRewriteRules | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
instantiateTelescope | Agda.TypeChecking.Telescope |
instantiateVarHeads | Agda.TypeChecking.Injectivity |
instantiateWhen | Agda.TypeChecking.Reduce |
Instantiation | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
inState | Agda.Syntax.Parser.LexActions |
instBody | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
instTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Int | Agda.Utils.Haskell.Syntax |
int | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.Compiler.Treeless.EliminateLiteralPatterns |
Integer | Agda.Compiler.JS.Syntax |
integer | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.Syntax.Parser.LexActions |
integerC | Agda.TypeChecking.Serialise.Base |
integerD | Agda.TypeChecking.Serialise.Base |
integerE | Agda.TypeChecking.Serialise.Base |
integerSemiring | Agda.Termination.Semiring |
integerToChar | Agda.Utils.Char |
Interaction | Agda.Interaction.Base |
Interaction' | Agda.Interaction.Base |
InteractionId | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
interactionId | Agda.Syntax.Common |
interactionIdToMetaId | Agda.Interaction.BasicOps |
InteractionMetaBoundaries | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InteractionMetaBoundaries_ | Agda.Interaction.Options.Warnings |
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 | |
1 (Data Constructor) | Agda.Utils.ProfileOptions |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Interactor | Agda.Main |
interAssocWith | Agda.Termination.SparseMatrix |
interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
interestingConstraint | Agda.TypeChecking.Pretty.Constraint |
Interface | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InterfaceFile | Agda.Interaction.FindFile |
InterleavedData | Agda.Syntax.Concrete.Definitions.Types |
interleavedDataCons | Agda.Syntax.Concrete.Definitions.Types |
InterleavedDecl | Agda.Syntax.Concrete.Definitions.Types |
interleavedDecl | Agda.Syntax.Concrete.Definitions.Types |
interleavedDeclNum | Agda.Syntax.Concrete.Definitions.Types |
interleavedDeclSig | Agda.Syntax.Concrete.Definitions.Types |
InterleavedFun | Agda.Syntax.Concrete.Definitions.Types |
interleavedFunClauses | Agda.Syntax.Concrete.Definitions.Types |
InterleavedMutual | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types |
interleaveRanges | Agda.Syntax.Position |
Internal | Agda.Utils.ProfileOptions |
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.BoolSet |
3 (Function) | Agda.Utils.SmallSet |
intersectVars | Agda.TypeChecking.Conversion |
intersectWith | Agda.Termination.SparseMatrix |
intersperse | Agda.Utils.List1 |
Interval | |
1 (Type/Class) | Agda.Syntax.Position |
2 (Data Constructor) | Agda.Syntax.Position |
interval | Agda.Syntax.Parser.Literate |
Interval' | Agda.Syntax.Position |
intervalInvariant | Agda.Syntax.Position |
intervalSort | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
intervalsToRange | Agda.Syntax.Position |
intervalToRange | Agda.Syntax.Position |
IntervalUniv | Agda.Syntax.Internal |
intervalUnview | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
intervalUnview' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IntervalView | Agda.Syntax.Internal |
intervalView | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
intervalView' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IntervalWithoutFile | Agda.Syntax.Position |
intFilePath | Agda.Interaction.FindFile |
intMap | Agda.Utils.Warshall |
inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Intro | Agda.Interaction.InteractionTop |
introTactic | Agda.Interaction.BasicOps |
intSemiring | Agda.Termination.Semiring |
IntSet | Agda.Utils.IntSet.Infinite |
intSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
intToDouble | Agda.Utils.Float |
intView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Inv | Agda.TypeChecking.Injectivity |
InvalidCatchallPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidCatchallPragma_ | Agda.Interaction.Options.Warnings |
InvalidCharacterLiteral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InvalidCharacterLiteral_ | Agda.Interaction.Options.Warnings |
InvalidConstructor | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidConstructorBlock | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidConstructorBlock_ | Agda.Interaction.Options.Warnings |
InvalidConstructor_ | Agda.Interaction.Options.Warnings |
InvalidCoverageCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidCoverageCheckPragma_ | Agda.Interaction.Options.Warnings |
InvalidExtensionError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions.Errors |
InvalidName | Agda.Syntax.Concrete.Definitions.Errors |
InvalidNoPositivityCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidNoPositivityCheckPragma_ | Agda.Interaction.Options.Warnings |
InvalidNoUniverseCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidNoUniverseCheckPragma_ | Agda.Interaction.Options.Warnings |
InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InvalidProjectionParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InvalidRecordDirective | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
InvalidRecordDirective_ | Agda.Interaction.Options.Warnings |
InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, 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 |
inverseApplyModalityButNotQuantity | 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 |
inverseScopeLookupModule | Agda.Syntax.Scope.Base |
inverseScopeLookupModule' | Agda.Syntax.Scope.Base |
inverseScopeLookupName | Agda.Syntax.Scope.Base |
inverseScopeLookupName' | Agda.Syntax.Scope.Base |
inverseScopeLookupName'' | Agda.Syntax.Scope.Base |
inverseSubst' | Agda.TypeChecking.MetaVars |
InversionDepthReached | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
InversionDepthReached_ | Agda.Interaction.Options.Warnings |
InversionMap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Invert | Agda.Syntax.Common |
InvertExcept | Agda.TypeChecking.MetaVars |
invertFunction | Agda.TypeChecking.Injectivity |
invertP | Agda.Utils.Permutation |
invLookup | Agda.Utils.BiMap |
InvView | Agda.TypeChecking.Injectivity |
io | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IOne | Agda.Syntax.Internal |
iOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iOpaqueNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iOptionsUsed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IORef | 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 |
IPBoundary | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipBoundary | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IPBoundary' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcClauseNo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IPClause | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcQName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipcWithSub | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IPFace' | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IPNoClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ipSolved | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Irrelevant | Agda.Syntax.Common |
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 |
isAccessibleDef | Agda.TypeChecking.Opacity |
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.Elim, Agda.Syntax.Internal |
isApplyElim' | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
IsBase | Agda.Utils.TypeLevel |
IsBasicRangeMap | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
isBelow | Agda.Utils.Warshall |
isBenchmarkOn | Agda.Utils.Benchmark |
isBinder | Agda.Syntax.Notation |
isBinderP | Agda.Syntax.Concrete |
isBinderUsed | Agda.TypeChecking.Free |
isBlocked | Agda.TypeChecking.Reduce |
isBlockedTerm | Agda.TypeChecking.MetaVars |
IsBool | Agda.Utils.Boolean |
isBoundaryConstraint | Agda.TypeChecking.Pretty.Warning |
isBounded | Agda.TypeChecking.SizedTypes |
isBoundedProjVar | Agda.TypeChecking.SizedTypes |
isBoundedSizeType | Agda.TypeChecking.SizedTypes |
IsBuiltin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isBuiltin | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
isBuiltinModule | Agda.Interaction.Options.Lenses |
isBuiltinModuleWithSafePostulates | Agda.Interaction.Options.Lenses |
isBuiltinNoDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isCanonical | Agda.TypeChecking.Conversion |
isClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isCode | Agda.Syntax.Parser.Literate |
isCodeLayer | Agda.Syntax.Parser.Literate |
isCoFibrantSort | Agda.TypeChecking.Irrelevance |
isCoinductive | Agda.TypeChecking.Rules.Data |
isCoinductiveProjection | Agda.Termination.Monad |
isCon | Agda.TypeChecking.Unquote |
isConName | Agda.Syntax.Scope.Base |
isConstructor | Agda.TypeChecking.Datatypes |
isCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isCovered | Agda.TypeChecking.Coverage |
isCubicalSubtype | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
IsData | Agda.Syntax.Internal |
IsDataModule | Agda.Syntax.Scope.Base |
isDataOrRecord | Agda.TypeChecking.Datatypes |
isDataOrRecordType | Agda.TypeChecking.Datatypes |
isDatatype | Agda.TypeChecking.Datatypes |
isDatatypeModule | Agda.Syntax.Scope.Monad |
isDebugPrinting | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isDecr | Agda.Termination.Order |
isDef | Agda.TypeChecking.Unquote |
isDefAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
isDefaultImportDir | Agda.Syntax.Common |
isDefName | Agda.Syntax.Scope.Base |
IsDominated | Agda.Utils.Favorites |
isDontExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsEllipsis | Agda.Syntax.Concrete.Pattern |
isEllipsis | Agda.Syntax.Concrete.Pattern |
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isEmpty | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.Termination.SparseMatrix |
isEmptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isEmptyObject | Agda.Compiler.JS.Compiler |
isEmptyTel | Agda.TypeChecking.Empty |
IsEmptyType | Agda.Interaction.Base |
isEmptyType | Agda.TypeChecking.Empty |
isEnabled | Agda.Compiler.Backend |
isEqualityType | Agda.Syntax.Internal |
isErasable | Agda.Compiler.Treeless.Erase |
isErased | Agda.Syntax.Common |
isEtaCon | Agda.TypeChecking.Records |
isEtaExpandable | Agda.TypeChecking.MetaVars |
isEtaOrCoinductiveRecordConstructor | Agda.TypeChecking.Records |
isEtaRecord | Agda.TypeChecking.Records |
isEtaRecordType | Agda.TypeChecking.Records |
isEtaVar | Agda.TypeChecking.Records |
isExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsExpr | Agda.Syntax.Concrete.Operators.Parser |
isExtendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isFaceConstraint | Agda.TypeChecking.MetaVars |
IsFam | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
IsFibrant | |
1 (Type/Class) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
isFibrant | Agda.TypeChecking.Irrelevance |
isFlexible | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
IsFlexiblePattern | Agda.TypeChecking.Rules.LHS |
isFlexiblePattern | Agda.TypeChecking.Rules.LHS |
isFlexNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
IsForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isForced | Agda.TypeChecking.Forcing |
IsFree | Agda.TypeChecking.Free.Reduce |
isFrozen | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isFunName | Agda.Syntax.Concrete.Definitions.Types |
isGeneralizableMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
IsIndex | Agda.TypeChecking.Positivity.Occurrence |
isInductiveRecord | Agda.TypeChecking.Records |
IsInfix | Agda.Syntax.Common |
isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isInftyNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
isInlineFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isInsertedHidden | Agda.Syntax.Common |
isInsideDotPattern | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsInstance | Agda.Syntax.Common |
isInstance | Agda.Syntax.Common |
isInstanceConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.TypeChecking.InstanceArguments, Agda.Compiler.Backend |
IsInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isInstantiatedMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isInteractionMetaB | Agda.TypeChecking.MetaVars |
isInterleavedData | Agda.Syntax.Concrete.Definitions.Types |
isInterleavedFun | Agda.Syntax.Concrete.Definitions.Types |
isInternalAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
isInterval | Agda.TypeChecking.Telescope.Path |
isIOne | Agda.Syntax.Internal |
isIrrelevant | Agda.Syntax.Common |
isIrrelevantOrPropM | Agda.TypeChecking.Irrelevance |
isJust | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
isLabeled | Agda.Syntax.Concrete.Pretty |
isLambdaHole | Agda.Syntax.Notation |
isLambdaNotation | Agda.Syntax.Notation |
isLeChildModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isLeft | Agda.Utils.Either |
isLeParentModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isLevelType | Agda.TypeChecking.Level |
isLevelUniverseEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsList | Agda.Utils.List1 |
isLocal | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsLock | Agda.Syntax.Common |
isLtChildModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isLtParentModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
IsMacro | Agda.Syntax.Common |
isMacro | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsMain | |
1 (Type/Class) | Agda.Compiler.Common, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.Compiler.Common, Agda.Compiler.Backend |
IsMeta | Agda.TypeChecking.Reduce |
isMeta | Agda.TypeChecking.Reduce |
isMetaTCWarning | Agda.TypeChecking.Warnings |
isMetaWarning | Agda.TypeChecking.Warnings |
isModChar | Agda.Compiler.MAlonzo.Misc |
isModuleAccount | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
isModuleFreeVar | Agda.TypeChecking.Rules.Term |
isName | Agda.Interaction.BasicOps |
isNameInScope | Agda.Syntax.Scope.Base |
isNameInScopeUnqualified | Agda.Syntax.Scope.Base |
isNameOfUniv | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isNegInf | Agda.Utils.Float |
isNegZero | Agda.Utils.Float |
isNeutral | Agda.TypeChecking.MetaVars.Occurs |
isNewerThan | Agda.Utils.FileName |
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 |
IsNot | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
isNothing | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
IsNotLock | Agda.Syntax.Common |
isolatedNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
IsOpaque | Agda.Syntax.Common |
isOpenMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isOpenMixfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isOperator | |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
3 (Function) | Agda.Compiler.MAlonzo.Pretty |
isOrder | Agda.Termination.Order |
iSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iSourceHash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isOverlappable | Agda.Syntax.Common |
isPath | Agda.TypeChecking.Telescope |
IsPathCons | Agda.TypeChecking.Rules.Data |
isPathCons | Agda.TypeChecking.Datatypes |
isPathType | Agda.Syntax.Internal |
IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isPattern | Agda.Syntax.Concrete |
isPosInf | Agda.Utils.Float |
isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isPosZero | Agda.Utils.Float |
isPragma | Agda.Syntax.Concrete |
isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
IsPrefixOf | Agda.TypeChecking.Abstract |
isPrefixOf | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.TypeChecking.Abstract |
isPrimEq | Agda.Syntax.Treeless, Agda.Compiler.Backend |
isPrimitive | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isPrimitiveModule | Agda.Interaction.Options.Lenses |
isProblemSolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isProjectionButNotCoinductive | Agda.Termination.Monad |
isProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsProjElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
isProjElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
IsProjP | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isProjP | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
isPropEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isProperApplyElim | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
isProperProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isPropM | Agda.TypeChecking.Irrelevance |
isQName | Agda.Interaction.BasicOps |
isQualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isQuantityAttribute | Agda.Syntax.Concrete.Attribute |
isReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsRecord | Agda.Syntax.Internal |
isRecord | Agda.TypeChecking.Records |
isRecordConstructor | Agda.TypeChecking.Records |
isRecordDirective | Agda.Syntax.Concrete |
IsRecordModule | Agda.Syntax.Scope.Base |
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 |
isRelevantProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isRelevantProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isRemoteMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isRight | Agda.Utils.Either |
isSafeInteger | Agda.Utils.Float |
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 |
isSmallSort | Agda.TypeChecking.Substitute |
isSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isSort | Agda.Syntax.Internal |
isSortJudgement | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isSortMeta_ | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isStaticFun | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IsStrict | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
isStrictDataSort | Agda.Syntax.Internal |
isStronglyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
isSublistOf | Agda.Utils.List |
isSubscriptDigit | Agda.Utils.Suffix |
isSubsetOf | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.BoolSet |
isSurrogateCodePoint | Agda.Utils.Char |
isTacticAttribute | Agda.Syntax.Concrete.Attribute |
iStart | Agda.Syntax.Position |
isTimeless | Agda.TypeChecking.Lock |
isTop | Agda.TypeChecking.SizedTypes.Utils |
isTopLevelValue | Agda.Compiler.JS.Compiler |
isTrivialPattern | Agda.TypeChecking.Coverage.Match |
isTwoLevelEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isType | Agda.TypeChecking.Rules.Term |
isType' | Agda.TypeChecking.Rules.Term |
IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isTypeEqualTo | Agda.TypeChecking.Rules.Term |
IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
isType_ | Agda.TypeChecking.Rules.Term |
isUnderscore | Agda.Syntax.Common |
isUnguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
isUnifyStateSolved | Agda.TypeChecking.Rules.LHS.Unify.Types |
isUnnamed | Agda.Syntax.Common |
isUnqualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
isUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend |
isUnsolvedWarning | Agda.TypeChecking.Warnings |
isUnstableDef | Agda.TypeChecking.Injectivity |
isUntypedBuiltin | Agda.TypeChecking.Rules.Builtin |
isValidJSIdent | Agda.Compiler.JS.Pretty |
isVar | Agda.TypeChecking.CompiledClause.Compile |
IsVarSet | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
isWeaklyRigid | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free |
IsWithP | Agda.Syntax.Concrete.Pattern |
isWithP | Agda.Syntax.Concrete.Pattern |
isWithPattern | Agda.Syntax.Concrete.Pattern |
isZeroNode | Agda.TypeChecking.SizedTypes.WarshallSolver |
Item | |
1 (Type/Class) | Agda.Utils.List1, Agda.Utils.List1 |
2 (Type/Class) | Agda.TypeChecking.Positivity |
iterate | Agda.Utils.List1 |
iterate' | Agda.Utils.Function |
iterateSolver | Agda.TypeChecking.SizedTypes.WarshallSolver |
iterateUntil | Agda.Utils.Function |
iterateUntilM | Agda.Utils.Function |
iterWhile | Agda.Utils.Function |
iTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
iUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
IVar | Agda.Utils.Haskell.Syntax |
iWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Ix | Agda.Utils.SmallSet |
IZero | Agda.Syntax.Internal |