IndexAgda-2.8.0.2
I
- IApplyAgda.Syntax.Internal.Elim
- IApplyPAgda.Syntax.Internal
- IApplyVarsAgda.TypeChecking.Telescope.Path
- iApplyVarsAgda.TypeChecking.Telescope.Path
- IArrayAgda.Utils.IArray
- iBuiltinAgda.TypeChecking.Monad.Base
- icod_Agda.TypeChecking.Serialise.Base
- ICODEAgda.TypeChecking.Serialise.Base
- icodeAgda.TypeChecking.Serialise.Base
- icodeArgsAgda.TypeChecking.Serialise.Base
- icodeDoubleAgda.TypeChecking.Serialise.Base
- icodeIntegerAgda.TypeChecking.Serialise.Base
- icodeMemoAgda.TypeChecking.Serialise.Base
- icodeNAgda.TypeChecking.Serialise.Base
- icodeN'Agda.TypeChecking.Serialise.Base
- icodeNodeAgda.TypeChecking.Serialise.Base
- icodeStringAgda.TypeChecking.Serialise.Base
- icodeXAgda.TypeChecking.Serialise.Base
- ICOptionAgda.Interaction.Options
- icOptionActiveAgda.Interaction.Options
- icOptionDescriptionAgda.Interaction.Options
- icOptionKindAgda.Interaction.Options
- icOptionOKAgda.Interaction.Options
- icOptionWarningAgda.Interaction.Options
- IdAgda.Syntax.Concrete.Name
- iDefaultPragmaOptionsAgda.TypeChecking.Monad.Base
- idempotentAgda.Termination.Termination
- IdentAgda.Syntax.ConcreteAgda.Utils.Haskell.Syntax
- identifierAgda.Syntax.Parser.LexActions
- IdentPAgda.Syntax.Concrete
- idFromFileAgda.TypeChecking.Monad.BaseAgda.Utils.FileId
- IdiomBracketErrorAgda.TypeChecking.Monad.Base
- IdiomBracketError_Agda.Interaction.Options.Errors
- IdiomBracketsAgda.Syntax.Concrete
- IdiomTypeAgda.Syntax.Internal
- iDisplayFormsAgda.TypeChecking.Monad.Base
- idPAgda.Utils.Permutation
- IdPartAgda.Syntax.Common
- IdSAgda.Syntax.InternalAgda.TypeChecking.Substitute
- idSAgda.TypeChecking.Substitute.Class
- IdToFileAgda.Utils.FileId
- idToFileAgda.Utils.FileId
- iEndAgda.Syntax.Position
- iEnd'Agda.Syntax.Position
- IfAgda.Utils.TypeLevel
- IfAgda.Compiler.JS.SyntaxAgda.Utils.Haskell.Syntax
- ifBlockedAgda.TypeChecking.Reduce
- ifDirtyAgda.Utils.Update
- iFilePragmaOptionsAgda.TypeChecking.Monad.Base
- iFileTypeAgda.TypeChecking.Monad.Base
- ifIsSortAgda.TypeChecking.Sort
- ifJustAgda.Utils.Maybe
- ifJustMAgda.Utils.MaybeAgda.Utils.Maybe.Strict
- ifLeAgda.TypeChecking.SizedTypes.Syntax
- ifMAgda.Utils.Monad
- ifNoConstraintsAgda.TypeChecking.Constraints
- ifNoConstraints_Agda.TypeChecking.Constraints
- ifNotMAgda.Utils.Monad
- ifNotNullAgda.Utils.List1Agda.Utils.Null
- ifNotNullMAgda.Utils.Null
- ifNotPathBAgda.TypeChecking.Telescope
- ifNotPiAgda.TypeChecking.Telescope
- ifNotPiOrPathBAgda.TypeChecking.Telescope
- ifNotPiOrPathTypeAgda.TypeChecking.Telescope
- ifNotPiTypeAgda.TypeChecking.Telescope
- ifNotSortAgda.TypeChecking.Sort
- ifNullAgda.Utils.List1Agda.Utils.Map1Agda.Utils.NullAgda.Utils.Set1
- ifNullMAgda.Utils.Null
- iForeignCodeAgda.TypeChecking.Monad.Base
- ifPathAgda.TypeChecking.Telescope
- ifPathBAgda.TypeChecking.Telescope
- ifPiAgda.TypeChecking.Telescope
- ifPiBAgda.TypeChecking.Telescope
- ifPiOrPathBAgda.TypeChecking.Telescope
- ifPiTypeAgda.TypeChecking.Telescope
- ifPiTypeBAgda.TypeChecking.Telescope
- ifThenElseAgda.Utils.Boolean
- ifTopLevelAndHighlightingLevelIsAgda.TypeChecking.Monad.Base
- ifTopLevelAndHighlightingLevelIsOrAgda.TypeChecking.Monad.Base
- iFullHashAgda.TypeChecking.Monad.Base
- IgnoreAbstractAgda.Interaction.Base
- IgnoreAbstractModeAgda.TypeChecking.Monad.Base
- ignoreAbstractModeAgda.TypeChecking.Monad.Signature
- IgnoreAllAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- ignoreBlockingAgda.Syntax.Internal.BlockersAgda.Syntax.Internal.Blockers
- IgnoreInAnnotationsAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- IgnoreNotAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- ignoreReducedAgda.TypeChecking.Monad.Base
- IgnoreSortsAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- IgnoreUnusedAgda.Compiler.ToTreeless
- iHighlightingAgda.TypeChecking.Monad.Base
- ihnameAgda.Compiler.MAlonzo.Misc
- iImportedModulesAgda.TypeChecking.Monad.Base
- iImportWarningAgda.TypeChecking.Monad.Base
- IInfoAgda.TypeChecking.Coverage.SplitClause
- iInsideScopeAgda.TypeChecking.Monad.Base
- ilamAgda.TypeChecking.Names
- iLengthAgda.Syntax.Position
- IllegalAgda.TypeChecking.Rules.LHS.UnifyAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
- IllegalAmbiguityAgda.Syntax.Scope.Base
- IllegalDeclarationBeforeTopLevelModuleAgda.TypeChecking.Monad.Base
- IllegalDeclarationBeforeTopLevelModule_Agda.Interaction.Options.Errors
- IllegalDeclarationInDataDefinitionAgda.TypeChecking.Monad.Base
- IllegalDeclarationInDataDefinition_Agda.Interaction.Options.Errors
- IllegalHidingInPostfixProjectionAgda.TypeChecking.Monad.Base
- IllegalHidingInPostfixProjection_Agda.Interaction.Options.Errors
- IllegalInstanceVariableInPatternSynonymAgda.TypeChecking.Monad.Base
- IllegalInstanceVariableInPatternSynonym_Agda.Interaction.Options.Errors
- IllegalLetInTelescopeAgda.TypeChecking.Monad.Base
- IllegalLetInTelescope_Agda.Interaction.Options.Errors
- IllegalPatternInTelescopeAgda.TypeChecking.Monad.Base
- IllegalPatternInTelescope_Agda.Interaction.Options.Errors
- IllegalRewriteRuleAgda.TypeChecking.Monad.Base
- IllegalRewriteRuleReasonAgda.TypeChecking.Monad.Base
- illegalRewriteWarningNameAgda.TypeChecking.Monad.Base
- IllformedAsClauseAgda.TypeChecking.Monad.Base
- IllformedAsClause_Agda.Interaction.Options.Warnings
- IllformedProjectionPatternAbstractAgda.TypeChecking.Monad.Base
- IllformedProjectionPatternAbstract_Agda.Interaction.Options.Errors
- IllformedProjectionPatternConcreteAgda.TypeChecking.Monad.Base
- IllformedProjectionPatternConcrete_Agda.Interaction.Options.Errors
- illiterateAgda.Syntax.Parser.Literate
- IllTypedPatternAfterWithAbstractionAgda.TypeChecking.Monad.Base
- IllTypedPatternAfterWithAbstraction_Agda.Interaction.Options.Errors
- IMAgda.Interaction.Monad
- IMaxAgda.Syntax.Internal
- imaxAgda.TypeChecking.Primitive.Cubical.Base
- iMetaBindingsAgda.TypeChecking.Monad.Base
- IMinAgda.Syntax.Internal
- iminAgda.TypeChecking.Primitive.Cubical.Base
- imoduleMapAgda.Syntax.Scope.Monad
- iModuleNameAgda.TypeChecking.Monad.Base
- imp_dirAgda.Syntax.Parser.Lexer
- ImpInsertAgda.TypeChecking.Implicit
- implicitArgsAgda.TypeChecking.Implicit
- ImplicitFlexAgda.TypeChecking.Rules.LHS.Problem
- ImplicitInsertionAgda.TypeChecking.Implicit
- implicitNamedArgsAgda.TypeChecking.Implicit
- implicitPAgda.TypeChecking.Rules.LHS.Implicit
- ImpliedPragmaOptionAgda.Interaction.Options
- impliedPragmaOptionsAgda.Interaction.Options
- impliesAgda.TypeChecking.SizedTypes.WarshallSolver
- impliesAgda.Utils.Boolean
- ImpliesPragmaOptionAgda.Interaction.Options
- ImpMissingDefinitionsAgda.Utils.Impossible
- ImportAgda.BenchmarkingAgda.Syntax.AbstractAgda.Syntax.Concrete
- ImportDeclAgda.Utils.Haskell.Syntax
- ImportDeclAgda.Utils.Haskell.Syntax
- ImportDirectiveAgda.Syntax.AbstractAgda.Syntax.Concrete
- ImportDirectiveAgda.Syntax.Common
- ImportDirective'Agda.Syntax.Common
- importDirRangeAgda.Syntax.Common
- ImportedModuleAgda.Syntax.Common
- ImportedModulesAgda.TypeChecking.Monad.Base
- ImportedNameAgda.Syntax.AbstractAgda.Syntax.Concrete
- ImportedNameAgda.Syntax.Common
- ImportedName'Agda.Syntax.Common
- ImportedNameMapAgda.Syntax.Scope.Monad
- ImportedNameMapAgda.Syntax.Scope.Monad
- importedNameMapFromListAgda.Syntax.Scope.Monad
- ImportedNSAgda.Syntax.Scope.Base
- ImportMayOpenAgda.Syntax.Concrete.Definitions.Errors
- importModuleAgda.Utils.Haskell.Syntax
- importPrimitiveModulesAgda.Interaction.Imports
- importPrimitivesAgda.Syntax.Translation.ConcreteToAbstract
- importQualifiedAgda.Utils.Haskell.Syntax
- ImportSAgda.Syntax.Abstract
- importsAgda.Compiler.JS.Syntax
- importsForPrimAgda.Compiler.MAlonzo.Primitives
- ImportSpecAgda.Utils.Haskell.Syntax
- importSpecsAgda.Utils.Haskell.Syntax
- ImpossibleAgda.Utils.Impossible
- ImpossibleAgda.Utils.Impossible
- impossibleAgda.Utils.Impossible
- ImpossibleConstructorAgda.TypeChecking.Monad.Base
- ImpossibleConstructor_Agda.Interaction.Options.Errors
- impossibleConstructorErrorNameAgda.TypeChecking.Errors.Names
- ImpossibleErrorAgda.Interaction.ExitCode
- ImpossiblePragmaAgda.Syntax.Concrete
- impossibleTermAgda.Syntax.Internal
- impossibleTestAgda.ImpossibleTest
- impossibleTestReduceMAgda.ImpossibleTest
- impRenamingAgda.Syntax.Common
- ImproperInstHeadAgda.TypeChecking.Monad.Base
- ImproperInstTeleAgda.TypeChecking.Monad.Base
- InAgda.Syntax.Concrete.Operators.Parser
- In1Agda.Utils.Three
- In2Agda.Utils.Three
- In3Agda.Utils.Three
- inAbstractModeAgda.TypeChecking.Monad.Signature
- inameMapAgda.Syntax.Scope.Monad
- InClauseAgda.TypeChecking.Positivity.Occurrence
- includesAgda.TypeChecking.Serialise.Base
- InclusionAgda.Utils.PartialOrd
- InclusionAgda.Utils.PartialOrd
- inclusionAgda.Utils.PartialOrd
- IncoherentAgda.Syntax.Common
- incomingAgda.TypeChecking.SizedTypes.WarshallSolver
- inCompilerEnvAgda.Compiler.Common
- incompleteMatchWarningsAgda.Interaction.Options.Warnings
- IncompletePatternAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- inConcreteModeAgda.TypeChecking.Monad.Signature
- inConcreteOrAbstractModeAgda.TypeChecking.Monad.Signature
- IncorrectTypeForRewriteRelationAgda.TypeChecking.Monad.Base
- IncorrectTypeForRewriteRelation_Agda.Interaction.Options.Errors
- IncorrectTypeForRewriteRelationReasonAgda.TypeChecking.Monad.Base
- increaseAgda.Termination.Order
- inCxtAgda.TypeChecking.Names
- IndArgTypeAgda.TypeChecking.Positivity.Occurrence
- InDefOfAgda.TypeChecking.Positivity.Occurrence
- IndentAgda.Compiler.JS.Pretty
- indentAgda.Compiler.JS.PrettyAgda.Utils.String
- indentByAgda.Compiler.JS.Pretty
- independentAgda.Interaction.InteractionTop
- IndexAgda.Utils.IndexedList
- IndexAgda.Utils.Suffix
- indexAgda.Utils.IArray
- IndexedClauseAgda.TypeChecking.Monad.Base
- IndexedClauseArgAgda.TypeChecking.Monad.Base
- indexWithDefaultAgda.Utils.List
- indicesAgda.Utils.IArray
- IndirectAgda.TypeChecking.Monad.Base.Types
- InductionAgda.Syntax.CommonAgda.Syntax.Common.Aspect
- InductionAgda.Syntax.Concrete
- InductionAndEtaAgda.TypeChecking.Monad.Base
- InductionAndEtaAgda.TypeChecking.Monad.Base
- InductiveAgda.Syntax.CommonAgda.Syntax.Common.Aspect
- INegAgda.Syntax.Internal
- inegAgda.TypeChecking.Primitive.Cubical.Base
- InfAgda.Syntax.Internal
- infAgda.TypeChecking.Positivity
- infallibleSortKitAgda.TypeChecking.Monad.Builtin
- InfectiveAgda.Interaction.OptionsAgda.Interaction.Options
- InfectiveCoinfectiveAgda.Interaction.OptionsAgda.Interaction.Options
- InfectiveCoinfectiveOptionAgda.Interaction.Options
- infectiveCoinfectiveOptionsAgda.Interaction.Options
- InfectiveImportAgda.TypeChecking.Monad.Base
- InfectiveImport_Agda.Interaction.Options.Warnings
- inferAgda.TypeChecking.CheckInternal
- inferApplicationAgda.TypeChecking.Rules.Application
- InferDefAgda.TypeChecking.Monad.Base
- InferExprAgda.TypeChecking.Monad.Base
- inferExprAgda.TheTypeCheckerAgda.TypeChecking.Rules.Term
- inferExpr'Agda.TypeChecking.Rules.Term
- inferExprForWithAgda.TypeChecking.Rules.Term
- inferFunSortAgda.TypeChecking.Sort
- inferInternalAgda.TypeChecking.CheckInternal
- inferInternal'Agda.TypeChecking.CheckInternal
- inferMetaAgda.TypeChecking.Rules.Term
- inferNeutralAgda.TypeChecking.ProjectionLike
- inferPiSortAgda.TypeChecking.Sort
- InferredAgda.TypeChecking.Monad.Base
- inferredBlockAgda.Syntax.Concrete.Definitions.Types
- inferredChecksAgda.Syntax.Concrete.Definitions.Types
- inferredLeftoversAgda.Syntax.Concrete.Definitions.Types
- InferredMutualAgda.Syntax.Concrete.Definitions.Types
- InferredMutualAgda.Syntax.Concrete.Definitions.Types
- inferSpineAgda.TypeChecking.CheckInternal
- inferUnivSortAgda.TypeChecking.Sort
- InferVarAgda.TypeChecking.Monad.Base
- infimumAgda.Termination.Order
- InfinityAgda.TypeChecking.SizedTypes.WarshallSolver
- infinityFlexsAgda.TypeChecking.SizedTypes.WarshallSolver
- InfixAgda.Syntax.Concrete
- InfixAppAgda.Utils.Haskell.Syntax
- InfixDefAgda.Syntax.Common
- InfixNotationAgda.Syntax.Notation
- Info_AllGoalsWarningsAgda.Interaction.Response.Base
- Info_AutoAgda.Interaction.Response.Base
- Info_CompilationErrorAgda.Interaction.Response.Base
- Info_CompilationOkAgda.Interaction.Response.Base
- Info_ConstraintsAgda.Interaction.Response.Base
- Info_ContextAgda.Interaction.Response.Base
- Info_ErrorAgda.Interaction.Response
- Info_ErrorAgda.Interaction.Response.Base
- Info_Error_bootAgda.Interaction.Response.Base
- Info_GenericErrorAgda.Interaction.Response.Base
- Info_GoalSpecificAgda.Interaction.Response.Base
- Info_HighlightingParseErrorAgda.Interaction.Response.Base
- Info_HighlightingScopeCheckErrorAgda.Interaction.Response.Base
- Info_InferredTypeAgda.Interaction.Response.Base
- Info_Intro_ConstructorUnknownAgda.Interaction.Response.Base
- Info_Intro_NotFoundAgda.Interaction.Response.Base
- Info_ModuleContentsAgda.Interaction.Response.Base
- Info_NormalFormAgda.Interaction.Response.Base
- Info_SearchAboutAgda.Interaction.Response.Base
- Info_TimeAgda.Interaction.Response.Base
- Info_VersionAgda.Interaction.Response.Base
- Info_WhyInScopeAgda.Interaction.Response.Base
- infoEqLHSAgda.TypeChecking.Coverage.SplitClause
- infoEqRHSAgda.TypeChecking.Coverage.SplitClause
- infoEqTelAgda.TypeChecking.Coverage.SplitClause
- infoLeftInvAgda.TypeChecking.Coverage.SplitClause
- infoRhoAgda.TypeChecking.Coverage.SplitClause
- informAgda.Setup.EmacsMode
- infoTauAgda.TypeChecking.Coverage.SplitClause
- infoTelAgda.TypeChecking.Coverage.SplitClause
- infoTel0Agda.TypeChecking.Coverage.SplitClause
- inFreshModuleIfFreeParamsAgda.TypeChecking.Monad.Signature
- InfSAgda.Syntax.Reflected
- InftyAgda.TypeChecking.SizedTypes.Syntax
- initAgda.Utils.List1Agda.Utils.List2
- init1Agda.Utils.List
- initCommandStateAgda.Interaction.Base
- initCopyInfoAgda.Syntax.Abstract
- initEnvAgda.TypeChecking.Monad.Base
- initFileDictAgda.TypeChecking.Monad.Base
- initFreeEnvAgda.TypeChecking.Free.Lazy
- InitialCandidatesAgda.Benchmarking
- initialiseCommandQueueAgda.Interaction.InteractionTop
- initialMetaIdAgda.TypeChecking.Monad.Base
- initLastAgda.Utils.ListAgda.Utils.List1
- initLast1Agda.Utils.List
- initLHSStateAgda.TypeChecking.Rules.LHS.ProblemRest
- initMaybeAgda.Utils.List
- initNiceStateAgda.Syntax.Concrete.Definitions.Monad
- initOccursCheckAgda.TypeChecking.MetaVars.Occurs
- initPersistentStateAgda.TypeChecking.Monad.Base
- initPersistentStateFromSessionStateAgda.TypeChecking.Monad.Base
- initPostScopeStateAgda.TypeChecking.Monad.Base
- initPreScopeStateAgda.TypeChecking.Monad.Base
- initsAgda.Utils.List1
- inits1Agda.Utils.List1
- initSessionStateAgda.TypeChecking.Monad.Base
- initStateAgda.Syntax.Parser.MonadAgda.TypeChecking.Monad.Base
- initStateFromPersistentStateAgda.TypeChecking.Monad.Base
- initStateFromSessionStateAgda.TypeChecking.Monad.Base
- initStateIOAgda.TypeChecking.Monad.Base
- initUnifyStateAgda.TypeChecking.Rules.LHS.Unify.Types
- initWithDefaultAgda.Utils.List
- injectAtAgda.TypeChecking.Rules.LHS.Unify.Types
- injectConstructorAgda.TypeChecking.Rules.LHS.Unify.Types
- injectDatatypeAgda.TypeChecking.Rules.LHS.Unify.Types
- injectIndicesAgda.TypeChecking.Rules.LHS.Unify.Types
- InjectiveForInferencePragmaAgda.Syntax.AbstractAgda.Syntax.Concrete
- InjectivePragmaAgda.Syntax.AbstractAgda.Syntax.Concrete
- InjectivityAgda.BenchmarkingAgda.TypeChecking.Rules.LHS.Unify.Types
- injectParametersAgda.TypeChecking.Rules.LHS.Unify.Types
- injectTypeAgda.TypeChecking.Rules.LHS.Unify.Types
- InlineNoExactSplitAgda.TypeChecking.Monad.Base
- InlineNoExactSplit_Agda.Interaction.Options.Warnings
- InlinePragmaAgda.Syntax.AbstractAgda.Syntax.Concrete
- InlineReductionsAgda.TypeChecking.Monad.Base
- InMutualAgda.Syntax.Concrete.Definitions.Types
- InMutualAgda.Syntax.Concrete.Definitions.Types
- inMutualBlockAgda.TypeChecking.Monad.Mutual
- inNameSpaceAgda.Syntax.Scope.Base
- inOriginalContextAgda.TypeChecking.Unquote
- inplaceSAgda.TypeChecking.Substitute.Class
- inputFlagAgda.Interaction.Options
- inRangeAgda.Utils.IArray
- InScopeAgda.Syntax.Scope.Base
- InScopeAgda.Syntax.Concrete.Name
- inScopeBecauseAgda.Syntax.Scope.Base
- InScopeSetAgda.Syntax.Scope.Base
- InScopeTagAgda.Syntax.Scope.Base
- inScopeTagAgda.Syntax.Scope.Base
- InSeqAgda.Compiler.Treeless.Subst
- InSeqAgda.Compiler.Treeless.Subst
- inSeqAgda.Compiler.Treeless.Subst
- insertAgda.Termination.CallGraphAgda.Termination.CallMatrixAgda.Utils.AssocListAgda.Utils.BagAgda.Utils.BiMapAgda.Utils.BoolSetAgda.Utils.FavoritesAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.HashTableAgda.Utils.List1Agda.Utils.Map1Agda.Utils.RangeMapAgda.Utils.Set1Agda.Utils.SmallSetAgda.Utils.TrieAgda.Utils.VarSet
- insertAfterAgda.Compiler.JS.Compiler
- insertComparedAgda.Utils.Favorites
- insertDTAgda.TypeChecking.DiscrimTree
- InsertedAgda.Syntax.Common
- insertedBinderAgda.Syntax.Abstract
- insertedBinder_Agda.Syntax.Abstract
- InsertedBinderNameAgda.Syntax.Common
- insertEdgeAgda.TypeChecking.SizedTypes.WarshallSolverAgda.Utils.Graph.AdjacencyMap.Unidirectional
- insertEdgeWithAgda.Utils.Graph.AdjacencyMap.Unidirectional
- insertHiddenLambdasAgda.TypeChecking.Rules.Term
- insertImplicitAgda.TypeChecking.Implicit
- insertImplicit'Agda.TypeChecking.Implicit
- insertImplicitPatSynArgsAgda.Syntax.Abstract
- insertImplicitPatternsAgda.TypeChecking.Rules.LHS.Implicit
- insertImplicitPatternsTAgda.TypeChecking.Rules.LHS.Implicit
- insertImplicitSizeLtPatternsAgda.TypeChecking.Rules.LHS.Implicit
- insertInspectsAgda.TypeChecking.Rules.Def
- insertLookupWithKeyAgda.Utils.BiMapAgda.Utils.Map1
- insertLookupWithKeyPreconditionAgda.Utils.BiMap
- insertMapAgda.Utils.Map1
- insertMapMaxAgda.Utils.Map1
- insertMapMinAgda.Utils.Map1
- insertMapWithAgda.Utils.Map1
- insertMapWithKeyAgda.Utils.Map1
- insertMetaSetAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- insertMetaVarAgda.TypeChecking.Monad.MetaVars
- insertMissingFieldsAgda.TypeChecking.Records
- insertMissingFieldsFailAgda.TypeChecking.Records
- insertMissingFieldsWarnAgda.TypeChecking.Records
- insertMutualBlockInfoAgda.TypeChecking.Monad.Mutual
- insertNamesAgda.TypeChecking.Rules.Def
- insertOldInteractionScopeAgda.Interaction.InteractionTop
- insertPatternsAgda.TypeChecking.Rules.Def
- insertPatternsLHSCoreAgda.TypeChecking.Rules.Def
- insertPreconditionAgda.Utils.BiMap
- insertSetAgda.Utils.Set1
- insertSetMaxAgda.Utils.Set1
- insertSetMinAgda.Utils.Set1
- insertTrailingArgsAgda.TypeChecking.Coverage
- insertWithAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.Map1Agda.Utils.Trie
- insertWithKeyAgda.Utils.Map1
- insideAndOutsideAgda.Interaction.Highlighting.PreciseAgda.Utils.RangeMap
- insideDotPatternAgda.TypeChecking.Monad.Env
- InsideOperandCtxAgda.Syntax.Fixity
- InstanceAgda.Syntax.Common
- InstanceArgAgda.Syntax.Concrete
- InstanceArgVAgda.Syntax.Concrete.Operators.Parser
- InstanceArgWithExplicitArgAgda.TypeChecking.Monad.Base
- InstanceArgWithExplicitArg_Agda.Interaction.Options.Warnings
- InstanceBAgda.Syntax.Concrete
- InstanceBlockAgda.Syntax.Concrete.Definitions.Types
- instanceClassAgda.TypeChecking.Monad.Base
- InstanceDefAgda.Syntax.Common
- InstanceInfoAgda.TypeChecking.Monad.Base
- InstanceInfoAgda.TypeChecking.Monad.Base
- InstanceMetaAgda.Syntax.Info
- InstanceNoCandidateAgda.TypeChecking.Monad.Base
- InstanceNoCandidate_Agda.Interaction.Options.Errors
- InstanceNoOutputTypeNameAgda.TypeChecking.Monad.Base
- InstanceNoOutputTypeName_Agda.Interaction.Options.Warnings
- InstanceNotInArgumentPositionAgda.TypeChecking.Monad.Base
- InstanceNotInArgumentPosition_Agda.Interaction.Options.Warnings
- instanceOverlapAgda.TypeChecking.Monad.Base
- InstancePAgda.Syntax.Concrete
- InstanceProblemAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- InstancesAgda.Utils.ProfileOptions
- InstanceSearchAgda.Benchmarking
- InstanceSearchDepthExhaustedAgda.TypeChecking.Monad.Base
- InstanceSearchDepthExhausted_Agda.Interaction.Options.Errors
- InstanceTableAgda.TypeChecking.Monad.Base
- InstanceTableAgda.TypeChecking.Monad.Base
- InstanceWithExplicitArgAgda.TypeChecking.Monad.Base
- InstanceWithExplicitArg_Agda.Interaction.Options.Warnings
- InstantiableAgda.TypeChecking.Monad.Base
- InstantiateAgda.TypeChecking.Reduce
- instantiateAgda.TypeChecking.Reduce
- instantiate'Agda.TypeChecking.Reduce
- InstantiatedAgda.Interaction.Base
- instantiateDefAgda.TypeChecking.Monad.Signature
- instantiateDefinitionTypeAgda.TypeChecking.Rules.Decl
- InstantiateFullAgda.TypeChecking.Reduce
- instantiateFullAgda.TypeChecking.Reduce
- instantiateFull'Agda.TypeChecking.Reduce
- instantiateRewriteRuleAgda.TypeChecking.Monad.Signature
- instantiateRewriteRulesAgda.TypeChecking.Monad.Signature
- instantiateTelescopeAgda.TypeChecking.Telescope
- instantiateVarHeadsAgda.TypeChecking.Injectivity
- instantiateWhenAgda.TypeChecking.Reduce
- InstantiationAgda.TypeChecking.Monad.Base
- InstantiationAgda.TypeChecking.Monad.Base
- inStateAgda.Syntax.Parser.LexActions
- instBodyAgda.TypeChecking.Monad.Base
- instTelAgda.TypeChecking.Monad.Base
- InstVAgda.TypeChecking.Monad.Base
- IntAgda.Utils.Haskell.Syntax
- intAgda.Syntax.Common.Pretty
- intAgda.Compiler.Treeless.EliminateLiteralPatterns
- IntegerAgda.Compiler.JS.Syntax
- integerAgda.Syntax.Common.PrettyAgda.Syntax.Parser.LexActions
- integerCAgda.TypeChecking.Serialise.Base
- integerDAgda.TypeChecking.Serialise.Base
- integerEAgda.TypeChecking.Serialise.Base
- integerSemiringAgda.Termination.Semiring
- integerToCharAgda.Utils.Char
- InteractionAgda.Interaction.Base
- Interaction'Agda.Interaction.Base
- InteractionEmacsAgda.Main
- InteractionErrorAgda.TypeChecking.Monad.Base
- InteractionErrorAgda.TypeChecking.Monad.Base
- interactionErrorAgda.TypeChecking.Monad.Base
- InteractionError_Agda.Interaction.Options.Errors
- InteractionError_Agda.Interaction.Options.Errors
- interactionErrorNameAgda.TypeChecking.Errors.Names
- interactionErrorNameStringAgda.Interaction.Options.Errors
- InteractionFormatAgda.Main
- InteractionIdAgda.Syntax.Common
- InteractionIdAgda.Syntax.Common
- interactionIdAgda.Syntax.Common
- interactionIdToMetaIdAgda.Interaction.BasicOps
- interactionInteractorAgda.Main
- InteractionJsonAgda.Main
- InteractionMetaBoundariesAgda.TypeChecking.Monad.Base
- InteractionMetaBoundaries_Agda.Interaction.Options.Warnings
- InteractionOutputCallbackAgda.Interaction.ResponseAgda.TypeChecking.Monad.Base
- InteractionPointAgda.TypeChecking.Monad.Base
- InteractionPointAgda.TypeChecking.Monad.Base
- InteractionPointsAgda.TypeChecking.Monad.Base
- InteractiveAgda.TypeChecking.Monad.Base.TypesAgda.Utils.ProfileOptions
- InteractorAgda.Main
- interAssocWithAgda.Termination.SparseMatrix
- interestingCallAgda.TypeChecking.Monad.Trace
- interestingConstraintAgda.TypeChecking.Pretty.Constraint
- InterfaceAgda.TypeChecking.Monad.Base
- InterfaceAgda.TypeChecking.Monad.Base
- InterfaceFileAgda.Interaction.FindFile
- InterfaceInstantiateFullAgda.Benchmarking
- InterleavedDataAgda.Syntax.Concrete.Definitions.Types
- interleavedDataConsAgda.Syntax.Concrete.Definitions.Types
- InterleavedDeclAgda.Syntax.Concrete.Definitions.Types
- interleavedDeclAgda.Syntax.Concrete.Definitions.Types
- interleavedDeclNumAgda.Syntax.Concrete.Definitions.TypesAgda.Syntax.Concrete.Definitions.Types
- interleavedDeclSigAgda.Syntax.Concrete.Definitions.TypesAgda.Syntax.Concrete.Definitions.Types
- InterleavedFunAgda.Syntax.Concrete.Definitions.Types
- interleavedFunClausesAgda.Syntax.Concrete.Definitions.Types
- InterleavedMutualAgda.Syntax.Concrete.Definitions.Types
- InterleavedMutualAgda.Syntax.Concrete
- interleaveRangesAgda.Syntax.Position
- InternalAgda.Utils.ProfileOptions
- InternalErrorAgda.TypeChecking.Monad.Base
- internalErrorAgda.TypeChecking.Monad.Base
- InternalError_Agda.Interaction.Options.Errors
- interpretAgda.Interaction.InteractionTop
- intersectionAgda.Utils.BoolSetAgda.Utils.Map1Agda.Utils.Set1Agda.Utils.SmallSetAgda.Utils.VarSet
- intersectionWithAgda.Utils.Map1
- intersectionWithKeyAgda.Utils.Map1
- intersectVarsAgda.TypeChecking.Conversion
- intersectWithAgda.Termination.SparseMatrix
- intersperseAgda.Utils.List1
- IntervalAgda.Syntax.Position
- IntervalAgda.Syntax.Position
- intervalAgda.Syntax.Parser.Literate
- Interval'Agda.Syntax.Position
- intervalInvariantAgda.Syntax.Position
- intervalSortAgda.TypeChecking.Monad.Builtin
- intervalsToRangeAgda.Syntax.Position
- intervalToRangeAgda.Syntax.Position
- IntervalUnivAgda.Syntax.Internal
- intervalUnviewAgda.TypeChecking.Monad.Builtin
- intervalUnview'Agda.TypeChecking.Monad.Builtin
- IntervalViewAgda.Syntax.Internal
- intervalViewAgda.TypeChecking.Monad.Builtin
- intervalView'Agda.TypeChecking.Monad.Builtin
- IntervalWithoutFileAgda.Syntax.Position
- intFilePathAgda.Interaction.FindFile
- inTopContextAgda.TypeChecking.Monad.Context
- IntroAgda.Interaction.InteractionTop
- introTacticAgda.Interaction.BasicOps
- intSemiringAgda.Termination.Semiring
- IntSetAgda.Utils.IntSet.Infinite
- intSignatureAgda.TypeChecking.Monad.Base
- intToDoubleAgda.Utils.Float
- intViewAgda.Syntax.Treeless
- InvAgda.TypeChecking.Injectivity
- InvalidBuiltinAgda.TypeChecking.Monad.Base
- InvalidBuiltin_Agda.Interaction.Options.Errors
- InvalidCatchallPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidCatchallPragma_Agda.Interaction.Options.Warnings
- InvalidCharacterLiteralAgda.TypeChecking.Monad.Base
- InvalidCharacterLiteral_Agda.Interaction.Options.Warnings
- InvalidConstructorBlockAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidConstructorBlock_Agda.Interaction.Options.Warnings
- InvalidCoverageCheckPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidCoverageCheckPragma_Agda.Interaction.Options.Warnings
- InvalidDisplayFormAgda.TypeChecking.Monad.Base
- InvalidDisplayForm_Agda.Interaction.Options.Warnings
- InvalidDottedExpressionAgda.TypeChecking.Monad.Base
- InvalidDottedExpression_Agda.Interaction.Options.Errors
- InvalidExtensionErrorAgda.Syntax.ParserAgda.Syntax.Parser.Monad
- InvalidFileNameAgda.TypeChecking.Monad.Base
- InvalidFileName_Agda.Interaction.Options.Errors
- InvalidFileNameReasonAgda.TypeChecking.Monad.Base
- InvalidInstanceHeadTypeAgda.TypeChecking.Monad.Base
- InvalidInstanceHeadType_Agda.Interaction.Options.Errors
- InvalidMeasureMutualAgda.Syntax.Concrete.Definitions.Errors
- InvalidMeasureMutual_Agda.Interaction.Options.Errors
- InvalidModalTelescopeUseAgda.TypeChecking.Monad.Base
- InvalidModalTelescopeUse_Agda.Interaction.Options.Errors
- InvalidNoPositivityCheckPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidNoPositivityCheckPragma_Agda.Interaction.Options.Warnings
- InvalidNoUniverseCheckPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidNoUniverseCheckPragma_Agda.Interaction.Options.Warnings
- InvalidPatternAgda.TypeChecking.Monad.Base
- InvalidPattern_Agda.Interaction.Options.Errors
- InvalidProjectionParameterAgda.TypeChecking.Monad.Base
- InvalidProjectionParameter_Agda.Interaction.Options.Errors
- InvalidPunAgda.TypeChecking.Monad.Base
- InvalidPun_Agda.Interaction.Options.Errors
- InvalidTerminationCheckPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidTerminationCheckPragma_Agda.Interaction.Options.Warnings
- InvalidTypeSortAgda.TypeChecking.Monad.Base
- InvalidTypeSort_Agda.Interaction.Options.Errors
- InvariantAgda.TypeChecking.Monad.Base.Types
- invariantAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.IntSet.Infinite
- InverseAgda.TypeChecking.Monad.Base
- inverseApplyCohesionAgda.Syntax.Common
- inverseApplyModalityButNotQuantityAgda.Syntax.Common
- inverseApplyPolarityAgda.Syntax.Common
- inverseApplyQuantityAgda.Syntax.Common
- inverseApplyRelevanceAgda.Syntax.Common
- inverseComposeAgda.Utils.POMonoid
- inverseComposeCohesionAgda.Syntax.Common
- inverseComposeModalityAgda.Syntax.Common
- inverseComposePolarityAgda.Syntax.Common
- inverseComposePolarity'Agda.Syntax.Common
- inverseComposeQuantityAgda.Syntax.Common
- inverseComposeRelevanceAgda.Syntax.Common
- InversePermuteAgda.Utils.Permutation
- inversePermuteAgda.Utils.Permutation
- InverseScopeLookupAgda.Benchmarking
- inverseScopeLookupModuleAgda.Syntax.Scope.Base
- inverseScopeLookupModule'Agda.Syntax.Scope.Base
- inverseScopeLookupNameAgda.Syntax.Scope.Base
- inverseScopeLookupName'Agda.Syntax.Scope.Base
- inverseScopeLookupName''Agda.Syntax.Scope.Base
- inverseSubst'Agda.TypeChecking.MetaVars
- InversionDepthReachedAgda.TypeChecking.Monad.Base
- InversionDepthReached_Agda.Interaction.Options.Warnings
- InversionMapAgda.TypeChecking.Monad.Base
- InvertAgda.Syntax.Common
- InvertExceptAgda.TypeChecking.MetaVars
- invertFunctionAgda.TypeChecking.Injectivity
- invertPAgda.Utils.Permutation
- invLookupAgda.Utils.BiMap
- InvViewAgda.TypeChecking.Injectivity
- ioAgda.TypeChecking.Primitive.Base
- IOExceptionAgda.TypeChecking.Monad.Base
- IOneAgda.Syntax.Internal
- iOpaqueBlocksAgda.TypeChecking.Monad.Base
- iOpaqueNamesAgda.TypeChecking.Monad.Base
- iOptionsUsedAgda.TypeChecking.Monad.Base
- IORefAgda.Utils.IORef
- IOTCMAgda.Interaction.Base
- IOTCMAgda.Interaction.Base
- IOTCM'Agda.Interaction.Base
- iPartialDefsAgda.TypeChecking.Monad.Base
- iPatternSynsAgda.TypeChecking.Monad.Base
- IPBoundaryAgda.TypeChecking.Monad.Base
- IPBoundaryAgda.TypeChecking.Monad.Base
- ipBoundaryAgda.TypeChecking.Monad.Base
- IPBoundary'Agda.TypeChecking.Monad.Base
- ipcClauseAgda.TypeChecking.Monad.Base
- ipcClauseNoAgda.TypeChecking.Monad.Base
- ipcClosureAgda.TypeChecking.Monad.Base
- IPClauseAgda.TypeChecking.Monad.Base
- IPClauseAgda.TypeChecking.Monad.Base
- ipClauseAgda.TypeChecking.Monad.Base
- ipcQNameAgda.TypeChecking.Monad.Base
- ipcTypeAgda.TypeChecking.Monad.Base
- ipcWithSubAgda.TypeChecking.Monad.Base
- IPFace'Agda.TypeChecking.Monad.Base.Types
- IPFace'Agda.TypeChecking.Monad.Base.Types
- ipMetaAgda.TypeChecking.Monad.Base
- IPNoClauseAgda.TypeChecking.Monad.Base
- ipRangeAgda.TypeChecking.Monad.Base
- ipSolvedAgda.TypeChecking.Monad.Base
- IrrelevantAgda.Syntax.Common
- irrelevantAgda.Syntax.Common
- irrelevantToShapeIrrelevantAgda.Syntax.Common
- IsAbstractAgda.Syntax.Common
- isAbsurdBodyAgda.Syntax.Internal
- isAbsurdLambdaNameAgda.TypeChecking.Monad.Base
- isAbsurdPAgda.Syntax.Concrete
- isAbsurdPatternNameAgda.Syntax.Internal
- isAccessibleDefAgda.TypeChecking.Opacity
- isAHoleAgda.Syntax.Notation
- isAliasAgda.TypeChecking.Rules.Def
- IsAmbiguousAgda.TypeChecking.Monad.Base
- isAmbiguousAgda.Syntax.Abstract.Name
- isAnonymousModuleNameAgda.Syntax.Abstract.Name
- IsApplyAgda.TypeChecking.Coverage.Match
- isApplyElimAgda.Syntax.Internal.Elim
- isApplyElim'Agda.Syntax.Internal.Elim
- IsBaseAgda.Utils.TypeLevel
- IsBasicRangeMapAgda.Interaction.Highlighting.PreciseAgda.Utils.RangeMap
- isBenchmarkOnAgda.Utils.Benchmark
- isBinderAgda.Syntax.Notation
- isBinderPAgda.Syntax.Concrete
- isBinderUsedAgda.TypeChecking.Free
- isBlockedAgda.TypeChecking.Reduce
- isBlockedTermAgda.TypeChecking.MetaVars
- isBlockingConstraintAgda.TypeChecking.Monad.Constraints
- IsBoolAgda.Utils.Boolean
- isBoundedAgda.TypeChecking.SizedTypes
- isBoundedProjVarAgda.TypeChecking.SizedTypes
- isBoundedSizeTypeAgda.TypeChecking.SizedTypes
- IsBuiltinAgda.Syntax.Builtin
- isBuiltinAgda.TypeChecking.Primitive.Base
- IsBuiltinModuleAgda.TypeChecking.Monad.Base.Types
- IsBuiltinModuleAgda.TypeChecking.Monad.Base.Types
- isBuiltinModuleAgda.TypeChecking.Monad.State
- IsBuiltinModuleWithSafePostulatesAgda.TypeChecking.Monad.Base.Types
- isBuiltinModuleWithSafePostulatesAgda.TypeChecking.Monad.State
- isBuiltinNoDefAgda.Syntax.Builtin
- isCanonicalAgda.TypeChecking.Conversion
- isClosedAgda.TypeChecking.Monad.Open
- isCodeAgda.Syntax.Parser.Literate
- isCodeLayerAgda.Syntax.Parser.Literate
- isCoFibrantSortAgda.TypeChecking.Irrelevance
- isCoinductiveAgda.TypeChecking.Rules.Data
- isCoinductiveProjectionAgda.Termination.Monad
- isConAgda.TypeChecking.Unquote
- isConNameAgda.Syntax.Scope.Base
- IsConstructorAgda.Syntax.Common
- isConstructorAgda.TypeChecking.Datatypes
- isContinuousAgda.Syntax.Common
- isCopatternLHSAgda.TypeChecking.Monad.Base
- iScopeAgda.TypeChecking.Monad.Base
- isCoveredAgda.TypeChecking.Coverage
- isCubicalSubtypeAgda.TypeChecking.Primitive.Cubical.Base
- IsDataAgda.Syntax.Internal
- IsDataModuleAgda.Syntax.Scope.Base
- isDataOrRecordAgda.TypeChecking.Datatypes
- isDataOrRecordTypeAgda.TypeChecking.Datatypes
- isDatatypeAgda.TypeChecking.Datatypes
- isDatatypeModuleAgda.Syntax.Scope.Monad
- isDebugPrintingAgda.TypeChecking.Monad.Debug
- isDecrAgda.Termination.Order
- isDefAgda.TypeChecking.Unquote
- isDefAccountAgda.Benchmarking
- isDefaultImportDirAgda.Syntax.Common
- isDefNameAgda.Syntax.Scope.Base
- IsDominatedAgda.Utils.Favorites
- isDontExpandLastAgda.TypeChecking.Monad.Base
- IsEllipsisAgda.Syntax.Concrete.Pattern
- isEllipsisAgda.Syntax.Concrete.Pattern
- IsEmptyAgda.Utils.Map1Agda.Utils.Set1
- IsEmptyAgda.TypeChecking.Monad.Base
- isEmptyAgda.Syntax.Common.PrettyAgda.Termination.SparseMatrix
- isEmptyFunctionAgda.TypeChecking.Monad.Base
- isEmptyObjectAgda.Compiler.JS.Compiler
- isEmptyTelAgda.TypeChecking.Empty
- IsEmptyTypeAgda.Interaction.Base
- isEmptyTypeAgda.TypeChecking.Empty
- isEnabledAgda.Compiler.Backend.Base
- isEqualityTypeAgda.Syntax.Internal
- isErasableAgda.Compiler.Treeless.Erase
- isErasedAgda.Syntax.Common
- isEtaConAgda.TypeChecking.Records
- isEtaExpandableAgda.TypeChecking.MetaVars
- isEtaOrCoinductiveRecordConstructorAgda.TypeChecking.Records
- isEtaRecordAgda.TypeChecking.Records
- isEtaRecordConstructorAgda.TypeChecking.Records
- isEtaRecordDefAgda.TypeChecking.Records
- isEtaRecordTypeAgda.TypeChecking.Records
- isEtaVarAgda.TypeChecking.Records
- isExpandLastAgda.TypeChecking.Monad.Base
- IsExprAgda.Syntax.Concrete.Operators.Parser
- IsExprAgda.Syntax.Common
- isExtendedLambdaAgda.TypeChecking.Monad.Base
- isExtendedLambdaNameAgda.TypeChecking.Monad.Base
- isFaceConstraintAgda.TypeChecking.MetaVars
- IsFamAgda.TypeChecking.Primitive.Cubical.Base
- IsFibrantAgda.Syntax.Internal.Univ
- IsFibrantAgda.Syntax.Internal.Univ
- isFibrantAgda.TypeChecking.Irrelevance
- isFibrant'Agda.TypeChecking.Irrelevance
- isFlexibleAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- IsFlexiblePatternAgda.TypeChecking.Rules.LHS
- isFlexiblePatternAgda.TypeChecking.Rules.LHS
- isFlexNodeAgda.TypeChecking.SizedTypes.WarshallSolver
- IsForcedAgda.TypeChecking.Monad.Base
- isForcedAgda.TypeChecking.Forcing
- IsFreeAgda.TypeChecking.Free.Reduce
- isFrozenAgda.TypeChecking.Monad.MetaVars
- isFunNameAgda.Syntax.Concrete.Definitions.Types
- isGeneralizableMetaAgda.TypeChecking.Monad.MetaVars
- isHoleAgda.Syntax.Concrete.Name
- IsIApplyAgda.TypeChecking.Coverage.Match
- iSignatureAgda.TypeChecking.Monad.Base
- isIncoherentAgda.Syntax.Common
- IsIndexAgda.TypeChecking.Positivity.Occurrence
- isInductiveRecordAgda.TypeChecking.Records
- IsInfixAgda.Syntax.Common
- isInfixAgda.Syntax.Concrete.Name
- isInftyNodeAgda.TypeChecking.SizedTypes.WarshallSolver
- isInlineFunAgda.TypeChecking.Monad.Signature
- isInModuleAgda.Syntax.Abstract.Name
- isInScopeAgda.Syntax.Concrete.Name
- isInsertedHiddenAgda.Syntax.Common
- isInsideDotPatternAgda.TypeChecking.Monad.Env
- IsInstanceAgda.Syntax.Common
- isInstanceAgda.Syntax.Common
- isInstanceConstraintAgda.TypeChecking.InstanceArgumentsAgda.TypeChecking.Monad.Constraints
- IsInstantiatedMetaAgda.TypeChecking.Monad.MetaVars
- isInstantiatedMetaAgda.TypeChecking.Monad.MetaVars
- isInstantiatedMeta'Agda.TypeChecking.Monad.MetaVars
- isInteractionMetaAgda.TypeChecking.Monad.MetaVars
- isInteractionMetaBAgda.TypeChecking.MetaVars
- isInterleavedDataAgda.Syntax.Concrete.Definitions.Types
- isInterleavedFunAgda.Syntax.Concrete.Definitions.Types
- isInternalAccountAgda.Benchmarking
- isIntervalAgda.TypeChecking.Telescope.Path
- isIOneAgda.Syntax.Internal
- isIrrelevantAgda.Syntax.Common
- isIrrelevantOrPropMAgda.TypeChecking.Irrelevance
- isJustAgda.Utils.MaybeAgda.Utils.Maybe.Strict
- isLabeledAgda.Syntax.Concrete.Pretty
- isLambdaHoleAgda.Syntax.Notation
- isLambdaNotationAgda.Syntax.Notation
- isLeChildModuleOfAgda.Syntax.Abstract.Name
- isLeftAgda.Utils.Either
- isLeParentModuleOfAgda.Syntax.Abstract.Name
- isLevelTypeAgda.TypeChecking.Level
- isLevelUniverseEnabledAgda.TypeChecking.Monad.Options
- IsLHSAgda.TypeChecking.Monad.Base
- IsListAgda.Utils.List1
- isLocalAgda.TypeChecking.Monad.Signature
- IsLockAgda.Syntax.Common
- isLtChildModuleOfAgda.Syntax.Abstract.Name
- isLtParentModuleOfAgda.Syntax.Abstract.Name
- IsMacroAgda.Syntax.Common
- isMacroAgda.TypeChecking.Monad.Base
- IsMainAgda.Compiler.BackendAgda.Compiler.CommonAgda.Syntax.Common
- IsMainAgda.Compiler.BackendAgda.Compiler.CommonAgda.Syntax.Common
- IsMetaAgda.TypeChecking.Reduce
- isMetaAgda.TypeChecking.Reduce
- isMetaTCWarningAgda.TypeChecking.Warnings
- isMetaWarningAgda.TypeChecking.Warnings
- isModCharAgda.Compiler.MAlonzo.Misc
- isModuleAccountAgda.Benchmarking
- isModuleFreeVarAgda.TypeChecking.Rules.Term
- isNameAgda.Interaction.BasicOps
- isNameInScopeAgda.Syntax.Scope.Base
- isNameInScopeUnqualifiedAgda.Syntax.Scope.Base
- isNameOfUnivAgda.TypeChecking.Monad.Builtin
- isNegInfAgda.Utils.Float
- isNegZeroAgda.Utils.Float
- isNeutralAgda.TypeChecking.MetaVars.Occurs
- isNewerThanAgda.Utils.FileName
- isNoAbsAgda.TypeChecking.Substitute.Class
- IsNoNameAgda.Syntax.Abstract.NameAgda.Syntax.Concrete.Name
- isNoNameAgda.Syntax.Abstract.NameAgda.Syntax.Concrete.Name
- IsNonEmptyAgda.Utils.Map1Agda.Utils.Set1
- isNonfixAgda.Syntax.Concrete.Name
- IsNotAgda.TypeChecking.Primitive.Cubical.Base
- isNothingAgda.Utils.MaybeAgda.Utils.Maybe.Strict
- IsNotLockAgda.Syntax.Common
- isoAgda.Utils.Lens
- isolatedNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
- IsOpaqueAgda.Syntax.Common
- isOpenMetaAgda.TypeChecking.Monad.MetaVars
- isOpenMixfixAgda.Syntax.Concrete.Name
- isOperatorAgda.Compiler.MAlonzo.PrettyAgda.Syntax.Abstract.NameAgda.Syntax.Concrete.Name
- isOrderAgda.Termination.Order
- iSourceAgda.TypeChecking.Monad.Base
- iSourceHashAgda.TypeChecking.Monad.Base
- isOverlappableAgda.Syntax.Common
- isOverlappingAgda.Syntax.Common
- isPathAgda.TypeChecking.Telescope
- IsPathConsAgda.TypeChecking.Rules.Data
- isPathConsAgda.TypeChecking.Datatypes
- isPathTypeAgda.Syntax.Internal
- IsPatSynAgda.TypeChecking.Monad.Base
- IsPatternAgda.Syntax.Common
- isPatternAgda.Syntax.Concrete
- IsPatternSynonymAgda.Syntax.Common
- isPosInfAgda.Utils.Float
- isPostfixAgda.Syntax.Concrete.Name
- isPosZeroAgda.Utils.Float
- isPragmaAgda.Syntax.Concrete
- isPrefixAgda.Syntax.Concrete.Name
- IsPrefixOfAgda.TypeChecking.Abstract
- isPrefixOfAgda.Utils.List1
- isPrefixOfAgda.TypeChecking.Abstract
- isPrimEqAgda.Syntax.Treeless
- isPrimitiveAgda.TypeChecking.Monad.Builtin
- IsPrimitiveModuleAgda.TypeChecking.Monad.Base.Types
- isPrimitiveModuleAgda.TypeChecking.Monad.State
- isProblemCompletelySolvedAgda.TypeChecking.Monad.Constraints
- isProblemSolvedAgda.TypeChecking.Monad.Constraints
- isProblemSolved'Agda.TypeChecking.Monad.Constraints
- isProjectionAgda.TypeChecking.Monad.Signature
- isProjection_Agda.TypeChecking.Monad.Signature
- isProjectionButNotCoinductiveAgda.Termination.Monad
- IsProjElimAgda.Syntax.Internal.Elim
- isProjElimAgda.Syntax.Internal.Elim
- IsProjPAgda.Syntax.Abstract.Name
- isProjPAgda.Syntax.Abstract.Name
- isPropAgda.Syntax.Internal
- isPropEnabledAgda.TypeChecking.Monad.Options
- isProperApplyElimAgda.Syntax.Internal.Elim
- isProperProjectionAgda.TypeChecking.Monad.Signature
- isProperSubmapOfAgda.Utils.Map1
- isProperSubmapOfByAgda.Utils.Map1
- isProperSubsetOfAgda.Utils.Set1
- isPropMAgda.TypeChecking.Irrelevance
- isQNameAgda.Interaction.BasicOps
- isQualifiedAgda.Syntax.Concrete.Name
- isQuantity0Agda.Syntax.Common
- isQuantityAttributeAgda.Syntax.Concrete.Attribute
- isQuantityωAgda.Syntax.Common
- isReconstructedAgda.TypeChecking.Monad.Base
- IsRecordAgda.Syntax.Internal
- isRecordAgda.TypeChecking.Records
- IsRecord_Agda.Syntax.Internal
- isRecordConstructorAgda.Syntax.Scope.MonadAgda.TypeChecking.Records
- IsRecordModuleAgda.Syntax.Scope.Base
- isRecordTypeAgda.TypeChecking.Records
- isRecursiveRecordAgda.TypeChecking.Records
- IsReducedAgda.TypeChecking.Monad.Base
- isReducedAgda.TypeChecking.Monad.Base
- isRelevanceAttributeAgda.Syntax.Concrete.Attribute
- isRelevantAgda.Syntax.Common
- isRelevantProjectionAgda.TypeChecking.Monad.Signature
- isRelevantProjection_Agda.TypeChecking.Monad.Signature
- isRemoteMetaAgda.TypeChecking.Monad.MetaVars
- isRightAgda.Utils.Either
- isSafeIntegerAgda.Utils.Float
- isShapeIrrelevantAgda.Syntax.Common
- isSingleIdentifierPAgda.Syntax.Concrete
- isSingletonAgda.Termination.SparseMatrix
- isSingletonRecordAgda.TypeChecking.Records
- isSingletonRecord'Agda.TypeChecking.Records
- isSingletonRecordModuloRelevanceAgda.TypeChecking.Records
- isSingletonTypeAgda.TypeChecking.Records
- isSingletonType'Agda.TypeChecking.Records
- isSingletonTypeModuloRelevanceAgda.TypeChecking.Records
- isSizeConstraintAgda.TypeChecking.SizedTypes
- isSizeConstraint_Agda.TypeChecking.SizedTypes
- isSizeNameTestAgda.TypeChecking.Monad.SizedTypes
- isSizeNameTestRawAgda.TypeChecking.Monad.SizedTypes
- isSizeProblemAgda.TypeChecking.SizedTypes
- IsSizeTypeAgda.TypeChecking.Monad.SizedTypes
- isSizeTypeAgda.TypeChecking.Monad.SizedTypes
- isSizeTypeTestAgda.TypeChecking.Monad.SizedTypes
- isSmallSortAgda.TypeChecking.Substitute
- isSolvingConstraintsAgda.TypeChecking.Monad.Constraints
- IsSortAgda.TypeChecking.Monad.Base
- isSortAgda.Syntax.Internal
- isSortJudgementAgda.TypeChecking.Monad.MetaVars
- isSortMetaAgda.TypeChecking.Monad.MetaVars
- isSortMeta_Agda.TypeChecking.Monad.MetaVars
- isSourceCodeWarningAgda.TypeChecking.Monad.Base
- isStaticFunAgda.TypeChecking.Monad.Signature
- IsStrictAgda.Syntax.Internal.Univ
- isStrictDataSortAgda.Syntax.Internal
- isStronglyRigidAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- isSubmapOfAgda.Utils.Map1
- isSubmapOfByAgda.Utils.Map1
- isSubscriptDigitAgda.Utils.Suffix
- isSubsetOfAgda.Utils.BoolSetAgda.Utils.Set1Agda.Utils.VarSet
- isSurrogateCodePointAgda.Utils.Char
- isTacticAttributeAgda.Syntax.Concrete.Attribute
- iStartAgda.Syntax.Position
- iStart'Agda.Syntax.Position
- isTimelessAgda.TypeChecking.Lock
- isTopAgda.TypeChecking.SizedTypes.Utils
- isTopLevelValueAgda.Compiler.JS.Compiler
- isTrivialPatternAgda.TypeChecking.Coverage.Match
- isTwoLevelEnabledAgda.TypeChecking.Monad.Options
- isTypeAgda.TypeChecking.Rules.Term
- isType'Agda.TypeChecking.Rules.Term
- IsType_Agda.TypeChecking.Monad.Base
- isType_Agda.TypeChecking.Rules.Term
- IsTypeCallAgda.TypeChecking.Monad.Base
- isTypeEqualToAgda.TypeChecking.Rules.Term
- isUnderscoreAgda.Syntax.Common
- isUnguardedAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- isUnifyStateSolvedAgda.TypeChecking.Rules.LHS.Unify.Types
- isUnnamedAgda.Syntax.Common
- isUnqualifiedAgda.Syntax.Concrete.Name
- isUnreachableAgda.Syntax.Treeless
- isUnsolvedWarningAgda.TypeChecking.Warnings
- isUnstableDefAgda.TypeChecking.Injectivity
- isUntypedBuiltinAgda.TypeChecking.Rules.Builtin
- isValidJSIdentAgda.Compiler.JS.Pretty
- isVarAgda.TypeChecking.CompiledClause.Compile
- IsVarSetAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- isWeaklyRigidAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- isWithFunctionAgda.TypeChecking.Monad.Base
- IsWithPAgda.Syntax.Concrete.Pattern
- isWithPAgda.Syntax.Concrete.Pattern
- isWithPatternAgda.Syntax.Concrete.Pattern
- isYesOverlapAgda.Syntax.Common
- isZeroNodeAgda.TypeChecking.SizedTypes.WarshallSolver
- itableCountsAgda.TypeChecking.Monad.Base
- itableTreeAgda.TypeChecking.Monad.Base
- ItemAgda.TypeChecking.Positivity
- ItemAgda.Utils.List1
- ItemAgda.Utils.List1
- iterateAgda.Utils.List1
- iterate'Agda.Utils.Function
- iterateSolverAgda.TypeChecking.SizedTypes.WarshallSolver
- iterateUntilAgda.Utils.Function
- iterateUntilMAgda.Utils.Function
- iterWhileAgda.Utils.Function
- iTopLevelModuleNameAgda.TypeChecking.Monad.Base
- iUserWarningsAgda.TypeChecking.Monad.Base
- IVarAgda.Utils.Haskell.Syntax
- iWarningsAgda.TypeChecking.Monad.Base
- IxAgda.Utils.IArrayAgda.Utils.SmallSet
- ixmapAgda.Utils.IArray
- IZeroAgda.Syntax.Internal