IndexAgda-2.7.0.1
I
- IApplyAgda.Syntax.Internal.Elim
- IApplyPAgda.Syntax.Internal
- IApplyVarsAgda.TypeChecking.Telescope.Path
- iApplyVarsAgda.TypeChecking.Telescope.Path
- IArrayAgda.Utils.IArray
- iBuiltinAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- idempotentAgda.Termination.Termination
- IdentAgda.Syntax.ConcreteAgda.Utils.Haskell.Syntax
- identifierAgda.Syntax.Parser.LexActions
- IdentPAgda.Syntax.Concrete
- IdiomBracketsAgda.Syntax.Concrete
- IdiomTypeAgda.Syntax.Internal
- iDisplayFormsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- idPAgda.Utils.Permutation
- IdPartAgda.Syntax.Common
- IdSAgda.Syntax.InternalAgda.TypeChecking.Substitute
- idSAgda.TypeChecking.Substitute.Class
- idViewAsPathAgda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- iEndAgda.Syntax.Position
- IfAgda.Utils.TypeLevel
- IfAgda.Compiler.JS.SyntaxAgda.Utils.Haskell.Syntax
- ifBlockedAgda.TypeChecking.Reduce
- ifDirtyAgda.Utils.Update
- iFilePragmaOptionsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iFileTypeAgda.Compiler.BackendAgda.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.Null
- ifNullMAgda.Utils.Null
- iForeignCodeAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- ifTopLevelAndHighlightingLevelIsOrAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iFullHashAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IgnoreAbstractAgda.Interaction.Base
- IgnoreAbstractModeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ignoreAbstractModeAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- IgnoreSortsAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- iHighlightingAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ihnameAgda.Compiler.MAlonzo.Misc
- iImportedModulesAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iImportWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IInfoAgda.TypeChecking.Coverage.SplitClause
- iInsideScopeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ilamAgda.TypeChecking.Names
- iLengthAgda.Syntax.Position
- IllegalAgda.TypeChecking.Rules.LHS.UnifyAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
- IllegalDeclarationInDataDefinitionAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalHidingInPostfixProjectionAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalInstanceVariableInPatternSynonymAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalLetInTelescopeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalPatternInTelescopeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalRewriteRuleAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllegalRewriteRuleReasonAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- illegalRewriteWarningNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllformedAsClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllformedAsClause_Agda.Interaction.Options.Warnings
- IllformedProjectionPatternAbstractAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IllformedProjectionPatternConcreteAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- illiterateAgda.Syntax.Parser.Literate
- IllTypedPatternAfterWithAbstractionAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IMAgda.Interaction.Monad
- IMaxAgda.Syntax.Internal
- imaxAgda.TypeChecking.Primitive.Cubical.Base
- iMetaBindingsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IMinAgda.Syntax.Internal
- iminAgda.TypeChecking.Primitive.Cubical.Base
- imoduleMapAgda.Syntax.Scope.Monad
- iModuleNameAgda.Compiler.BackendAgda.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
- 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
- importModuleAgda.Utils.Haskell.Syntax
- 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.Compiler.BackendAgda.TypeChecking.Monad.Base
- ImpossibleErrorAgda.Interaction.ExitCode
- ImpossiblePragmaAgda.Syntax.Concrete
- impossibleTermAgda.Syntax.Internal
- impossibleTestAgda.ImpossibleTest
- impossibleTestReduceMAgda.ImpossibleTest
- impRenamingAgda.Syntax.Common
- InAgda.Syntax.Concrete.Operators.Parser
- In1Agda.Utils.Three
- In2Agda.Utils.Three
- In3Agda.Utils.Three
- inAbstractModeAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- inameMapAgda.Syntax.Scope.Monad
- incAgda.Utils.Warshall
- 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.Compiler.BackendAgda.TypeChecking.Monad.Signature
- inConcreteOrAbstractModeAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- IncorrectTypeForRewriteRelationAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IncorrectTypeForRewriteRelationReasonAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- IndexedClauseArgAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- indexWithDefaultAgda.Utils.List
- indicesAgda.Utils.IArray
- IndirectAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InductionAgda.Syntax.CommonAgda.Syntax.Common.Aspect
- InductionAgda.Syntax.Concrete
- InductionAndEtaAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InductionAndEtaAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InductiveAgda.Syntax.CommonAgda.Syntax.Common.Aspect
- INegAgda.Syntax.Internal
- inegAgda.TypeChecking.Primitive.Cubical.Base
- InfAgda.Syntax.Internal
- infAgda.TypeChecking.Positivity
- infallibleSortKitAgda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- InfectiveAgda.Interaction.Options
- InfectiveCoinfectiveAgda.Interaction.Options
- InfectiveCoinfectiveOptionAgda.Interaction.Options
- infectiveCoinfectiveOptionsAgda.Interaction.Options
- InfectiveImportAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InfectiveImport_Agda.Interaction.Options.Warnings
- inferAgda.TypeChecking.CheckInternal
- inferApplicationAgda.TypeChecking.Rules.Application
- InferDefAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InferExprAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- infimumAgda.Termination.Order
- InfiniteAgda.Utils.Warshall
- infiniteAgda.Utils.Warshall
- 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
- infoTauAgda.TypeChecking.Coverage.SplitClause
- infoTelAgda.TypeChecking.Coverage.SplitClause
- infoTel0Agda.TypeChecking.Coverage.SplitClause
- inFreshModuleIfFreeParamsAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- initFreeEnvAgda.TypeChecking.Free.Lazy
- initGraphAgda.Utils.Warshall
- InitialCandidatesAgda.Benchmarking
- initialiseCommandQueueAgda.Interaction.InteractionTop
- initialMetaIdAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- initPostScopeStateAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- initPreScopeStateAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- initsAgda.Utils.List1
- inits1Agda.Utils.List1
- initStateAgda.Compiler.BackendAgda.Syntax.Parser.MonadAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- InlineNoExactSplit_Agda.Interaction.Options.Warnings
- InlinePragmaAgda.Syntax.AbstractAgda.Syntax.Concrete
- InlineReductionsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InMutualAgda.Syntax.Concrete.Definitions.Types
- InMutualAgda.Syntax.Concrete.Definitions.Types
- inMutualBlockAgda.Compiler.BackendAgda.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.RangeMapAgda.Utils.SmallSetAgda.Utils.Trie
- insertAfterAgda.Compiler.JS.Compiler
- insertComparedAgda.Utils.Favorites
- insertDTAgda.TypeChecking.DiscrimTree
- InsertedAgda.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
- insertImplicitBindersTAgda.TypeChecking.Implicit
- insertImplicitBindersT1Agda.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.BiMap
- insertLookupWithKeyPreconditionAgda.Utils.BiMap
- insertMetaSetAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- insertMetaVarAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- insertMissingFieldsAgda.TypeChecking.Records
- insertMissingFieldsFailAgda.TypeChecking.Records
- insertMissingFieldsWarnAgda.TypeChecking.Records
- insertMutualBlockInfoAgda.Compiler.BackendAgda.TypeChecking.Monad.Mutual
- insertNamesAgda.TypeChecking.Rules.Def
- insertOldInteractionScopeAgda.Interaction.InteractionTop
- insertPatternsAgda.TypeChecking.Rules.Def
- insertPatternsLHSCoreAgda.TypeChecking.Rules.Def
- insertPreconditionAgda.Utils.BiMap
- insertTrailingArgsAgda.TypeChecking.Coverage
- insertWithAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.Trie
- insideAndOutsideAgda.Interaction.Highlighting.PreciseAgda.Utils.RangeMap
- insideDotPatternAgda.Compiler.BackendAgda.TypeChecking.Monad.Env
- InsideOperandCtxAgda.Syntax.Fixity
- InstanceAgda.Syntax.Common
- InstanceArgAgda.Syntax.Concrete
- InstanceArgVAgda.Syntax.Concrete.Operators.Parser
- InstanceArgWithExplicitArgAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceArgWithExplicitArg_Agda.Interaction.Options.Warnings
- InstanceBAgda.Syntax.Concrete
- InstanceBlockAgda.Syntax.Concrete.Definitions.Types
- instanceClassAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceDefAgda.Syntax.Common
- InstanceInfoAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceInfoAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceMetaAgda.Syntax.Info
- InstanceNoCandidateAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceNoOutputTypeNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceNoOutputTypeName_Agda.Interaction.Options.Warnings
- instanceOverlapAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstancePAgda.Syntax.Concrete
- InstancesAgda.Utils.ProfileOptions
- InstanceSearchAgda.Benchmarking
- InstanceSearchDepthExhaustedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceTableAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceTableAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceWithExplicitArgAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstanceWithExplicitArg_Agda.Interaction.Options.Warnings
- InstantiableAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstantiateAgda.TypeChecking.Reduce
- instantiateAgda.TypeChecking.Reduce
- instantiate'Agda.TypeChecking.Reduce
- InstantiatedAgda.Interaction.Base
- instantiateDefAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- instantiateDefinitionTypeAgda.TypeChecking.Rules.Decl
- InstantiateFullAgda.TypeChecking.Reduce
- instantiateFullAgda.TypeChecking.Reduce
- instantiateFull'Agda.TypeChecking.Reduce
- instantiateRewriteRuleAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- instantiateRewriteRulesAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- instantiateTelescopeAgda.TypeChecking.Telescope
- instantiateVarHeadsAgda.TypeChecking.Injectivity
- instantiateWhenAgda.TypeChecking.Reduce
- InstantiationAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstantiationAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- inStateAgda.Syntax.Parser.LexActions
- instBodyAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- instTelAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InstVAgda.Compiler.BackendAgda.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
- InteractionIdAgda.Syntax.Common
- InteractionIdAgda.Syntax.Common
- interactionIdAgda.Syntax.Common
- interactionIdToMetaIdAgda.Interaction.BasicOps
- InteractionMetaBoundariesAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InteractionMetaBoundaries_Agda.Interaction.Options.Warnings
- InteractionOutputCallbackAgda.Compiler.BackendAgda.Interaction.ResponseAgda.TypeChecking.Monad.Base
- InteractionPointAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InteractionPointAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InteractionPointsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InteractiveAgda.Compiler.BackendAgda.TypeChecking.Monad.BaseAgda.Utils.ProfileOptions
- InteractorAgda.Main
- interAssocWithAgda.Termination.SparseMatrix
- interestingCallAgda.Compiler.BackendAgda.TypeChecking.Monad.Trace
- interestingConstraintAgda.TypeChecking.Pretty.Constraint
- InterfaceAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InterfaceAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- internalErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- interpretAgda.Interaction.InteractionTop
- intersectionAgda.Utils.BoolSetAgda.Utils.SmallSetAgda.Utils.VarSet
- 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.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- intervalsToRangeAgda.Syntax.Position
- intervalToRangeAgda.Syntax.Position
- IntervalUnivAgda.Syntax.Internal
- intervalUnviewAgda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- intervalUnview'Agda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- IntervalViewAgda.Syntax.Internal
- intervalViewAgda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- intervalView'Agda.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- IntervalWithoutFileAgda.Syntax.Position
- intFilePathAgda.Interaction.FindFile
- intMapAgda.Utils.Warshall
- inTopContextAgda.Compiler.BackendAgda.TypeChecking.Monad.Context
- IntroAgda.Interaction.InteractionTop
- introTacticAgda.Interaction.BasicOps
- intSemiringAgda.Termination.Semiring
- IntSetAgda.Utils.IntSet.Infinite
- intSignatureAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- intToDoubleAgda.Utils.Float
- intViewAgda.Syntax.Treeless
- InvAgda.TypeChecking.Injectivity
- InvalidCatchallPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidCatchallPragma_Agda.Interaction.Options.Warnings
- InvalidCharacterLiteralAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidCharacterLiteral_Agda.Interaction.Options.Warnings
- InvalidConstructorAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidConstructor_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
- InvalidExtensionErrorAgda.Syntax.ParserAgda.Syntax.Parser.Monad
- InvalidFileNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidFileNameReasonAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidMeasureMutualAgda.Syntax.Concrete.Definitions.Errors
- InvalidNameAgda.Syntax.Concrete.Definitions.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidProjectionParameterAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidTerminationCheckPragmaAgda.Syntax.Concrete.DefinitionsAgda.Syntax.Concrete.Definitions.Errors
- InvalidTerminationCheckPragma_Agda.Interaction.Options.Warnings
- InvalidTypeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvalidTypeSortAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- InvariantAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- invariantAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.IntSet.Infinite
- InverseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- inverseApplyCohesionAgda.Syntax.Common
- inverseApplyModalityButNotQuantityAgda.Syntax.Common
- inverseApplyQuantityAgda.Syntax.Common
- inverseApplyRelevanceAgda.Syntax.Common
- inverseComposeAgda.Utils.POMonoid
- inverseComposeCohesionAgda.Syntax.Common
- inverseComposeModalityAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- InversionDepthReached_Agda.Interaction.Options.Warnings
- InversionMapAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- IOneAgda.Syntax.Internal
- iOpaqueBlocksAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iOpaqueNamesAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iOptionsUsedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IORefAgda.Utils.IORef
- IOTCMAgda.Interaction.Base
- IOTCMAgda.Interaction.Base
- IOTCM'Agda.Interaction.Base
- iPartialDefsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iPatternSynsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPBoundaryAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPBoundaryAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipBoundaryAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPBoundary'Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcClauseNoAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcClosureAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcQNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcTypeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipcWithSubAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPFace'Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPFace'Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IPNoClauseAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipRangeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- ipSolvedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IrrelevantAgda.Syntax.Common
- irrToNonStrictAgda.Syntax.Common
- IsAbstractAgda.Syntax.Common
- isAbsurdBodyAgda.Syntax.Internal
- isAbsurdLambdaNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isAbsurdPAgda.Syntax.Concrete
- isAbsurdPatternNameAgda.Syntax.Internal
- isAccessibleDefAgda.TypeChecking.Opacity
- isAHoleAgda.Syntax.Notation
- isAliasAgda.TypeChecking.Rules.Def
- 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
- isBelowAgda.Utils.Warshall
- isBenchmarkOnAgda.Utils.Benchmark
- isBinderAgda.Syntax.Notation
- isBinderPAgda.Syntax.Concrete
- isBinderUsedAgda.TypeChecking.Free
- isBlockedAgda.TypeChecking.Reduce
- isBlockedTermAgda.TypeChecking.MetaVars
- isBlockingConstraintAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- IsBoolAgda.Utils.Boolean
- isBoundaryConstraintAgda.TypeChecking.Pretty.Warning
- isBoundedAgda.TypeChecking.SizedTypes
- isBoundedProjVarAgda.TypeChecking.SizedTypes
- isBoundedSizeTypeAgda.TypeChecking.SizedTypes
- IsBuiltinAgda.Compiler.BackendAgda.Syntax.Builtin
- isBuiltinAgda.TypeChecking.Primitive.Base
- isBuiltinModuleAgda.Interaction.Options.Lenses
- isBuiltinModuleWithSafePostulatesAgda.Interaction.Options.Lenses
- isBuiltinNoDefAgda.Compiler.BackendAgda.Syntax.Builtin
- isCanonicalAgda.TypeChecking.Conversion
- isClosedAgda.Compiler.BackendAgda.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.TypeChecking.Datatypes
- isContinuousAgda.Syntax.Common
- isCopatternLHSAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iScopeAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Debug
- isDecrAgda.Termination.Order
- isDefAgda.TypeChecking.Unquote
- isDefAccountAgda.Benchmarking
- isDefaultImportDirAgda.Syntax.Common
- isDefNameAgda.Syntax.Scope.Base
- IsDominatedAgda.Utils.Favorites
- isDontExpandLastAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IsEllipsisAgda.Syntax.Concrete.Pattern
- isEllipsisAgda.Syntax.Concrete.Pattern
- IsEmptyAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isEmptyAgda.Syntax.Common.PrettyAgda.Termination.SparseMatrix
- isEmptyFunctionAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- IsExprAgda.Syntax.Concrete.Operators.Parser
- isExtendedLambdaAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isExtendedLambdaNameAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isFaceConstraintAgda.TypeChecking.MetaVars
- IsFamAgda.TypeChecking.Primitive.Cubical.Base
- IsFibrantAgda.Syntax.Internal.Univ
- IsFibrantAgda.Syntax.Internal.Univ
- isFibrantAgda.TypeChecking.Irrelevance
- isFlexibleAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- IsFlexiblePatternAgda.TypeChecking.Rules.LHS
- isFlexiblePatternAgda.TypeChecking.Rules.LHS
- isFlexNodeAgda.TypeChecking.SizedTypes.WarshallSolver
- IsForcedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isForcedAgda.TypeChecking.Forcing
- IsFreeAgda.TypeChecking.Free.Reduce
- isFrozenAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isFunNameAgda.Syntax.Concrete.Definitions.Types
- isGeneralizableMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isHoleAgda.Syntax.Concrete.Name
- IsIApplyAgda.TypeChecking.Coverage.Match
- iSignatureAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isInModuleAgda.Syntax.Abstract.Name
- isInScopeAgda.Syntax.Concrete.Name
- isInsertedHiddenAgda.Syntax.Common
- isInsideDotPatternAgda.Compiler.BackendAgda.TypeChecking.Monad.Env
- IsInstanceAgda.Syntax.Common
- isInstanceAgda.Syntax.Common
- isInstanceConstraintAgda.Compiler.BackendAgda.TypeChecking.InstanceArgumentsAgda.TypeChecking.Monad.Constraints
- IsInstantiatedMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isInstantiatedMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isInstantiatedMeta'Agda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isInteractionMetaAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Options
- IsLHSAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IsListAgda.Utils.List1
- isLocalAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- IsLockAgda.Syntax.Common
- isLtChildModuleOfAgda.Syntax.Abstract.Name
- isLtParentModuleOfAgda.Syntax.Abstract.Name
- IsMacroAgda.Syntax.Common
- isMacroAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.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
- isNonfixAgda.Syntax.Concrete.Name
- isNonStrictAgda.Syntax.Common
- 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.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isOpenMixfixAgda.Syntax.Concrete.Name
- isOperatorAgda.Compiler.MAlonzo.PrettyAgda.Syntax.Abstract.NameAgda.Syntax.Concrete.Name
- isOrderAgda.Termination.Order
- iSourceAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- iSourceHashAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isOverlappableAgda.Syntax.Common
- isOverlappingAgda.Syntax.Common
- isPathAgda.TypeChecking.Telescope
- IsPathConsAgda.TypeChecking.Rules.Data
- isPathConsAgda.TypeChecking.Datatypes
- isPathTypeAgda.Syntax.Internal
- IsPatSynAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isPatternAgda.Syntax.Concrete
- 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.Compiler.BackendAgda.TypeChecking.Monad.Builtin
- isPrimitiveModuleAgda.Interaction.Options.Lenses
- isProblemCompletelySolvedAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- isProblemSolvedAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- isProblemSolved'Agda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- isProjectionAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isProjection_Agda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isProjectionButNotCoinductiveAgda.Termination.Monad
- IsProjElimAgda.Syntax.Internal.Elim
- isProjElimAgda.Syntax.Internal.Elim
- IsProjPAgda.Syntax.Abstract.Name
- isProjPAgda.Syntax.Abstract.Name
- isPropEnabledAgda.Compiler.BackendAgda.TypeChecking.Monad.Options
- isProperApplyElimAgda.Syntax.Internal.Elim
- isProperProjectionAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isPropMAgda.TypeChecking.Irrelevance
- isQNameAgda.Interaction.BasicOps
- isQualifiedAgda.Syntax.Concrete.Name
- isQuantityAttributeAgda.Syntax.Concrete.Attribute
- isQuantityωAgda.Syntax.Common
- isReconstructedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IsRecordAgda.Syntax.Internal
- isRecordAgda.TypeChecking.Records
- isRecordConstructorAgda.TypeChecking.Records
- IsRecordModuleAgda.Syntax.Scope.Base
- isRecordTypeAgda.TypeChecking.Records
- isRecursiveRecordAgda.TypeChecking.Records
- IsReducedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isReducedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isRelevanceAttributeAgda.Syntax.Concrete.Attribute
- isRelevantAgda.Syntax.Common
- isRelevantProjectionAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isRelevantProjection_Agda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- isRemoteMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isRightAgda.Utils.Either
- isSafeIntegerAgda.Utils.Float
- 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.Compiler.BackendAgda.TypeChecking.Monad.SizedTypes
- isSizeNameTestRawAgda.Compiler.BackendAgda.TypeChecking.Monad.SizedTypes
- isSizeProblemAgda.TypeChecking.SizedTypes
- IsSizeTypeAgda.Compiler.BackendAgda.TypeChecking.Monad.SizedTypes
- isSizeTypeAgda.Compiler.BackendAgda.TypeChecking.Monad.SizedTypes
- isSizeTypeTestAgda.Compiler.BackendAgda.TypeChecking.Monad.SizedTypes
- isSmallSortAgda.TypeChecking.Substitute
- isSolvingConstraintsAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- IsSortAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isSortAgda.Syntax.Internal
- isSortJudgementAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isSortMetaAgda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isSortMeta_Agda.Compiler.BackendAgda.TypeChecking.Monad.MetaVars
- isSourceCodeWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isStaticFunAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- IsStrictAgda.Syntax.Internal.Univ
- isStrictDataSortAgda.Syntax.Internal
- isStronglyRigidAgda.TypeChecking.FreeAgda.TypeChecking.Free.Lazy
- isSublistOfAgda.Utils.List
- isSubscriptDigitAgda.Utils.Suffix
- isSubsetOfAgda.Utils.BoolSetAgda.Utils.VarSet
- isSurrogateCodePointAgda.Utils.Char
- isTacticAttributeAgda.Syntax.Concrete.Attribute
- iStartAgda.Syntax.Position
- isTimelessAgda.TypeChecking.Lock
- isTopAgda.TypeChecking.SizedTypes.Utils
- isTopLevelValueAgda.Compiler.JS.Compiler
- isTrivialPatternAgda.TypeChecking.Coverage.Match
- isTwoLevelEnabledAgda.Compiler.BackendAgda.TypeChecking.Monad.Options
- isTypeAgda.TypeChecking.Rules.Term
- isType'Agda.TypeChecking.Rules.Term
- IsType_Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- isType_Agda.TypeChecking.Rules.Term
- IsTypeCallAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- IsWithPAgda.Syntax.Concrete.Pattern
- isWithPAgda.Syntax.Concrete.Pattern
- isWithPatternAgda.Syntax.Concrete.Pattern
- isYesOverlapAgda.Syntax.Common
- isZeroNodeAgda.TypeChecking.SizedTypes.WarshallSolver
- itableCountsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- itableTreeAgda.Compiler.BackendAgda.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.Compiler.BackendAgda.TypeChecking.Monad.Base
- iUserWarningsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IVarAgda.Utils.Haskell.Syntax
- iWarningsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- IxAgda.Utils.IArrayAgda.Utils.SmallSet
- ixmapAgda.Utils.IArray
- IZeroAgda.Syntax.Internal