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

Index - I

iBuiltinAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ICArgListAgda.Auto.Syntax
ICExpAgda.Auto.Syntax
icnvhAgda.Auto.Convert
Id 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
IdentAgda.Syntax.Concrete
identifier 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Parser.LexActions
identityAgda.Utils.TestHelpers
IdentPAgda.Syntax.Concrete
idPAgda.Utils.Permutation
IdPartAgda.Syntax.Notation
idSubAgda.TypeChecking.Substitute
iEndAgda.Syntax.Position, Agda.Interaction.GhciTop
If 
1 (Data Constructor)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.Epic.AuxAST
ifBlockAgda.Compiler.JS.Parser
ifCleanAgda.TypeChecking.Rules.LHS.Unify
ifMAgda.Utils.Monad
ifNoConstraintsAgda.TypeChecking.Constraints
ifNoConstraints_Agda.TypeChecking.Constraints
IFSNoCandidateInScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IgnoreAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ignoreAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ignoreBlockingAgda.Syntax.Internal
ignoreForced 
1 (Function)Agda.TypeChecking.Irrelevance
2 (Function)Agda.Compiler.Epic.Erasure
ignoreInterfacesAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
ignoreReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHaskellImportsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iHighlightingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ihnameAgda.Compiler.MAlonzo.Misc
iImportedModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iInsideScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IlltypedPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IMAgda.Interaction.Monad
iModuleNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ImpInsertAgda.TypeChecking.Implicit
impInsertAgda.TypeChecking.Implicit
ImplicitInsertionAgda.TypeChecking.Implicit
ImplicitPAgda.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
importDirRangeAgda.Syntax.Concrete
ImportedModuleAgda.Syntax.Concrete
importedModulesAgda.Compiler.Epic.CompileState
ImportedName 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
importedNameAgda.Syntax.Concrete
ImportedNSAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
ImportPragmaAgda.Syntax.Concrete
importsAgda.Compiler.MAlonzo.Compiler
importsForPrimAgda.Compiler.MAlonzo.Primitives
IMPOSSIBLEAgda.Compiler.Epic.AuxAST
Impossible 
1 (Type/Class)Agda.Utils.Impossible
2 (Data Constructor)Agda.Utils.Impossible
ImpossiblePragmaAgda.Syntax.Concrete
impossibleTermAgda.Syntax.Internal
impossibleTestAgda.ImpossibleTest
imp_dirAgda.Syntax.Parser.Lexer
inAbstractModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
incAgda.Utils.Warshall
InClauseAgda.TypeChecking.Positivity
IncompletePatternAgda.Interaction.Highlighting.Precise
IncompletePatternMatchingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inConcreteModeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
inContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
InDefOfAgda.TypeChecking.Positivity
indentAgda.Utils.String
IndependenceAgda.Interaction.GhciTop
independenceAgda.Interaction.GhciTop
IndependentAgda.Interaction.GhciTop
Index 
1 (Data Constructor)Agda.Utils.Suffix
2 (Type/Class)Agda.Termination.CallGraph
IndexFreeInParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndexVariablesNotDistinctAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IndicesNotConstructorApplicationsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InductionAgda.Syntax.Common
InductiveAgda.Syntax.Common
InfAgda.Syntax.Internal
inferableAgda.Compiler.Epic.Smashing
inferableTermAgda.Compiler.Epic.Smashing
InferDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferDefAgda.TypeChecking.Rules.Term
InferExprAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inferExprAgda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop
inferHeadAgda.TypeChecking.Rules.Term
inferMetaAgda.TypeChecking.Rules.Term
infertypevarAgda.Auto.CaseSplit
InferVarAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
infimumAgda.Termination.CallGraph
InfiniteAgda.Utils.Warshall
infiniteAgda.Utils.Warshall
InfixAgda.Syntax.Concrete
InfixDefAgda.Syntax.Common
infixlPAgda.Syntax.Concrete.Operators.Parser
infixPAgda.Syntax.Concrete.Operators.Parser
infixrPAgda.Syntax.Concrete.Operators.Parser
InfoAgda.Syntax.Info
infodeclAgda.Compiler.MAlonzo.Compiler
infoOnExceptionAgda.Interaction.GhciTop
initCompileStateAgda.Compiler.Epic.CompileState
initEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
initGraphAgda.Utils.Warshall
initialDotStateAgda.Interaction.Highlighting.Dot
initialPrimsAgda.Compiler.Epic.Primitive
initialRelsAgda.Compiler.Epic.Erasure
initialTagsAgda.Compiler.Epic.Injection
initiateAgda.Compiler.Epic.Erasure
initMapSAgda.Auto.Convert
initMetaAgda.Auto.NarrowingSearch
initState 
1 (Function)Agda.Syntax.Parser.Monad
2 (Function)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Function)Agda.Interaction.GhciTop
injArgAgda.Compiler.Epic.Interface
injArityAgda.Compiler.Epic.Interface
InjConstraintsAgda.Compiler.Epic.Injection
InjectiveFun 
1 (Type/Class)Agda.Compiler.Epic.Interface
2 (Data Constructor)Agda.Compiler.Epic.Interface
injectiveFunsAgda.Compiler.Epic.Interface
InlineAgda.Compiler.Epic.AuxAST
inMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
inNameSpaceAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
InScopeTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inScopeTagAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
insert 
1 (Function)Agda.Utils.Graph
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Termination.CallGraph
insertAfterAgda.Compiler.JS.Compiler
insertAtAgda.Compiler.Epic.Injection
insertImplicitAgda.TypeChecking.Implicit
insertImplicitPatternsAgda.TypeChecking.Rules.LHS.Implicit
insertImplicitProblemAgda.TypeChecking.Rules.LHS.Implicit
insertPatternsAgda.TypeChecking.Rules.Def
insertTeleAgda.Compiler.Epic.Forcing
insertWithKeyMAgda.Utils.Map
InsideOperandCtxAgda.Syntax.Fixity
insideScopeAgda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop
Instance 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Common
InstanceArgAgda.Syntax.Concrete
InstanceArgVAgda.Syntax.Concrete.Operators.Parser
InstancePAgda.Syntax.Concrete
InstantiableAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstantiateAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
InstantiatedAgda.Interaction.BasicOps
instantiateDefAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
InstantiateFullAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiateFullAgda.TypeChecking.Reduce, Agda.Interaction.GhciTop
instantiatePatternAgda.TypeChecking.Rules.LHS
instantiateTelAgda.TypeChecking.Rules.LHS.Instantiate
inStateAgda.Syntax.Parser.LexActions
InstSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InstVAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
intAgda.Utils.Pretty
IntegerAgda.Compiler.JS.Syntax
integerAgda.Utils.Pretty
integerSemiringAgda.Termination.Semiring
Interaction 
1 (Type/Class)Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Interaction.GhciTop
interactionAgda.Interaction.CommandLine.CommandLine
InteractionId 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interactionLoopAgda.Interaction.CommandLine.CommandLine
InteractionPointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
interestingCallAgda.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
InternalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
internalErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
intersectVarsAgda.TypeChecking.Conversion
intersectWithAgda.Termination.SparseMatrix
Interval 
1 (Type/Class)Agda.Syntax.Position, Agda.Interaction.GhciTop
2 (Data Constructor)Agda.Syntax.Position, Agda.Interaction.GhciTop
intervalInvariantAgda.Syntax.Position, Agda.Interaction.GhciTop
intLitAgda.Compiler.JS.Parser
intMapAgda.Utils.Warshall
introTacticAgda.Interaction.BasicOps
InvAgda.TypeChecking.Injectivity
InvalidPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InvariantAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
InverseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
inverseApplyRelevanceAgda.TypeChecking.Irrelevance
inverseComposeRelevanceAgda.TypeChecking.Irrelevance
inverseScopeLookupAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupModuleAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
inverseScopeLookupNameAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
invertPAgda.Utils.Permutation
InvViewAgda.TypeChecking.Injectivity
ioAgda.TypeChecking.Primitive
IOExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
iotapossmetaAgda.Auto.Typecheck
iotastepAgda.Auto.Typecheck
ioTCMAgda.Interaction.GhciTop
ioTCM_Agda.Interaction.GhciTop
iPragmaOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
IrrAgda.Compiler.Epic.Interface
IrrelAgda.TypeChecking.MetaVars.Occurs
IrrelevantAgda.Syntax.Common
IrrelevantDatatypeAgda.TypeChecking.Coverage
irrelevantVarsAgda.TypeChecking.Free
irrToNonStrictAgda.TypeChecking.Irrelevance
IsAbstractAgda.Syntax.Common
isAHoleAgda.Syntax.Notation
isBelowAgda.Utils.Warshall
isBinderUsedAgda.TypeChecking.Free
isBindingHoleAgda.Syntax.Notation
isBlockedTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isCoinductiveAgda.TypeChecking.Rules.Data
isConAgda.TypeChecking.Quote
iScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isDataOrRecordTypeAgda.TypeChecking.Datatypes
isDatatype 
1 (Function)Agda.TypeChecking.Datatypes
2 (Function)Agda.TypeChecking.Coverage
IsEmptyAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isEmpty 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Termination.SparseMatrix
3 (Function)Agda.Termination.Matrix
IsEmptyTypeAgda.Interaction.BasicOps
isEmptyTypeAgda.TypeChecking.Empty
isEtaExpandableAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
isEtaRecordAgda.TypeChecking.Records
isEtaRecordTypeAgda.TypeChecking.Records
isEtaRecordTypeHHAgda.TypeChecking.Rules.LHS.Unify
IsExprAgda.Syntax.Concrete.Operators.Parser
isFrozenAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isGeneratedRecordConstructorAgda.TypeChecking.Records
isHaskellKindAgda.Compiler.HaskellTypes
isHiddenArgAgda.Syntax.Common
isHoleAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isHomAgda.TypeChecking.Rules.LHS.Unify
iSignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isImportedAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isIndependentAgda.Interaction.GhciTop
IsInfixAgda.Syntax.Common
isInfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isInjectiveAgda.Compiler.Epic.Injection
isInjectiveHereAgda.Compiler.Epic.Injection
isInModuleAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isInstantiatedMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isInteractionMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isIrrAgda.Compiler.Epic.Erasure
isJustAgda.Utils.Maybe
isLambdaHoleAgda.Syntax.Notation
isLeftAgda.Utils.Either
isLevelConstraintAgda.TypeChecking.UniversePolymorphism
isLiterateAgda.Interaction.Options
isNatishAgda.Compiler.Epic.NatDetection
isNewerThanAgda.Interaction.Imports
isNoBodyAgda.Compiler.Epic.Injection
isNoNameAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNonfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isNothingAgda.Utils.Maybe
isntTypeConfAgda.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, Agda.Interaction.GhciTop
isPostfixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isPrefixAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
isProblemSolvedAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
isProjectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
isReallyEmptyTypeAgda.TypeChecking.Empty
isRecAgda.Compiler.Epic.NatDetection
isRecordAgda.TypeChecking.Records
isRecordConstructorAgda.TypeChecking.Records
IsReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isReducedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isRelAgda.Compiler.Epic.Erasure
isRightAgda.Utils.Either
isSingleton 
1 (Function)Agda.Termination.SparseMatrix
2 (Function)Agda.Compiler.JS.Compiler
isSingletonRecordAgda.TypeChecking.Records
isSingletonRecord'Agda.TypeChecking.Records
isSingletonRecordModuloRelevanceAgda.TypeChecking.Records
isSizeNameTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSizeTypeTestAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
isSolvedProblemAgda.TypeChecking.Rules.LHS
isSolvingConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
IsSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isSortMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
isStringAgda.Utils.Generics
isSublistOfAgda.Utils.List
isSubModuleOfAgda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop
isSubsetOfAgda.Utils.VarSet
isSuccessAgda.Utils.QuickCheck
IsTagAgda.Compiler.Epic.Injection
iStartAgda.Syntax.Position, Agda.Interaction.GhciTop
isTypeAgda.TypeChecking.Rules.Term
IsTypeCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isTypeConfAgda.TypeChecking.Test.Generators
isTypeEqualToAgda.TypeChecking.Rules.Term
IsType_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
isType_Agda.TypeChecking.Rules.Term
isUnicodeIdAgda.Utils.Unicode
isVisitedAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
isWellScopedAgda.TypeChecking.Test.Generators
isZeroAgda.Utils.TestHelpers
ItemAgda.TypeChecking.Positivity
iterate'Agda.Utils.Function