Agda-2.3.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

iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ICArgList | Agda.Auto.Syntax
ICExp | Agda.Auto.Syntax
icnvh | Agda.Auto.Convert
Id |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
Ident | Agda.Syntax.Concrete
identifier |
1 (Function) | Agda.Compiler.JS.Parser
2 (Function) | Agda.Syntax.Parser.LexActions
identity | Agda.Utils.TestHelpers
IdentP | Agda.Syntax.Concrete
idP | Agda.Utils.Permutation
IdPart | Agda.Syntax.Notation
IdS | Agda.TypeChecking.Substitute
idS | Agda.TypeChecking.Substitute
iEnd | Agda.Syntax.Position
If |
1 (Data Constructor) | Agda.Compiler.JS.Syntax
2 (Data Constructor) | Agda.Compiler.Epic.AuxAST
ifBlock | Agda.Compiler.JS.Parser
ifBlocked | Agda.TypeChecking.Reduce
ifBlockedType | Agda.TypeChecking.Reduce
ifClean | Agda.TypeChecking.Rules.LHS.Unify
ifM | Agda.Utils.Monad
ifNoConstraints | Agda.TypeChecking.Constraints
ifNoConstraints_ | Agda.TypeChecking.Constraints
IFSNoCandidateInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ifTopLevelAndHighlightingLevelIs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ignoreBlocking | Agda.Syntax.Internal
ignoreForced |
1 (Function) | Agda.TypeChecking.Irrelevance
2 (Function) | Agda.Compiler.Epic.Erasure
ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreSharing | Agda.Syntax.Internal
ignoreSharingType | Agda.Syntax.Internal
iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihname | Agda.Compiler.MAlonzo.Misc
iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IM | Agda.Interaction.Monad
iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsert | Agda.TypeChecking.Implicit
impInsert | Agda.TypeChecking.Implicit
implicitArgs | Agda.TypeChecking.Implicit
ImplicitInsertion | Agda.TypeChecking.Implicit
ImplicitP | Agda.Syntax.Abstract
Import |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
ImportDirective |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
importDirRange | Agda.Syntax.Concrete
ImportedModule | Agda.Syntax.Concrete
importedModules | Agda.Compiler.Epic.CompileState
ImportedName |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
importedName | Agda.Syntax.Concrete
ImportedNS | Agda.Syntax.Scope.Base
ImportPragma | Agda.Syntax.Concrete
imports | Agda.Compiler.MAlonzo.Compiler
importsForPrim | Agda.Compiler.MAlonzo.Primitives
IMPOSSIBLE | Agda.Compiler.Epic.AuxAST
Impossible |
1 (Type/Class) | Agda.Utils.Impossible
2 (Data Constructor) | Agda.Utils.Impossible
ImpossiblePragma | Agda.Syntax.Concrete
impossibleTerm | Agda.Syntax.Internal
impossibleTest | Agda.ImpossibleTest
imp_dir | Agda.Syntax.Parser.Lexer
inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inc | Agda.Utils.Warshall
InClause | Agda.TypeChecking.Positivity
IncompletePattern | Agda.Interaction.Highlighting.Precise
IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
increase | Agda.Termination.CallGraph
IndArgType | Agda.TypeChecking.Positivity
InDefOf | Agda.TypeChecking.Positivity
indent | Agda.Utils.String
independent | Agda.Interaction.InteractionTop
Index |
1 (Data Constructor) | Agda.Utils.Suffix
2 (Type/Class) | Agda.Termination.CallGraph
IndexVariablesNotDistinct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesFreeInParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesNotConstructorApplications | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Indirect | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Induction | Agda.Syntax.Common
Inductive | Agda.Syntax.Common
Inf | Agda.Syntax.Internal
inf | Agda.TypeChecking.Positivity
inferable | Agda.Compiler.Epic.Smashing
inferableTerm | Agda.Compiler.Epic.Smashing
InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferDef | Agda.TypeChecking.Rules.Term
InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker
inferExprForWith | Agda.TypeChecking.Rules.Term
inferHead | Agda.TypeChecking.Rules.Term
inferMeta | Agda.TypeChecking.Rules.Term
inferOrCheck | Agda.TypeChecking.Rules.Term
infertypevar | Agda.Auto.CaseSplit
InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
infimum | Agda.Termination.CallGraph
Infinite | Agda.Utils.Warshall
infinite | Agda.Utils.Warshall
Infix | Agda.Syntax.Concrete
InfixDef | Agda.Syntax.Common
infixlP | Agda.Syntax.Concrete.Operators.Parser
infixP | Agda.Syntax.Concrete.Operators.Parser
infixrP | Agda.Syntax.Concrete.Operators.Parser
Info | Agda.Syntax.Info
infodecl | Agda.Compiler.MAlonzo.Compiler
Info_AllGoals | Agda.Interaction.Response
Info_Auto | Agda.Interaction.Response
Info_CompilationOk | Agda.Interaction.Response
Info_Constraints | Agda.Interaction.Response
Info_Context | Agda.Interaction.Response
Info_CurrentGoal | Agda.Interaction.Response
Info_Error | Agda.Interaction.Response
Info_GoalType | Agda.Interaction.Response
Info_InferredType | Agda.Interaction.Response
Info_Intro | Agda.Interaction.Response
Info_ModuleContents | Agda.Interaction.Response
Info_NormalForm | Agda.Interaction.Response
initCommandState | Agda.Interaction.InteractionTop
initCompileState | Agda.Compiler.Epic.CompileState
initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraph | Agda.Utils.Warshall
initialDotState | Agda.Interaction.Highlighting.Dot
initialIFSCandidates | Agda.TypeChecking.InstanceArguments
initializeIFSMeta | Agda.TypeChecking.InstanceArguments
initialPrims | Agda.Compiler.Epic.Primitive
initialRels | Agda.Compiler.Epic.Erasure
initialTags | Agda.Compiler.Epic.Injection
initiate | Agda.Compiler.Epic.Erasure
initMapS | Agda.Auto.Convert
initMeta | Agda.Auto.NarrowingSearch
initOccursCheck | Agda.TypeChecking.MetaVars.Occurs
initState |
1 (Function) | Agda.Syntax.Parser.Monad
2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
injArg | Agda.Compiler.Epic.Interface
injArity | Agda.Compiler.Epic.Interface
InjConstraints | Agda.Compiler.Epic.Injection
InjectiveFun |
1 (Type/Class) | Agda.Compiler.Epic.Interface
2 (Data Constructor) | Agda.Compiler.Epic.Interface
injectiveFuns | Agda.Compiler.Epic.Interface
Inline | Agda.Compiler.Epic.AuxAST
inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpace | Agda.Syntax.Scope.Base
InScope | Agda.Syntax.Scope.Base
InScopeTag | Agda.Syntax.Scope.Base
inScopeTag | Agda.Syntax.Scope.Base
insert |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.Trie
3 (Function) | Agda.Termination.CallGraph
4 (Function) | Agda.Utils.Graph
insertAfter | Agda.Compiler.JS.Compiler
insertAt | Agda.Compiler.Epic.Injection
insertImplicit | Agda.TypeChecking.Implicit
insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit
insertPatterns | Agda.TypeChecking.Rules.Def
insertTele | Agda.Compiler.Epic.Forcing
insertWith | Agda.Utils.HashMap
insertWithKeyM | Agda.Utils.Map
InsideOperandCtx | Agda.Syntax.Fixity
insideScope | Agda.Syntax.Translation.ConcreteToAbstract
Instance |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Common
InstanceArg | Agda.Syntax.Concrete
InstanceArgV | Agda.Syntax.Concrete.Operators.Parser
InstanceP | Agda.Syntax.Concrete
instanceTransformBiMT' | Agda.Utils.Geniplate
instanceUniverseBiT' | Agda.Utils.Geniplate
Instantiable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Instantiate | Agda.TypeChecking.Reduce
instantiate | Agda.TypeChecking.Reduce
Instantiated | Agda.Interaction.BasicOps
instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFull | Agda.TypeChecking.Reduce
instantiateFull | Agda.TypeChecking.Reduce
instantiatePattern | Agda.TypeChecking.Rules.LHS
instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate
inState | Agda.Syntax.Parser.LexActions
InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
int | Agda.Utils.Pretty
Integer | Agda.Compiler.JS.Syntax
integer | Agda.Utils.Pretty
integerSemiring | Agda.Termination.Semiring
Interaction | Agda.Interaction.InteractionTop
interaction | Agda.Interaction.CommandLine.CommandLine
InteractionId |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interactionLoop | Agda.Interaction.CommandLine.CommandLine
InteractionOutputCallback | Agda.Interaction.Response
InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Interactive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
Interface |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interpret | Agda.Interaction.InteractionTop
intersection | Agda.Utils.HashMap
intersectionWith | Agda.Utils.HashMap
intersectVars | Agda.TypeChecking.Conversion
intersectWith | Agda.Termination.SparseMatrix
Interval |
1 (Type/Class) | Agda.Syntax.Position
2 (Data Constructor) | Agda.Syntax.Position
Interval' | Agda.Syntax.Position
intervalInvariant | Agda.Syntax.Position
intLit | Agda.Compiler.JS.Parser
intMap | Agda.Utils.Warshall
inTopContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
introTactic | Agda.Interaction.BasicOps
Inv | Agda.TypeChecking.Injectivity
InvalidNoTerminationCheckPragma | Agda.Syntax.Concrete.Definitions
InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
invariant | Agda.Utils.Graph
Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseApplyRelevance | Agda.TypeChecking.Irrelevance
inverseComposeRelevance | Agda.TypeChecking.Irrelevance
inverseScopeLookup | Agda.Syntax.Scope.Base
inverseScopeLookupModule | Agda.Syntax.Scope.Base
inverseScopeLookupName | Agda.Syntax.Scope.Base
inverseSubst | Agda.TypeChecking.MetaVars
invertP | Agda.Utils.Permutation
InvView | Agda.TypeChecking.Injectivity
io | Agda.TypeChecking.Primitive
IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotapossmeta | Agda.Auto.Typecheck
iotastep | Agda.Auto.Typecheck
IOTCM |
1 (Type/Class) | Agda.Interaction.InteractionTop
2 (Data Constructor) | Agda.Interaction.InteractionTop
iPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Irr | Agda.Compiler.Epic.Interface
Irrel | Agda.TypeChecking.MetaVars.Occurs
Irrelevant | Agda.Syntax.Common
IrrelevantDatatype | Agda.TypeChecking.Coverage
Irrelevantly | Agda.TypeChecking.Free
irrelevantOrUnused | Agda.TypeChecking.Irrelevance
irrelevantVars | Agda.TypeChecking.Free
irrToNonStrict | Agda.TypeChecking.Irrelevance
IsAbstract | Agda.Syntax.Common
isAHole | Agda.Syntax.Notation
isAnonymousModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
isBelow | Agda.Utils.Warshall
isBinderUsed | Agda.TypeChecking.Free
isBindingHole | Agda.Syntax.Notation
isBlockedTerm | Agda.TypeChecking.MetaVars
isBounded | Agda.TypeChecking.SizedTypes
isCoinductive | Agda.TypeChecking.Rules.Data
isCon | Agda.TypeChecking.Quote
iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IsData | Agda.TypeChecking.Datatypes
isDataOrRecord | Agda.TypeChecking.Datatypes
isDataOrRecordType | Agda.TypeChecking.Datatypes
isDatatype |
1 (Function) | Agda.TypeChecking.Datatypes
2 (Function) | Agda.TypeChecking.Coverage
isDatatypeModule | Agda.Syntax.Scope.Monad
IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Termination.Matrix
3 (Function) | Agda.Termination.SparseMatrix
isEmptyObject | Agda.Compiler.JS.Compiler
IsEmptyType | Agda.Interaction.BasicOps
isEmptyType | Agda.TypeChecking.Empty
isEtaExpandable | Agda.TypeChecking.MetaVars
isEtaRecord | Agda.TypeChecking.Records
isEtaRecordType | Agda.TypeChecking.Records
isEtaRecordTypeHH | Agda.TypeChecking.Rules.LHS.Unify
IsExpr | Agda.Syntax.Concrete.Operators.Parser
isFrozen | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isGeneratedRecordConstructor | Agda.TypeChecking.Records
isHaskellKind | Agda.Compiler.HaskellTypes
isHiddenArg | Agda.Syntax.Common
isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isHom | Agda.TypeChecking.Rules.LHS.Unify
iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isInductiveRecord | Agda.TypeChecking.Records
IsInfix | Agda.Syntax.Common
isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInjective | Agda.Compiler.Epic.Injection
isInjectiveHere | Agda.Compiler.Epic.Injection
isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
isInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isIrr | Agda.Compiler.Epic.Erasure
isJust | Agda.Utils.Maybe
isLambdaHole | Agda.Syntax.Notation
isLeft | Agda.Utils.Either
isLevelConstraint | Agda.TypeChecking.UniversePolymorphism
IsLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isLiterate | Agda.Interaction.Options
isNatish | Agda.Compiler.Epic.NatDetection
isNewerThan | Agda.Interaction.Imports
isNoBody | Agda.Compiler.Epic.Injection
isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothing | Agda.Utils.Maybe
isntTypeConf | Agda.TypeChecking.Test.Generators
isOperator |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
IsPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isProblemSolved | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isRec | Agda.Compiler.Epic.NatDetection
IsRecord | Agda.TypeChecking.Datatypes
isRecord | Agda.TypeChecking.Records
isRecordConstructor | Agda.TypeChecking.Records
IsReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isRel | Agda.Compiler.Epic.Erasure
isRight | Agda.Utils.Either
isSet | Agda.Syntax.Abstract.Views
isSingleton |
1 (Function) | Agda.Termination.SparseMatrix
2 (Function) | Agda.Compiler.JS.Compiler
isSingletonRecord | Agda.TypeChecking.Records
isSingletonRecord' | Agda.TypeChecking.Records
isSingletonRecordModuloRelevance | Agda.TypeChecking.Records
isSingletonType | Agda.TypeChecking.Records
isSingletonType' | Agda.TypeChecking.Records
isSingletonTypeModuloRelevance | Agda.TypeChecking.Records
isSizeConstraint | Agda.TypeChecking.SizedTypes
isSizeNameTest | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeNameTestRaw | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeProblem | Agda.TypeChecking.SizedTypes
isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeTest | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblem | Agda.TypeChecking.Rules.LHS
isSolvingConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isSublistOf | Agda.Utils.List
isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract
isSubscriptDigit | Agda.Utils.Suffix
isSubsetOf | Agda.Utils.VarSet
isSuccess | Agda.Utils.QuickCheck
IsTag | Agda.Compiler.Epic.Injection
iStart | Agda.Syntax.Position
isTopLevelValue | Agda.Compiler.JS.Compiler
isType | Agda.TypeChecking.Rules.Term
IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConf | Agda.TypeChecking.Test.Generators
isTypeEqualTo | Agda.TypeChecking.Rules.Term
IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_ | Agda.TypeChecking.Rules.Term
isUnicodeId | Agda.Utils.Unicode
isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScoped | Agda.TypeChecking.Test.Generators
isZero | Agda.Utils.TestHelpers
Item | Agda.TypeChecking.Positivity
iterate' | Agda.Utils.Function