Agda-2.8.0: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - I

IApply | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
IApplyP | Agda.Syntax.Internal
IApplyVars | Agda.TypeChecking.Telescope.Path
iApplyVars | Agda.TypeChecking.Telescope.Path
IArray | Agda.Utils.IArray
iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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 | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
idFromFile | Agda.Utils.FileId, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IdiomBracketError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IdiomBracketError_ | Agda.Interaction.Options.Errors
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
IdToFile | Agda.Utils.FileId
idToFile | Agda.Utils.FileId
iEnd | Agda.Syntax.Position
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.Map1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Null
4 (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
IgnoreUnused | Agda.Compiler.ToTreeless
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
IllegalAmbiguity | Agda.Syntax.Scope.Base
IllegalDeclarationBeforeTopLevelModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalDeclarationBeforeTopLevelModule_ | Agda.Interaction.Options.Errors
IllegalDeclarationInDataDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalDeclarationInDataDefinition_ | Agda.Interaction.Options.Errors
IllegalHidingInPostfixProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalHidingInPostfixProjection_ | Agda.Interaction.Options.Errors
IllegalInstanceVariableInPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalInstanceVariableInPatternSynonym_ | Agda.Interaction.Options.Errors
IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalLetInTelescope_ | Agda.Interaction.Options.Errors
IllegalPatternInTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalPatternInTelescope_ | Agda.Interaction.Options.Errors
IllegalRewriteRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllegalRewriteRuleReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
illegalRewriteWarningName | 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
IllformedProjectionPatternAbstract_ | Agda.Interaction.Options.Errors
IllformedProjectionPatternConcrete | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllformedProjectionPatternConcrete_ | Agda.Interaction.Options.Errors
illiterate | Agda.Syntax.Parser.Literate
IllTypedPatternAfterWithAbstraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IllTypedPatternAfterWithAbstraction_ | Agda.Interaction.Options.Errors
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
ImpliedPragmaOption | Agda.Interaction.Options
impliedPragmaOptions | Agda.Interaction.Options
implies |
1 (Function) | Agda.Utils.Boolean
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver
ImpliesPragmaOption | Agda.Interaction.Options
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
ImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ImportMayOpen | Agda.Syntax.Concrete.Definitions.Errors
importModule | Agda.Utils.Haskell.Syntax
importPrimitiveModules | Agda.Interaction.Imports
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
impossibleConstructorErrorName | Agda.TypeChecking.Errors.Names
ImpossibleConstructor_ | Agda.Interaction.Options.Errors
ImpossibleError | Agda.Interaction.ExitCode
ImpossiblePragma | Agda.Syntax.Concrete
impossibleTerm | Agda.Syntax.Internal
impossibleTest | Agda.ImpossibleTest
impossibleTestReduceM | Agda.ImpossibleTest
impRenaming | Agda.Syntax.Common
ImproperInstHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ImproperInstTele | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
Incoherent | Agda.Syntax.Common
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
IncorrectTypeForRewriteRelation_ | Agda.Interaction.Options.Errors
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
index | Agda.Utils.IArray
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
indices | Agda.Utils.IArray
Indirect | Agda.TypeChecking.Monad.Base.Types, 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
inferUnivSort | Agda.TypeChecking.Sort
InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
infimum | Agda.Termination.Order
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
inform | Agda.Setup.EmacsMode
infoTau | Agda.TypeChecking.Coverage.SplitClause
infoTel | Agda.TypeChecking.Coverage.SplitClause
infoTel0 | Agda.TypeChecking.Coverage.SplitClause
Info_AllGoalsWarnings | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Auto | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_CompilationError | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_CompilationOk | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Constraints | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Context | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Error |
1 (Data Constructor) | Agda.Interaction.Response.Base, Agda.Interaction.Response
2 (Type/Class) | Agda.Interaction.Response
Info_Error_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_GenericError | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_GoalSpecific | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_HighlightingParseError | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_HighlightingScopeCheckError | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_InferredType | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Intro_ConstructorUnknown | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Intro_NotFound | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_ModuleContents | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_NormalForm | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_SearchAbout | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Time | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_Version | Agda.Interaction.Response.Base, Agda.Interaction.Response
Info_WhyInScope | Agda.Interaction.Response.Base, 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
initCommandState | Agda.Interaction.Base
initCopyInfo | Agda.Syntax.Abstract
initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initFileDict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initFreeEnv | Agda.TypeChecking.Free.Lazy
InitialCandidates | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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
initMaybe | Agda.Utils.List
initNiceState | Agda.Syntax.Concrete.Definitions.Monad
initOccursCheck | Agda.TypeChecking.MetaVars.Occurs
initPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initPersistentStateFromSessionState | 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
initSessionState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initState |
1 (Function) | Agda.Syntax.Parser.Monad
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initStateFromPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initStateFromSessionState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
initStateIO | 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
InjectiveForInferencePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
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
inRange | Agda.Utils.IArray
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.VarSet
3 (Function) | Agda.Utils.Set1
4 (Function) | Agda.Utils.Map1
5 (Function) | Agda.Utils.Bag
6 (Function) | Agda.Utils.HashTable
7 (Function) | Agda.Utils.BoolSet
8 (Function) | Agda.Utils.AssocList
9 (Function) | Agda.Utils.SmallSet
10 (Function) | Agda.Utils.Trie
11 (Function) | Agda.Utils.Favorites
12 (Function) | Agda.Utils.BiMap
13 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
14 (Function) | Agda.Termination.CallMatrix
15 (Function) | Agda.Termination.CallGraph
16 (Function) | Agda.Utils.RangeMap
insertAfter | Agda.Compiler.JS.Compiler
insertCompared | Agda.Utils.Favorites
insertDT | Agda.TypeChecking.DiscrimTree
Inserted | Agda.Syntax.Common
insertedBinder | Agda.Syntax.Abstract
InsertedBinderName | Agda.Syntax.Common
insertedBinder_ | Agda.Syntax.Abstract
insertEdge |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver
insertEdgeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
insertHiddenLambdas | Agda.TypeChecking.Rules.Term
insertImplicit | Agda.TypeChecking.Implicit
insertImplicit' | Agda.TypeChecking.Implicit
insertImplicitPatSynArgs | Agda.Syntax.Abstract
insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitPatternsT | Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitSizeLtPatterns | Agda.TypeChecking.Rules.LHS.Implicit
insertInspects | Agda.TypeChecking.Rules.Def
insertLookupWithKey |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.BiMap
insertLookupWithKeyPrecondition | Agda.Utils.BiMap
insertMap | Agda.Utils.Map1
insertMapMax | Agda.Utils.Map1
insertMapMin | Agda.Utils.Map1
insertMapWith | Agda.Utils.Map1
insertMapWithKey | Agda.Utils.Map1
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
insertSet | Agda.Utils.Set1
insertSetMax | Agda.Utils.Set1
insertSetMin | Agda.Utils.Set1
insertTrailingArgs | Agda.TypeChecking.Coverage
insertWith |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
insertWithKey | Agda.Utils.Map1
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
instanceClass | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceDef | Agda.Syntax.Common
InstanceInfo |
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
InstanceMeta | Agda.Syntax.Info
InstanceNoCandidate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoCandidate_ | Agda.Interaction.Options.Errors
InstanceNoOutputTypeName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNoOutputTypeName_ | Agda.Interaction.Options.Warnings
InstanceNotInArgumentPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceNotInArgumentPosition_ | Agda.Interaction.Options.Warnings
instanceOverlap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceP | Agda.Syntax.Concrete
InstanceProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
Instances | Agda.Utils.ProfileOptions
InstanceSearch | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InstanceSearchDepthExhausted | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceSearchDepthExhausted_ | Agda.Interaction.Options.Errors
InstanceTable |
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
InstanceWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InstanceWithExplicitArg_ | Agda.Interaction.Options.Warnings
Instantiable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Instantiate | Agda.TypeChecking.Reduce
instantiate | Agda.TypeChecking.Reduce
instantiate' | Agda.TypeChecking.Reduce
Instantiated | Agda.Interaction.Base
instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateDefinitionType | Agda.TypeChecking.Rules.Decl
InstantiateFull | Agda.TypeChecking.Reduce
instantiateFull | Agda.TypeChecking.Reduce
instantiateFull' | Agda.TypeChecking.Reduce
instantiateRewriteRule | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateRewriteRules | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
instantiateTelescope | Agda.TypeChecking.Telescope
instantiateVarHeads | Agda.TypeChecking.Injectivity
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
InteractionEmacs | Agda.Main
InteractionError |
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
interactionError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
interactionErrorName | Agda.TypeChecking.Errors.Names
interactionErrorNameString | Agda.Interaction.Options.Errors
InteractionError_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
InteractionFormat | Agda.Main
InteractionId |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
interactionId | Agda.Syntax.Common
interactionIdToMetaId | Agda.Interaction.BasicOps
interactionInteractor | Agda.Main
InteractionJson | Agda.Main
InteractionMetaBoundaries | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InteractionMetaBoundaries_ | Agda.Interaction.Options.Warnings
InteractionOutputCallback | Agda.TypeChecking.Monad.Base, Agda.Interaction.Response, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Types, 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
InterfaceInstantiateFull | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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
InternalError_ | Agda.Interaction.Options.Errors
interpret | Agda.Interaction.InteractionTop
intersection |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.BoolSet
5 (Function) | Agda.Utils.SmallSet
intersectionWith | Agda.Utils.Map1
intersectionWithKey | Agda.Utils.Map1
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
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
InvalidBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidBuiltin_ | Agda.Interaction.Options.Errors
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
InvalidConstructorBlock | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidConstructorBlock_ | Agda.Interaction.Options.Warnings
InvalidCoverageCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidCoverageCheckPragma_ | Agda.Interaction.Options.Warnings
InvalidDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidDisplayForm_ | Agda.Interaction.Options.Warnings
InvalidDottedExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidDottedExpression_ | Agda.Interaction.Options.Errors
InvalidExtensionError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
InvalidFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidFileNameReason | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidFileName_ | Agda.Interaction.Options.Errors
InvalidInstanceHeadType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidInstanceHeadType_ | Agda.Interaction.Options.Errors
InvalidMeasureMutual | Agda.Syntax.Concrete.Definitions.Errors
InvalidMeasureMutual_ | Agda.Interaction.Options.Errors
InvalidModalTelescopeUse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidModalTelescopeUse_ | Agda.Interaction.Options.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
InvalidPattern_ | Agda.Interaction.Options.Errors
InvalidProjectionParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidProjectionParameter_ | Agda.Interaction.Options.Errors
InvalidPun | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidPun_ | Agda.Interaction.Options.Errors
InvalidTerminationCheckPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
InvalidTerminationCheckPragma_ | Agda.Interaction.Options.Warnings
InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
InvalidTypeSort_ | Agda.Interaction.Options.Errors
Invariant | Agda.TypeChecking.Monad.Base.Types, 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
inverseApplyPolarity | Agda.Syntax.Common
inverseApplyQuantity | Agda.Syntax.Common
inverseApplyRelevance | Agda.Syntax.Common
inverseCompose | Agda.Utils.POMonoid
inverseComposeCohesion | Agda.Syntax.Common
inverseComposeModality | Agda.Syntax.Common
inverseComposePolarity | Agda.Syntax.Common
inverseComposePolarity' | 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
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.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, 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
irrelevant | Agda.Syntax.Common
irrelevantToShapeIrrelevant | 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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
isBenchmarkOn | Agda.Utils.Benchmark
isBinder | Agda.Syntax.Notation
isBinderP | Agda.Syntax.Concrete
isBinderUsed | Agda.TypeChecking.Free
isBlocked | Agda.TypeChecking.Reduce
isBlockedTerm | Agda.TypeChecking.MetaVars
isBlockingConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsBool | Agda.Utils.Boolean
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 |
1 (Type/Class) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isBuiltinModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsBuiltinModuleWithSafePostulates | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isBuiltinModuleWithSafePostulates | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common
isConstructor | Agda.TypeChecking.Datatypes
isContinuous | Agda.Syntax.Common
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 |
1 (Data Constructor) | Agda.Utils.Set1
2 (Data Constructor) | Agda.Utils.Map1
3 (Data Constructor) | 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.Base, 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
isEtaRecordConstructor | Agda.TypeChecking.Records
isEtaRecordDef | Agda.TypeChecking.Records
isEtaRecordType | Agda.TypeChecking.Records
isEtaVar | Agda.TypeChecking.Records
isExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsExpr |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Concrete.Operators.Parser
isExtendedLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsIApply | Agda.TypeChecking.Coverage.Match
iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isIncoherent | Agda.Syntax.Common
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.Syntax.Common, Agda.Compiler.Common, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Common, 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
isNoAbs | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
IsNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend
isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Concrete, Agda.Syntax.Abstract, Agda.Compiler.Backend
IsNonEmpty |
1 (Data Constructor) | Agda.Utils.Set1
2 (Data Constructor) | Agda.Utils.Map1
isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
iso | Agda.Utils.Lens
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
isOverlapping | 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.Common
isPattern | Agda.Syntax.Concrete
IsPatternSynonym | Agda.Syntax.Common
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.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isPrimitiveModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProblemCompletelySolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProblemSolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProblemSolved' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
isProjectionButNotCoinductive | Agda.Termination.Monad
isProjection_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsProjElim | Agda.Syntax.Internal.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
isProp | Agda.Syntax.Internal
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
isProperSubmapOf | Agda.Utils.Map1
isProperSubmapOfBy | Agda.Utils.Map1
isProperSubsetOf | Agda.Utils.Set1
isPropM | Agda.TypeChecking.Irrelevance
isQName | Agda.Interaction.BasicOps
isQualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isQuantity0 | Agda.Syntax.Common
isQuantityAttribute | Agda.Syntax.Concrete.Attribute
isQuantityω | Agda.Syntax.Common
isReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsRecord | Agda.Syntax.Internal
isRecord | Agda.TypeChecking.Records
isRecordConstructor |
1 (Function) | Agda.Syntax.Scope.Monad
2 (Function) | Agda.TypeChecking.Records
IsRecordModule | Agda.Syntax.Scope.Base
isRecordType | Agda.TypeChecking.Records
IsRecord_ | Agda.Syntax.Internal
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
isShapeIrrelevant | Agda.Syntax.Common
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
isSourceCodeWarning | Agda.TypeChecking.Monad.Base, 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
isSubmapOf | Agda.Utils.Map1
isSubmapOfBy | Agda.Utils.Map1
isSubscriptDigit | Agda.Utils.Suffix
isSubsetOf |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.BoolSet
isSurrogateCodePoint | Agda.Utils.Char
isTacticAttribute | Agda.Syntax.Concrete.Attribute
iStart | Agda.Syntax.Position
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
isWithFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
IsWithP | Agda.Syntax.Concrete.Pattern
isWithP | Agda.Syntax.Concrete.Pattern
isWithPattern | Agda.Syntax.Concrete.Pattern
isYesOverlap | Agda.Syntax.Common
isZeroNode | Agda.TypeChecking.SizedTypes.WarshallSolver
itableCounts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
itableTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.IArray, Agda.Utils.SmallSet
ixmap | Agda.Utils.IArray
IZero | Agda.Syntax.Internal