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

Index - _

_arrowAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_axiomConstTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_bindHoleNamesAgda.Syntax.Notation
_catchallAgda.Syntax.Concrete.Definitions.Monad
_conAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conArityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conErasedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conErasureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conForcedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conInlineAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conProjAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conSrcConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_covChkAgda.Syntax.Concrete.Definitions.Monad
_dataAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataIxsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataPathConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_datarecParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataTranspAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataTranspIxAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dbracesAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_emptyIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_eqLeftAgda.TypeChecking.Rules.LHS.Unify.Types
_eqRightAgda.TypeChecking.Rules.LHS.Unify.Types
_eqtLhsAgda.Syntax.Internal
_eqtNameAgda.Syntax.Internal
_eqtParamsAgda.Syntax.Internal
_eqtRhsAgda.Syntax.Internal
_eqtSortAgda.Syntax.Internal
_eqtTypeAgda.Syntax.Internal
_eqTypeAgda.TypeChecking.Rules.LHS.Unify.Types
_exprFieldAAgda.Syntax.Concrete
_exprModAAgda.Syntax.Concrete
_fixityAssocAgda.Syntax.Common
_fixityLevelAgda.Syntax.Common
_forallQAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_funClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funCoveringAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funExtLamAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funIsKanOpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funOpaqueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funSplitTreeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funTreelessAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funWithAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_getSortAgda.Syntax.Internal
_importDirModAAgda.Syntax.Concrete
_itableCountsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_itableTreeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_kindPosCheckAgda.Syntax.Concrete.Definitions.Types
_kindUniCheckAgda.Syntax.Concrete.Definitions.Types
_lambdaAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_leftIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_lhsIndexedSplitAgda.TypeChecking.Rules.LHS.Problem
_lhsOutPatAgda.TypeChecking.Rules.LHS.Problem
_lhsPartialSplitAgda.TypeChecking.Rules.LHS.Problem
_lhsProblemAgda.TypeChecking.Rules.LHS.Problem
_lhsTargetAgda.TypeChecking.Rules.LHS.Problem
_lhsTelAgda.TypeChecking.Rules.LHS.Problem
_libAboveAgda.Interaction.Library.Base, Agda.Interaction.Library
_libDependsAgda.Interaction.Library.Base, Agda.Interaction.Library
_libFileAgda.Interaction.Library.Base, Agda.Interaction.Library
_libIncludesAgda.Interaction.Library.Base, Agda.Interaction.Library
_libNameAgda.Interaction.Library.Base, Agda.Interaction.Library
_libPragmasAgda.Interaction.Library.Base, Agda.Interaction.Library
_loneSigsAgda.Syntax.Concrete.Definitions.Monad
_mvInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_nameFieldAAgda.Syntax.Concrete
_nameIdAgda.Syntax.Concrete.Definitions.Monad
_nlmEqsAgda.TypeChecking.Rewriting.NonLinMatch
_nlmSubAgda.TypeChecking.Rewriting.NonLinMatch
_notaFixityAgda.Syntax.Notation
_optAllowExecAgda.Interaction.Options
_optAllowIncompleteMatchAgda.Interaction.Options
_optAllowUnsolvedAgda.Interaction.Options
_optAutoInlineAgda.Interaction.Options
_optBacktrackingInstancesAgda.Interaction.Options
_optCachingAgda.Interaction.Options
_optCallByNameAgda.Interaction.Options
_optCohesionAgda.Interaction.Options
_optCompileMainAgda.Interaction.Options
_optConfluenceCheckAgda.Interaction.Options
_optCopatternsAgda.Interaction.Options
_optCountClustersAgda.Interaction.Options
_optCubicalAgda.Interaction.Options
_optCubicalCompatibleAgda.Interaction.Options
_optCumulativityAgda.Interaction.Options
_optDoubleCheckAgda.Interaction.Options
_optErasedMatchesAgda.Interaction.Options
_optEraseRecordParametersAgda.Interaction.Options
_optErasureAgda.Interaction.Options
_optEtaAgda.Interaction.Options
_optExactSplitAgda.Interaction.Options
_optExperimentalIrrelevanceAgda.Interaction.Options
_optFastReduceAgda.Interaction.Options
_optFirstOrderAgda.Interaction.Options
_optFlatSplitAgda.Interaction.Options
_optForcedArgumentRecursionAgda.Interaction.Options
_optForcingAgda.Interaction.Options
_optGuardedAgda.Interaction.Options
_optGuardednessAgda.Interaction.Options
_optHiddenArgumentPunsAgda.Interaction.Options
_optImportSortsAgda.Interaction.Options
_optInferAbsurdClausesAgda.Interaction.Options
_optInjectiveTypeConstructorsAgda.Interaction.Options
_optInstanceSearchDepthAgda.Interaction.Options
_optInversionMaxDepthAgda.Interaction.Options
_optIrrelevantProjectionsAgda.Interaction.Options
_optKeepCoveringClausesAgda.Interaction.Options
_optKeepPatternVariablesAgda.Interaction.Options
_optLargeIndicesAgda.Interaction.Options
_optLevelUniverseAgda.Interaction.Options
_optLoadPrimitivesAgda.Interaction.Options
_optOmegaInOmegaAgda.Interaction.Options
_optPatternMatchingAgda.Interaction.Options
_optPositivityCheckAgda.Interaction.Options
_optPostfixProjectionsAgda.Interaction.Options
_optPrintPatternSynonymsAgda.Interaction.Options
_optProfilingAgda.Interaction.Options
_optProjectionLikeAgda.Interaction.Options
_optPropAgda.Interaction.Options
_optQualifiedInstancesAgda.Interaction.Options
_optRequireUniqueMetaSolutionsAgda.Interaction.Options
_optRewritingAgda.Interaction.Options
_optSafeAgda.Interaction.Options
_optSaveMetasAgda.Interaction.Options
_optShowGeneralizedAgda.Interaction.Options
_optShowIdentitySubstitutionsAgda.Interaction.Options
_optShowImplicitAgda.Interaction.Options
_optShowIrrelevantAgda.Interaction.Options
_optSizedTypesAgda.Interaction.Options
_optSyntacticEqualityAgda.Interaction.Options
_optTerminationCheckAgda.Interaction.Options
_optTerminationDepthAgda.Interaction.Options
_optTwoLevelAgda.Interaction.Options
_optUniverseCheckAgda.Interaction.Options
_optUniversePolymorphismAgda.Interaction.Options
_optUseUnicodeAgda.Interaction.Options
_optVerboseAgda.Interaction.Options
_optWarningModeAgda.Interaction.Options
_optWithoutKAgda.Interaction.Options
_posChkAgda.Syntax.Concrete.Definitions.Monad
_primAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primClausesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primCompiledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primInvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primOpaqueAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primSortNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primSortSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_problemContAgda.TypeChecking.Rules.LHS.Problem
_problemEqsAgda.TypeChecking.Rules.LHS.Problem
_problemRestPatsAgda.TypeChecking.Rules.LHS.Problem
_qnameModAAgda.Syntax.Concrete
_recAbstrAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recCompAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recConHeadAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recEtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recEtaEquality'Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recFieldsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recInductionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recMutualAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recNamedConAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recParsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recPatternMatchingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recTerminatesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_rightIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_scopeCurrentAgda.Syntax.Scope.Base
_scopeFixitiesAgda.Syntax.Scope.Base
_scopeInScopeAgda.Syntax.Scope.Base
_scopeInverseModuleAgda.Syntax.Scope.Base
_scopeInverseNameAgda.Syntax.Scope.Base
_scopeLocalsAgda.Syntax.Scope.Base
_scopeModulesAgda.Syntax.Scope.Base
_scopePolaritiesAgda.Syntax.Scope.Base
_scopePrecedenceAgda.Syntax.Scope.Base
_scopeVarsToBindAgda.Syntax.Scope.Base
_secTelescopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigDefinitionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigInstancesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigRewriteRulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigSectionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_termChkAgda.Syntax.Concrete.Definitions.Monad
_terSizeDepthAgda.Termination.Monad
_uniChkAgda.Syntax.Concrete.Definitions.Monad
_unquoteNormaliseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_warn2ErrorAgda.Interaction.Options.Warnings, Agda.Interaction.Options
_warningSetAgda.Interaction.Options.Warnings, Agda.Interaction.Options
__CRASH_WHEN__Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
__DUMMY_DOM__Agda.Syntax.Internal
__DUMMY_LEVEL__Agda.Syntax.Internal
__DUMMY_SORT__Agda.Syntax.Internal
__DUMMY_TERM__Agda.Syntax.Internal
__DUMMY_TYPE__Agda.Syntax.Internal
__IMPOSSIBLE_VERBOSE__Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
__IMPOSSIBLE__Agda.Utils.Impossible
__UNREACHABLE__Agda.Utils.Impossible