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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - _

_arrow | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_axiomConstTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_bindHoleNames | Agda.Syntax.Notation
_catchall | Agda.Syntax.Concrete.Definitions.Monad
_conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conProj | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_covChk | Agda.Syntax.Concrete.Definitions.Monad
_dataAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataPathCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_datarecPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataTransp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dataTranspIx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_dbraces | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_emptyIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_eqLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
_eqRight | Agda.TypeChecking.Rules.LHS.Unify.Types
_eqtLhs | Agda.Syntax.Internal
_eqtName | Agda.Syntax.Internal
_eqtParams | Agda.Syntax.Internal
_eqtRange | Agda.Syntax.Internal
_eqtRhs | Agda.Syntax.Internal
_eqtSort | Agda.Syntax.Internal
_eqtType | Agda.Syntax.Internal
_eqType | Agda.TypeChecking.Rules.LHS.Unify.Types
_exprFieldA | Agda.Syntax.Concrete
_exprModA | Agda.Syntax.Concrete
_fixityAssoc | Agda.Syntax.Common
_fixityLevel | Agda.Syntax.Common
_forallQ | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funCovering | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funExtLam | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funIsKanOp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funSplitTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funTerminates | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funTreeless | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_funWith | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_getSort | Agda.Syntax.Internal
_importDirModA | Agda.Syntax.Concrete
_itableCounts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_itableTree | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_kindPosCheck | Agda.Syntax.Concrete.Definitions.Types
_kindUniCheck | Agda.Syntax.Concrete.Definitions.Types
_lambda | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_leftIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_lhsIndexedSplit | Agda.TypeChecking.Rules.LHS.Problem
_lhsOutPat | Agda.TypeChecking.Rules.LHS.Problem
_lhsPartialSplit | Agda.TypeChecking.Rules.LHS.Problem
_lhsProblem | Agda.TypeChecking.Rules.LHS.Problem
_lhsTarget | Agda.TypeChecking.Rules.LHS.Problem
_lhsTel | Agda.TypeChecking.Rules.LHS.Problem
_libAbove | Agda.Interaction.Library.Base, Agda.Interaction.Library
_libDepends | Agda.Interaction.Library.Base, Agda.Interaction.Library
_libFile | Agda.Interaction.Library.Base, Agda.Interaction.Library
_libIncludes | Agda.Interaction.Library.Base, Agda.Interaction.Library
_libName | Agda.Interaction.Library.Base, Agda.Interaction.Library
_libPragmas | Agda.Interaction.Library.Base, Agda.Interaction.Library
_loneSigs | Agda.Syntax.Concrete.Definitions.Monad
_mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_nameFieldA | Agda.Syntax.Concrete
_nameId | Agda.Syntax.Concrete.Definitions.Monad
_nlmEqs | Agda.TypeChecking.Rewriting.NonLinMatch
_nlmSub | Agda.TypeChecking.Rewriting.NonLinMatch
_notaFixity | Agda.Syntax.Notation
_optAllowExec | Agda.Interaction.Options
_optAllowIncompleteMatch | Agda.Interaction.Options
_optAllowUnsolved | Agda.Interaction.Options
_optAutoInline | Agda.Interaction.Options
_optBacktrackingInstances | Agda.Interaction.Options
_optCaching | Agda.Interaction.Options
_optCallByName | Agda.Interaction.Options
_optCohesion | Agda.Interaction.Options
_optCompileMain | Agda.Interaction.Options
_optConfluenceCheck | Agda.Interaction.Options
_optCopatterns | Agda.Interaction.Options
_optCountClusters | Agda.Interaction.Options
_optCubical | Agda.Interaction.Options
_optCubicalCompatible | Agda.Interaction.Options
_optCumulativity | Agda.Interaction.Options
_optDoubleCheck | Agda.Interaction.Options
_optErasedMatches | Agda.Interaction.Options
_optEraseRecordParameters | Agda.Interaction.Options
_optErasure | Agda.Interaction.Options
_optEta | Agda.Interaction.Options
_optExactSplit | Agda.Interaction.Options
_optExperimentalIrrelevance | Agda.Interaction.Options
_optExperimentalLazyInstances | Agda.Interaction.Options
_optFastReduce | Agda.Interaction.Options
_optFirstOrder | Agda.Interaction.Options
_optFlatSplit | Agda.Interaction.Options
_optForcedArgumentRecursion | Agda.Interaction.Options
_optForcing | Agda.Interaction.Options
_optGuarded | Agda.Interaction.Options
_optGuardedness | Agda.Interaction.Options
_optHiddenArgumentPuns | Agda.Interaction.Options
_optImportSorts | Agda.Interaction.Options
_optInferAbsurdClauses | Agda.Interaction.Options
_optInjectiveTypeConstructors | Agda.Interaction.Options
_optInstanceSearchDepth | Agda.Interaction.Options
_optInversionMaxDepth | Agda.Interaction.Options
_optIrrelevantProjections | Agda.Interaction.Options
_optKeepCoveringClauses | Agda.Interaction.Options
_optKeepPatternVariables | Agda.Interaction.Options
_optLargeIndices | Agda.Interaction.Options
_optLevelUniverse | Agda.Interaction.Options
_optLoadPrimitives | Agda.Interaction.Options
_optOmegaInOmega | Agda.Interaction.Options
_optPatternMatching | Agda.Interaction.Options
_optPolarity | Agda.Interaction.Options
_optPositivityCheck | Agda.Interaction.Options
_optPostfixProjections | Agda.Interaction.Options
_optPrintPatternSynonyms | Agda.Interaction.Options
_optProfiling | Agda.Interaction.Options
_optProjectionLike | Agda.Interaction.Options
_optProp | Agda.Interaction.Options
_optQualifiedInstances | Agda.Interaction.Options
_optRequireUniqueMetaSolutions | Agda.Interaction.Options
_optRewriting | Agda.Interaction.Options
_optSafe | Agda.Interaction.Options
_optSaveMetas | Agda.Interaction.Options
_optShowGeneralized | Agda.Interaction.Options
_optShowIdentitySubstitutions | Agda.Interaction.Options
_optShowImplicit | Agda.Interaction.Options
_optShowIrrelevant | Agda.Interaction.Options
_optSizedTypes | Agda.Interaction.Options
_optSyntacticEquality | Agda.Interaction.Options
_optTerminationCheck | Agda.Interaction.Options
_optTerminationDepth | Agda.Interaction.Options
_optTwoLevel | Agda.Interaction.Options
_optUniverseCheck | Agda.Interaction.Options
_optUniversePolymorphism | Agda.Interaction.Options
_optUseUnicode | Agda.Interaction.Options
_optVerbose | Agda.Interaction.Options
_optWarningMode | Agda.Interaction.Options
_optWithoutK | Agda.Interaction.Options
_posChk | Agda.Syntax.Concrete.Definitions.Monad
_primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primOpaque | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primSortName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_primSortSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_problemCont | Agda.TypeChecking.Rules.LHS.Problem
_problemEqs | Agda.TypeChecking.Rules.LHS.Problem
_problemRestPats | Agda.TypeChecking.Rules.LHS.Problem
_qnameModA | Agda.Syntax.Concrete
_recAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recEtaEquality' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recNamedCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recPatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_recTerminates | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_rightIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
_scopeCurrent | Agda.Syntax.Scope.Base
_scopeFixities | Agda.Syntax.Scope.Base
_scopeInScope | Agda.Syntax.Scope.Base
_scopeInverseModule | Agda.Syntax.Scope.Base
_scopeInverseName | Agda.Syntax.Scope.Base
_scopeLocals | Agda.Syntax.Scope.Base
_scopeModules | Agda.Syntax.Scope.Base
_scopePolarities | Agda.Syntax.Scope.Base
_scopePrecedence | Agda.Syntax.Scope.Base
_scopeRecords | Agda.Syntax.Scope.Base
_scopeVarsToBind | Agda.Syntax.Scope.Base
_secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigRewriteRules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_termChk | Agda.Syntax.Concrete.Definitions.Monad
_terSizeDepth | Agda.Termination.Monad
_uniChk | Agda.Syntax.Concrete.Definitions.Monad
_unquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
_warn2Error | Agda.Interaction.Options.Warnings, Agda.Interaction.Options
_warningSet | Agda.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_WITH__ | 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
__IMPOSSIBLE__1 | Agda.Utils.Impossible
__UNREACHABLE__ | Agda.Utils.Impossible