Agda-2.6.2.2: 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
iBuiltin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
Id |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
iDefaultPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
iEnd | Agda.Syntax.Position
If |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
3 (Type/Class) | Agda.Utils.TypeLevel
ifBlocked | Agda.TypeChecking.Reduce
ifDirty | Agda.Utils.Update
iFilePragmaOptions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iFileType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
ifNotPi | 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.Compiler.Backend, Agda.TypeChecking.Monad
ifPath | Agda.TypeChecking.Rules.Term
ifPi | Agda.TypeChecking.Telescope
ifPiType | Agda.TypeChecking.Telescope
ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIsOr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iFullHash | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IgnoreAbstract | Agda.Interaction.Base
IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ignoreAbstractMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad
IgnoreSorts | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
iHighlighting | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ihname | Agda.Compiler.MAlonzo.Misc
iImportedModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iImportWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iInsideScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ilam | Agda.TypeChecking.Names
iLength | Agda.Syntax.Position
IllegalLetInTelescope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllegalPatternInTelescope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllformedAsClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IllformedAsClause_ | Agda.Interaction.Options.Warnings
IllformedProjectionPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
illiterate | Agda.Syntax.Parser.Literate
IM | Agda.Interaction.Monad
IMax | Agda.Syntax.Internal
imax | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
IMin | Agda.Syntax.Internal
imin | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
imoduleMap | Agda.Syntax.Scope.Monad
iModuleName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ImpInsert | Agda.TypeChecking.Implicit
implicitArgs | Agda.TypeChecking.Implicit
ImplicitFlex | Agda.TypeChecking.Rules.LHS.Problem
ImplicitInsertion | Agda.TypeChecking.Implicit
implicitNamedArgs | Agda.TypeChecking.Implicit
implicitP | Agda.TypeChecking.Rules.LHS.Implicit
implies | Agda.TypeChecking.SizedTypes.WarshallSolver
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 |
1 (Function) | Agda.Compiler.JS.Syntax
2 (Function) | Agda.Compiler.MAlonzo.Compiler
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Interaction.Highlighting.Precise
inConcreteMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
inConcreteOrAbstractMode | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
indexWithDefault | Agda.Utils.List
Indirect | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Induction |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Concrete
Inductive | Agda.Syntax.Common
INeg | Agda.Syntax.Internal
Inf | Agda.Syntax.Internal
inf | Agda.TypeChecking.Positivity
InfectiveImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InfectiveImport_ | Agda.Interaction.Options.Warnings
infectiveOptions | Agda.Interaction.Options
infer | Agda.TypeChecking.CheckInternal
inferApplication | Agda.TypeChecking.Rules.Application
InferDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InferExpr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
inferExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker
inferExpr' | Agda.TypeChecking.Rules.Term
inferExprForWith | Agda.TypeChecking.Rules.Term
inferFunSort | Agda.TypeChecking.Sort
inferMeta | Agda.TypeChecking.Rules.Term
inferPiSort | Agda.TypeChecking.Sort
Inferred | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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
infodecl | Agda.Compiler.MAlonzo.Compiler
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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
initCCEnv | Agda.Compiler.MAlonzo.Compiler
initCommandState | Agda.Interaction.Base
initCopyInfo | Agda.Syntax.Abstract
initEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initExpRefInfo | Agda.Auto.SearchControl
initFreeEnv | Agda.TypeChecking.Free.Lazy
initGraph | Agda.Utils.Warshall
initialiseCommandQueue | Agda.Interaction.InteractionTop
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
initNiceEnv | Agda.Syntax.Concrete.Definitions.Monad
initOccursCheck | Agda.TypeChecking.MetaVars.Occurs
initPersistentState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initPostScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initPreScopeState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
inits | Agda.Utils.List1
initState |
1 (Function) | Agda.Syntax.Parser.Monad
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
initWithDefault | Agda.Utils.List
InjectivePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
Injectivity | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InlinePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
InlineReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InMutual |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types
inMutualBlock | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
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.Bag
3 (Function) | Agda.Utils.SmallSet
4 (Function) | Agda.Utils.Trie
5 (Function) | Agda.Utils.BiMap
6 (Function) | Agda.Utils.RangeMap
7 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
8 (Function) | Agda.Utils.Favorites
9 (Function) | Agda.Utils.AssocList
10 (Function) | Agda.Termination.CallMatrix
11 (Function) | Agda.Termination.CallGraph
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
insertMissingFields | Agda.TypeChecking.Records
insertMissingFieldsFail | Agda.TypeChecking.Records
insertMissingFieldsWarn | Agda.TypeChecking.Records
insertMutualBlockInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
InsideOperandCtx | Agda.Syntax.Fixity
Instance | Agda.Syntax.Common
InstanceArg | Agda.Syntax.Concrete
InstanceArgV | Agda.Syntax.Concrete.Operators.Parser
InstanceArgWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
InstanceNoOutputTypeName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceNoOutputTypeName_ | Agda.Interaction.Options.Warnings
InstanceP | Agda.Syntax.Concrete
InstanceSearch | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
InstanceSearchDepthExhausted | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceTable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceWithExplicitArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InstanceWithExplicitArg_ | Agda.Interaction.Options.Warnings
Instantiable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Instantiate | Agda.TypeChecking.Reduce
instantiate | Agda.TypeChecking.Reduce
instantiate' | Agda.TypeChecking.Reduce
Instantiated | Agda.Interaction.Base
instantiateDef | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateDefinitionType | Agda.TypeChecking.Rules.Decl
InstantiateFull | Agda.TypeChecking.Reduce
instantiateFull | Agda.TypeChecking.Reduce
instantiateFull' | Agda.TypeChecking.Reduce
instantiateFullExceptForDefinitions | Agda.TypeChecking.Reduce
instantiateFullExceptForDefinitions' | Agda.TypeChecking.Reduce
instantiateRewriteRule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateRewriteRules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
instantiateTelescope | Agda.TypeChecking.Telescope
instantiateVarHeads | Agda.TypeChecking.Injectivity
inState | Agda.Syntax.Parser.LexActions
InstV | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Int | Agda.Utils.Haskell.Syntax
int |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Compiler.Treeless.EliminateLiteralPatterns
Integer | Agda.Compiler.JS.Syntax
integer |
1 (Function) | Agda.Utils.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
InteractionOutputCallback | Agda.Interaction.Response
InteractionPoint |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Interactive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Interactor | Agda.Main
interAssocWith | Agda.Termination.SparseMatrix
interestingCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
interestingConstraint | Agda.TypeChecking.Pretty.Constraint
Interface |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
InternalError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
internalError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
interpret | Agda.Interaction.InteractionTop
intersection |
1 (Function) | Agda.Utils.VarSet
2 (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
intervalsToRange | Agda.Syntax.Position
intervalToRange | Agda.Syntax.Position
intervalUnview | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
intervalUnview' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
IntervalView | Agda.Syntax.Internal
intervalView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
intervalView' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
IntervalWithoutFile | Agda.Syntax.Position
intFilePath | Agda.Interaction.FindFile
intMap | Agda.Utils.Warshall
inTopContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
Intro | Agda.Interaction.InteractionTop
intros | Agda.Compiler.MAlonzo.Compiler
introTactic | Agda.Interaction.BasicOps
intSemiring | Agda.Termination.Semiring
IntSet | Agda.Utils.IntSet.Infinite
intSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
InvalidTypeSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Invariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
invariant |
1 (Function) | Agda.Utils.IntSet.Infinite
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
Inverse | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
InversionDepthReached_ | Agda.Interaction.Options.Warnings
InversionMap | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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, Agda.TypeChecking.Primitive.Base
IOException | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IOne | Agda.Syntax.Internal
iOptionsUsed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
iPatternSyns | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbEquations | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbMetaApp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPBoundary |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPBoundary' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbOverapplied | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipbValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcBoundary | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClauseNo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcClosure | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPClause |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcQName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipcWithSub | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipMeta | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IPNoClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ipSolved | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Irrelevant | Agda.Syntax.Common
irrToNonStrict | Agda.Syntax.Common
IsAbstract | Agda.Syntax.Common
isAbsurdBody | Agda.Syntax.Internal
isAbsurdLambdaName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isAbsurdP | Agda.Syntax.Concrete
isAbsurdPatternName | Agda.Syntax.Internal
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
isBinderP | Agda.Syntax.Concrete
isBinderUsed | Agda.TypeChecking.Free
isBindingHole | Agda.Syntax.Notation
isBlocked | Agda.TypeChecking.Reduce
isBlockedTerm | Agda.TypeChecking.MetaVars
isBounded | Agda.TypeChecking.SizedTypes
isBoundedProjVar | Agda.TypeChecking.SizedTypes
isBoundedSizeType | Agda.TypeChecking.SizedTypes
isBuiltin | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
isBuiltinModule | Agda.Interaction.Options.Lenses
isBuiltinModuleWithSafePostulates | Agda.Interaction.Options.Lenses
isBuiltinNoDef | Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
isCanonical | Agda.TypeChecking.Conversion
isClosed | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
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
isCopatternLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
iScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isCovered | Agda.TypeChecking.Coverage
IsData |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
IsEllipsis | Agda.Syntax.Concrete.Pattern
isEllipsis | Agda.Syntax.Concrete.Pattern
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isEmpty |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Termination.SparseMatrix
isEmptyFunction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
IsExpr | Agda.Syntax.Concrete.Operators.Parser
isExtendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IsFam | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
IsFibrant |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | 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.Compiler.Backend, Agda.TypeChecking.Monad
isForced | Agda.TypeChecking.Forcing
IsFree | Agda.TypeChecking.Free.Reduce
isFrozen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isFullyInstantiatedMeta | Agda.TypeChecking.Reduce
isFunName | Agda.Syntax.Concrete.Definitions.Types
isGeneralizableMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isGeneratedRecordConstructor | Agda.TypeChecking.Records
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IsIApply | Agda.TypeChecking.Coverage.Match
iSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isImported | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
IsInstance | Agda.Syntax.Common
isInstance | Agda.Syntax.Common
isInstanceConstraint | Agda.TypeChecking.InstanceArguments
IsInstantiatedMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInstantiatedMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInstantiatedMeta' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isInteractionMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.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
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
IsLHS | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isLocal | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad
IsMain |
1 (Type/Class) | Agda.Compiler.Backend, Agda.Compiler.Common
2 (Data Constructor) | Agda.Compiler.Backend, Agda.Compiler.Common
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
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
isNormalHole | Agda.Syntax.Notation
IsNot | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
isNothing |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
IsNotLock | Agda.Syntax.Common
isolatedNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
isOpenMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad
iSourceHash | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isOverlappable | Agda.Syntax.Common
isPath | Agda.TypeChecking.Telescope
IsPathCons | Agda.TypeChecking.Rules.Data
isPathType | Agda.Syntax.Internal
IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isPattern | Agda.Syntax.Concrete
isPosInf | Agda.Utils.Float
isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPosZero | Agda.Utils.Float
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
isPrimitiveModule | Agda.Interaction.Options.Lenses
isProblemSolved | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
isProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isProjectionButNotCoinductive | Agda.Termination.Monad
isProjection_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad
isProperProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad
IsRecord |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS
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.Compiler.Backend, Agda.TypeChecking.Monad
isReduced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isRelevanceAttribute | Agda.Syntax.Concrete.Attribute
isRelevant | Agda.Syntax.Common
isRelevantProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
isRelevantProjection_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeNameTestRaw | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeProblem | Agda.TypeChecking.SizedTypes
IsSizeType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSizeTypeTest | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
isSmallSort | Agda.TypeChecking.Substitute
isSolvingConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
IsSort | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isSort | Agda.Syntax.Internal
isSortMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isSortMeta_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
isStaticFun | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
IsStrict | 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.SmallSet
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.Compiler.Backend, Agda.TypeChecking.Monad
isType | Agda.TypeChecking.Rules.Term
isType' | Agda.TypeChecking.Rules.Term
IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isTypeEqualTo | Agda.TypeChecking.Rules.Term
IsType_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
isType_ | Agda.TypeChecking.Rules.Term
isUnderscore | Agda.Syntax.Common
isUnguarded | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
isUnnamed | Agda.Syntax.Common
isUnqualified | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend
isUnsolvedWarning | Agda.TypeChecking.Warnings
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 | 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
iUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
IVar | Agda.Utils.Haskell.Syntax
iWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Ix | Agda.Utils.SmallSet
IZero | Agda.Syntax.Internal