Agda-2.6.2.2: 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 - C

C |
1 (Data Constructor) | Agda.Auto.Options
2 (Type/Class) | Agda.Utils.Cluster
cacheCurrentLog | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
CachedTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cachingStarts | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
CAction | Agda.Auto.Syntax
calc | Agda.Auto.NarrowingSearch
calcEqRState | Agda.Auto.Typecheck
CALConcat | Agda.Auto.Syntax
Call |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callBackend | Agda.Compiler.Backend
callByName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
CallComb | Agda.Termination.CallMatrix
callCompiler | Agda.Compiler.CallCompiler
callCompiler' | Agda.Compiler.CallCompiler
callGHC | Agda.Compiler.MAlonzo.Compiler
CallGraph |
1 (Type/Class) | Agda.Termination.CallGraph
2 (Data Constructor) | Agda.Termination.CallGraph
CallInfo |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callInfoCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callInfoRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callInfos | Agda.Termination.Monad
callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
callMain | Agda.Compiler.JS.Syntax
CallMatrix |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
CallMatrix' | Agda.Termination.CallMatrix
CallMatrixAug |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
callMatrixSet | Agda.Termination.CallGraph
CallPath |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
CallSite | Agda.Utils.CallStack
CallSiteFilter | Agda.Utils.CallStack
CallStack | Agda.Utils.CallStack
callStack | Agda.Utils.CallStack
CALNil | Agda.Auto.Syntax
camelTo2 | Agda.Interaction.JSON
Candidate |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CandidateKind | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateKind | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateOverlappable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
candidateType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
canHaveSuffixTest | Agda.Syntax.Scope.Monad
CannotCreateMissingClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CannotResolveAmbiguousPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
canonicalizeAbsolutePath | Agda.Utils.FileName
canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve
canonicalName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
canProject | Agda.TypeChecking.Substitute
CantGeneralizeOverSorts | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CantGeneralizeOverSorts_ | Agda.Interaction.Options.Warnings
CantInvert | Agda.TypeChecking.MetaVars
CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitBlocker | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitConIdx | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitConName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitFailures | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitGivenIdx | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cantSplitTel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend
Carrier | Agda.Utils.Zipper
Case |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.TypeChecking.CompiledClause
3 (Type/Class) | Agda.TypeChecking.CompiledClause
CaseContext | Agda.Interaction.MakeCase
caseEitherM | Agda.Utils.Either
CaseInfo |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseLazy | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseList | Agda.Utils.List
caseListM | Agda.Utils.List
caseListT | Agda.Utils.ListT
caseMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
caseMaybeM |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
CaseSplit | Agda.Syntax.Common
caseSplitSearch | Agda.Auto.CaseSplit
caseSplitSearch' | Agda.Auto.CaseSplit
caseToSeq | Agda.Compiler.Treeless.Uncase
CaseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
caseType | Agda.Syntax.Treeless, Agda.Compiler.Backend
castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve
castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve
cat | Agda.Utils.Pretty
Catchall | Agda.Syntax.Concrete.Definitions.Types
catchAll | Agda.TypeChecking.CompiledClause
catchAllBranch | Agda.TypeChecking.CompiledClause
CatchallClause | Agda.Interaction.Highlighting.Precise
CatchallPragma | Agda.Syntax.Concrete
catchallPragma | Agda.Syntax.Concrete.Definitions.Monad
catchAndPrintImpossible | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
catchConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
catchError_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term
CatchImpossible | Agda.Utils.Impossible
catchImpossible | Agda.Utils.Impossible
catchImpossibleJust | Agda.Utils.Impossible
CatchIO | Agda.Utils.IO
catchIO | Agda.Utils.IO
catchPatternErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
categorizedecl | Agda.Auto.Syntax
catMaybes |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
3 (Function) | Agda.Utils.List1
catMaybesMP | Agda.Utils.Monad
CC |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve
2 (Type/Class) | Agda.Compiler.MAlonzo.Compiler
CCContext | Agda.Compiler.MAlonzo.Compiler
ccContext | Agda.Compiler.MAlonzo.Compiler
CCEnv |
1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler
2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler
ccNameSupply | Agda.Compiler.MAlonzo.Compiler
CCT | Agda.Compiler.MAlonzo.Compiler
cdcont | Agda.Auto.Syntax
cddeffreevars | Agda.Auto.Syntax
cdname | Agda.Auto.Syntax
cdorigin | Agda.Auto.Syntax
cdtype | Agda.Auto.Syntax
CErased | Agda.Syntax.Common
CExp | Agda.Auto.Syntax
CFull | Agda.Syntax.Common
Change | Agda.Utils.Update
ChangeT | Agda.Utils.Update
Char |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
char | Agda.Utils.Pretty
chaseDisplayForms | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
checkAbsurdLambda | Agda.TypeChecking.Rules.Term
checkAlias | Agda.TypeChecking.Rules.Def
checkApplication | Agda.TypeChecking.Rules.Application
CheckArgs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkArguments | Agda.TypeChecking.Rules.Application
checkArguments_ | Agda.TypeChecking.Rules.Application
checkAxiom | Agda.TypeChecking.Rules.Decl
checkAxiom' | Agda.TypeChecking.Rules.Decl
CheckClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkClause | Agda.TypeChecking.Rules.Def
checkClauseLHS | Agda.TypeChecking.Rules.Def
checkClauseTelescopeBindings | Agda.Syntax.Translation.ReflectedToAbstract
checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl
checkCompilerPragmas | Agda.Compiler.JS.Compiler
CheckConfluence | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConfluenceOfClauses | Agda.TypeChecking.Rewriting.Confluence
checkConfluenceOfRules | Agda.TypeChecking.Rewriting.Confluence
CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConstructor | Agda.TypeChecking.Rules.Data
checkConstructorCount | Agda.Compiler.MAlonzo.HaskellTypes
CheckConstructorFitsIn | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkConstructorType | Agda.Compiler.MAlonzo.Compiler
checkCover | Agda.Compiler.MAlonzo.Compiler
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkDataDef | Agda.TypeChecking.Rules.Data
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDeclCached | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker
checkDisplayPragma | Agda.TypeChecking.Rules.Display
checkDomain | Agda.TypeChecking.Rules.Term
checkDontExpandLast | Agda.TypeChecking.Rules.Term
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkEarlierThan | Agda.TypeChecking.Lock
checkedMainDecl | Agda.Compiler.MAlonzo.Primitives
checkedMainDef | Agda.Compiler.MAlonzo.Primitives
CheckedMainFunctionDef |
1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives
2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives
CheckedTarget |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkeliminand | Agda.Auto.Typecheck
checkEmptyTel | Agda.TypeChecking.Empty
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker
checkExpr' | Agda.TypeChecking.Rules.Term
CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkExtendedLambda | Agda.TypeChecking.Rules.Term
checkForImportCycle | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkFunDef | Agda.TypeChecking.Rules.Def
checkFunDef' | Agda.TypeChecking.Rules.Def
CheckFunDefCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkFunDefS | Agda.TypeChecking.Rules.Def
checkGeneralize | Agda.TypeChecking.Rules.Decl
checkGeneralizeTelescope | Agda.TypeChecking.Rules.Term
checkIApplyConfluence | Agda.TypeChecking.IApplyConfluence
checkIApplyConfluence_ | Agda.TypeChecking.IApplyConfluence
checkImport | Agda.TypeChecking.Rules.Decl
checkIndexSorts | Agda.TypeChecking.Rules.Data
checkInjectivity | Agda.TypeChecking.Injectivity
checkInjectivity' | Agda.TypeChecking.Injectivity
checkInjectivity_ | Agda.TypeChecking.Rules.Decl
checkInternal | Agda.TypeChecking.CheckInternal
checkInternal' | Agda.TypeChecking.CheckInternal
checkInternalType' | Agda.TypeChecking.CheckInternal
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckK | Agda.Compiler.MAlonzo.Misc
checkKnownArgument | Agda.TypeChecking.Rules.Term
checkKnownArguments | Agda.TypeChecking.Rules.Term
CheckLambda | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLambda | Agda.TypeChecking.Rules.Term
checkLambda' | Agda.TypeChecking.Rules.Term
checkLazyMatch | Agda.TypeChecking.CompiledClause
checkLeftHandSide | Agda.TypeChecking.Rules.LHS
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLetBinding | Agda.TypeChecking.Rules.Term
checkLetBindings | Agda.TypeChecking.Rules.Term
checkLevel | Agda.TypeChecking.Rules.Term
CheckLHS |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLinearity | Agda.TypeChecking.MetaVars
checkLiteral | Agda.TypeChecking.Rules.Term
CheckLock | Agda.Interaction.Base
CheckLockedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkLockedVars | Agda.TypeChecking.Lock
checkLoneSigs | Agda.Syntax.Concrete.Definitions.Monad
checkMacroType | Agda.TypeChecking.Rules.Def
checkMeta | Agda.TypeChecking.Rules.Term
CheckMetaInst | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkMetaInst | Agda.TypeChecking.MetaVars
CheckMetaSolution | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkModuleArity | Agda.TypeChecking.Rules.Decl
checkModuleName | Agda.Interaction.FindFile
checkMutual | Agda.TypeChecking.Rules.Decl
checkNamedArg | Agda.TypeChecking.Rules.Term
CheckNamedWhere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkNoFixityInRenamingModule | Agda.Syntax.Scope.Monad
checkNoShadowing | Agda.Syntax.Scope.Monad
checkOpts | Agda.Interaction.Options
checkOrInferMeta | Agda.TypeChecking.Rules.Term
checkOverapplication | Agda.TypeChecking.Injectivity
checkPath | Agda.TypeChecking.Rules.Term
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPatternLinearity | Agda.Syntax.Abstract.Pattern
CheckPatternLinearityType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CheckPatternLinearityValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPiDomain | Agda.TypeChecking.Rules.Term
checkPiTelescope | Agda.TypeChecking.Rules.Term
checkpoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
CheckpointId |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkpointSubstitution | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
checkpointSubstitution' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
checkPositivity_ | Agda.TypeChecking.Rules.Decl
checkPostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch
checkPostponedLambda | Agda.TypeChecking.Rules.Term
checkPostponedLambda0 | Agda.TypeChecking.Rules.Term
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPragma | Agda.TypeChecking.Rules.Decl
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkPrimitive | Agda.TypeChecking.Rules.Decl
CheckProjAppToKnownPrincipalArg | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkProjAppToKnownPrincipalArg | Agda.TypeChecking.Rules.Application
CheckProjection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl
checkQuestionMark | Agda.TypeChecking.Rules.Term
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkRecDef | Agda.TypeChecking.Rules.Record
checkRecordExpression | Agda.TypeChecking.Rules.Term
checkRecordProjections | Agda.TypeChecking.Rules.Record
checkRecordUpdate | Agda.TypeChecking.Rules.Term
CheckResult |
1 (Type/Class) | Agda.Compiler.Backend, Agda.Interaction.Imports
2 (Data Constructor) | Agda.Compiler.Backend, Agda.Interaction.Imports
checkRewriteRule | Agda.TypeChecking.Rewriting
CheckRHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
checkRHS | Agda.TypeChecking.Rules.Def
checkSection | Agda.TypeChecking.Rules.Decl
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkSectionApplication | Agda.TypeChecking.Rules.Decl
checkSectionApplication' | Agda.TypeChecking.Rules.Decl
CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkSizeLtSat | Agda.TypeChecking.SizedTypes
checkSizeNeverZero | Agda.TypeChecking.SizedTypes
checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes
checkSolutionForMeta | Agda.TypeChecking.MetaVars
checkSort | Agda.TypeChecking.CheckInternal
checkSortOfSplitVar | Agda.TypeChecking.Rules.LHS
checkStrictlyPositive | Agda.TypeChecking.Positivity
checkSubtypeIsEqual | Agda.TypeChecking.MetaVars
checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality
checkSystemCoverage | Agda.TypeChecking.Rules.Def
checkTacticAttribute | Agda.TypeChecking.Rules.Term
CheckTargetType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkTelePiSort | Agda.TypeChecking.Sort
checkTelescope | Agda.TypeChecking.Rules.Term
checkTelescope' | Agda.TypeChecking.Rules.Term
checkTermination_ | Agda.TypeChecking.Rules.Decl
CheckType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkType | Agda.TypeChecking.CheckInternal
checkType' | Agda.TypeChecking.CheckInternal
checkTypeCheckingProblem | Agda.TypeChecking.Constraints
checkTypedBindings | Agda.TypeChecking.Rules.Term
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives
checkTypeOfMain' | Agda.Compiler.MAlonzo.Primitives
checkTypeSignature | Agda.TypeChecking.Rules.Decl
checkTypeSignature' | Agda.TypeChecking.Rules.Decl
checkUnderscore | Agda.TypeChecking.Rules.Term
checkUnquoteDecl | Agda.TypeChecking.Rules.Decl
checkUnquoteDef | Agda.TypeChecking.Rules.Decl
checkWhere | Agda.TypeChecking.Rules.Def
checkWithFunction | Agda.TypeChecking.Rules.Def
CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
checkWithRHS | Agda.TypeChecking.Rules.Def
Choice | Agda.Auto.NarrowingSearch
choice | Agda.TypeChecking.Unquote
choiceP | Agda.Utils.Parser.MemoisedCPS
choose | Agda.Auto.NarrowingSearch
ChooseEither | Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseFlex | Agda.TypeChecking.Rules.LHS.Problem
chooseHighlightingMethod | Agda.Interaction.Highlighting.Common
ChooseLeft | Agda.TypeChecking.Rules.LHS.Problem
choosePrioMeta | Agda.Auto.NarrowingSearch
ChooseRight | Agda.TypeChecking.Rules.LHS.Problem
chop | Agda.Utils.List
chopWhen | Agda.Utils.List
Chr | Agda.Utils.Pretty
Cl |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile
cl | Agda.TypeChecking.Names
cl' | Agda.TypeChecking.Names
ClashesViaRenaming | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashesViaRenaming_ | Agda.Interaction.Options.Warnings
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
classifyForeign | Agda.Compiler.MAlonzo.Pragmas
classifyPragma | Agda.Compiler.MAlonzo.Pragmas
classifyWarning | Agda.TypeChecking.Warnings
classifyWarnings | Agda.TypeChecking.Warnings
Clause |
1 (Type/Class) | Agda.Auto.Syntax
2 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
3 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions
4 (Type/Class) | Agda.Syntax.Internal
5 (Data Constructor) | Agda.Syntax.Internal
6 (Type/Class) | Agda.Syntax.Reflected
7 (Data Constructor) | Agda.Syntax.Reflected
8 (Type/Class) | Agda.Syntax.Abstract
9 (Data Constructor) | Agda.Syntax.Abstract
Clause' | Agda.Syntax.Abstract
clauseArgs | Agda.Syntax.Internal.Pattern
clauseBody | Agda.Syntax.Internal
clauseCatchall |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Abstract
clauseElims | Agda.Syntax.Internal.Pattern
clauseEllipsis | Agda.Syntax.Internal
clauseExact | Agda.Syntax.Internal
clauseFullRange | Agda.Syntax.Internal
clauseLHS | Agda.Syntax.Abstract
clauseLHSRange | Agda.Syntax.Internal
clausePats |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Reflected
clausePerm | Agda.Syntax.Internal.Pattern
clauseQName | Agda.TypeChecking.Rewriting.Clause
clauseRecursive | Agda.Syntax.Internal
clauseRHS |
1 (Function) | Agda.Syntax.Reflected
2 (Function) | Agda.Syntax.Abstract
ClausesPostChecks | Agda.TypeChecking.Rules.Def
clauseStrippedPats | Agda.Syntax.Abstract
clauseTel |
1 (Function) | Agda.Syntax.Internal
2 (Function) | Agda.Syntax.Reflected
clauseToRewriteRule | Agda.TypeChecking.Rewriting.Clause
clauseToSplitClause | Agda.TypeChecking.Coverage
clauseType | Agda.Syntax.Internal
clauseUnreachable | Agda.Syntax.Internal
clauseWhereDecls | Agda.Syntax.Abstract
ClauseZipper | Agda.Interaction.MakeCase
clBody | Agda.TypeChecking.CompiledClause.Compile
Clean | Agda.TypeChecking.Unquote
clean | Agda.Utils.Graph.AdjacencyMap.Unidirectional
cleanCachedLog | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
clearAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clearMetaListeners | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
clearRunningInfo | Agda.Interaction.EmacsCommand
clearWarning | Agda.Interaction.EmacsCommand
clEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ClockTime | Agda.Utils.Time
Clos |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
closed | Agda.TypeChecking.Free
ClosedLevel | Agda.Syntax.Internal
closedTerm | Agda.Compiler.MAlonzo.Compiler
closedTermToTreeless | Agda.Compiler.ToTreeless
closedTerm_ | Agda.Compiler.MAlonzo.Compiler
ClosedType | Agda.TypeChecking.Rules.Data
closeVerboseBracket | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
closeVerboseBracketException | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
closify | Agda.Auto.Syntax
Closure |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clPats | Agda.TypeChecking.CompiledClause.Compile
Cls | Agda.TypeChecking.CompiledClause.Compile
clScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
clSignature | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cluster | Agda.Utils.Cluster
cluster' | Agda.Utils.Cluster
clValue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
cmdToName | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
Cmd_abort | Agda.Interaction.Base
Cmd_autoAll | Agda.Interaction.Base
Cmd_autoOne | Agda.Interaction.Base
Cmd_compile | Agda.Interaction.Base
Cmd_compute | Agda.Interaction.Base
Cmd_compute_toplevel | Agda.Interaction.Base
Cmd_constraints | Agda.Interaction.Base
Cmd_context | Agda.Interaction.Base
Cmd_elaborate_give | Agda.Interaction.Base
Cmd_exit | Agda.Interaction.Base
Cmd_give | Agda.Interaction.Base
Cmd_goal_type | Agda.Interaction.Base
Cmd_goal_type_context | Agda.Interaction.Base
cmd_goal_type_context_and | Agda.Interaction.InteractionTop
Cmd_goal_type_context_check | Agda.Interaction.Base
Cmd_goal_type_context_infer | Agda.Interaction.Base
Cmd_helper_function | Agda.Interaction.Base
Cmd_highlight | Agda.Interaction.Base
Cmd_infer | Agda.Interaction.Base
Cmd_infer_toplevel | Agda.Interaction.Base
Cmd_intro | Agda.Interaction.Base
Cmd_load | Agda.Interaction.Base
cmd_load' | Agda.Interaction.InteractionTop
Cmd_load_highlighting_info | Agda.Interaction.Base
Cmd_make_case | Agda.Interaction.Base
Cmd_metas | Agda.Interaction.Base
Cmd_refine | Agda.Interaction.Base
Cmd_refine_or_intro | Agda.Interaction.Base
Cmd_search_about_toplevel | Agda.Interaction.Base
Cmd_show_module_contents | Agda.Interaction.Base
Cmd_show_module_contents_toplevel | Agda.Interaction.Base
Cmd_show_version | Agda.Interaction.Base
Cmd_solveAll | Agda.Interaction.Base
Cmd_solveOne | Agda.Interaction.Base
Cmd_tokenHighlighting | Agda.Interaction.Base
Cmd_why_in_scope | Agda.Interaction.Base
Cmd_why_in_scope_toplevel | Agda.Interaction.Base
CMFBlocked | Agda.Auto.Typecheck
CMFFlex | Agda.Auto.Typecheck
CMFlex |
1 (Type/Class) | Agda.Auto.Typecheck
2 (Data Constructor) | Agda.Auto.Typecheck
CMFSemi | Agda.Auto.Typecheck
CMode | Agda.Auto.Typecheck
Cmp | Agda.TypeChecking.SizedTypes.Syntax
cmp | Agda.TypeChecking.SizedTypes.Syntax
CmpElim | Agda.Interaction.Base
CmpEq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CmpInType | Agda.Interaction.Base
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CmpLevels | Agda.Interaction.Base
CmpSorts | Agda.Interaction.Base
CmpTeles | Agda.Interaction.Base
CmpTypes | Agda.Interaction.Base
CMRigid | Agda.Auto.Typecheck
CMSet |
1 (Type/Class) | Agda.Termination.CallMatrix
2 (Data Constructor) | Agda.Termination.CallMatrix
cmSet | Agda.Termination.CallMatrix
CoConName | Agda.Syntax.Scope.Base
Code | Agda.Syntax.Parser.Literate
code | Agda.Syntax.Parser.Lexer
CoDomain | Agda.Utils.TypeLevel
CoDomain' | Agda.Utils.TypeLevel
coerce | Agda.TypeChecking.Conversion
coerceAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend
coerceSize | Agda.TypeChecking.Conversion
coerceView | Agda.Syntax.Treeless, Agda.Compiler.Backend
Cohesion | Agda.Syntax.Common
CohesionAttribute | Agda.Syntax.Concrete.Attribute
cohesionAttributeTable | Agda.Syntax.Concrete.Attribute
CoinductionKit |
1 (Type/Class) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
2 (Data Constructor) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
coinductionKit | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
coinductionKit' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
CoInductive | Agda.Syntax.Common
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoInfectiveImport | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoInfectiveImport_ | Agda.Interaction.Options.Warnings
coinfectiveOptions | Agda.Interaction.Options
col | Agda.Termination.SparseMatrix
coldescr | Agda.Utils.Warshall
collapseDefault | Agda.Utils.WithDefault
collapseO | Agda.Termination.Order
Collection | Agda.Utils.Singleton
collectStats | Agda.TypeChecking.Serialise.Base
colon |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
cols | Agda.Termination.SparseMatrix
Column | Agda.Syntax.Parser.Monad
combineHashes | Agda.Utils.Hash
comma |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
Command |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
Command' | Agda.Interaction.Base
commandLineFlags | Agda.Compiler.Backend
CommandLineOptions | Agda.Interaction.Options
commandLineOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CommandM | Agda.Interaction.Base
commandMToIO | Agda.Interaction.InteractionTop
CommandQueue |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
commandQueue | Agda.Interaction.Base
commands | Agda.Interaction.Base
CommandState |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
Comment |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Type/Class) | Agda.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Compiler.JS.Syntax
4 (Data Constructor) | Agda.Syntax.Parser.Literate
5 (Data Constructor) | Agda.Interaction.Highlighting.Precise
commitInfo | Agda.VersionCommit
commonParentModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver
commonPrefix | Agda.Utils.List
commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver
commonSuffix | Agda.Utils.List
comp' | Agda.Auto.Typecheck
Compaction | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compactP | Agda.Utils.Permutation
compactS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Comparable | Agda.Utils.PartialOrd
comparable | Agda.Utils.PartialOrd
comparableOrd | Agda.Utils.PartialOrd
Compare | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
compareArgs | Agda.TypeChecking.Conversion
CompareAs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compareAs | Agda.TypeChecking.Conversion
compareAs' | Agda.TypeChecking.Conversion
compareAsDir | Agda.TypeChecking.Conversion
compareAtom | Agda.TypeChecking.Conversion
compareAtomDir | Agda.TypeChecking.Conversion
compareBelowMax | Agda.TypeChecking.SizedTypes
compareCohesion | Agda.TypeChecking.Conversion
CompareDirection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compareDom | Agda.TypeChecking.Conversion
compareElims | Agda.TypeChecking.Conversion
compareFavorites | Agda.Utils.Favorites
compareInterval | Agda.TypeChecking.Conversion
compareIrrelevant | Agda.TypeChecking.Conversion
compareLevel | Agda.TypeChecking.Conversion
compareMaxViews | Agda.TypeChecking.SizedTypes
compareOffset | Agda.TypeChecking.SizedTypes.Syntax
compareQuantity | Agda.TypeChecking.Conversion
compareRelevance | Agda.TypeChecking.Conversion
CompareResult | Agda.Utils.Favorites
compareSizes | Agda.TypeChecking.SizedTypes
compareSizeViews | Agda.TypeChecking.SizedTypes
compareSort | Agda.TypeChecking.Conversion
compareTerm | Agda.TypeChecking.Conversion
compareTerm' | Agda.TypeChecking.Conversion
compareTermOnFace | Agda.TypeChecking.Conversion
compareTermOnFace' | Agda.TypeChecking.Conversion
compareType | Agda.TypeChecking.Conversion
compareWithFavorites | Agda.Utils.Favorites
compareWithPol | Agda.TypeChecking.Conversion
Comparison | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compGlue | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
compHCompU | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
CompilationError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compile | Agda.TypeChecking.CompiledClause.Compile
compileAlt | Agda.Compiler.JS.Compiler
compileClauses | Agda.TypeChecking.CompiledClause.Compile
compileClauses' | Agda.TypeChecking.CompiledClause.Compile
Compiled |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
compiledClauseBody | Agda.TypeChecking.Substitute
CompiledClauses | Agda.TypeChecking.CompiledClause
CompiledClauses' | Agda.TypeChecking.CompiledClause
compiledcondecl | Agda.Compiler.MAlonzo.Compiler
compileDef | Agda.Compiler.Backend
compileDir | Agda.Compiler.Common
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compiledTypeSynonym | Agda.Compiler.MAlonzo.Compiler
CompilePragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
compilePrim |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
CompilerBackend | Agda.Interaction.Base
CompilerPragma |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
compileTerm | Agda.Compiler.JS.Compiler
compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile
CompKit |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
complement | Agda.Utils.SmallSet
complete |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function) | Agda.Termination.CallGraph
completeIter | Agda.Utils.Graph.AdjacencyMap.Unidirectional
completionStep | Agda.Termination.CallGraph
compose | Agda.TypeChecking.SizedTypes.Utils
composeCohesion | Agda.Syntax.Common
composeErased | Agda.Syntax.Common
composeFlexRig | Agda.TypeChecking.Free.Lazy
composeModality | Agda.Syntax.Common
composeP | Agda.Utils.Permutation
composePol | Agda.TypeChecking.Polarity
composeQuantity | Agda.Syntax.Common
composeRelevance | Agda.Syntax.Common
composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
composeVarOcc | Agda.TypeChecking.Free.Lazy
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional
ComposeZip | Agda.Utils.Zipper
ComposeZipper | Agda.Utils.Zipper
Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
computeEdges | Agda.TypeChecking.Positivity
computeElimHeadType | Agda.TypeChecking.Conversion
computeErasedConstructorArgs | Agda.Compiler.Treeless.Erase
computeFixitiesAndPolarities | Agda.Syntax.Scope.Monad
computeForcingAnnotations | Agda.TypeChecking.Forcing
computeIgnoreAbstract | Agda.Interaction.BasicOps
ComputeMode | Agda.Interaction.Base
computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
ComputeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences | Agda.TypeChecking.Positivity
computeOccurrences' | Agda.TypeChecking.Positivity
computePolarity | Agda.TypeChecking.Polarity
computeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve
computeUnsolvedInfo | Agda.Interaction.Highlighting.Generate
computeWrapInput | Agda.Interaction.BasicOps
Con |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Abstract
conAbstr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conApp | Agda.TypeChecking.Substitute
conArgs | Agda.TypeChecking.MetaVars.Occurs
ConArgType | Agda.TypeChecking.Positivity.Occurrence
conArity | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conBranches | Agda.TypeChecking.CompiledClause
conCase | Agda.TypeChecking.CompiledClause
Concat | Agda.TypeChecking.Positivity
concat | Agda.Utils.List1
Concat' | Agda.TypeChecking.Positivity
concatargs | Agda.Auto.CaseSplit
concatListT | Agda.Utils.ListT
conComp | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConcreteDef | Agda.Syntax.Common
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConcreteNames | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
concreteNamesInScope | Agda.Syntax.Scope.Base
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract
conData | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conDataRecord | Agda.Syntax.Internal
ConDecl |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Utils.Haskell.Syntax
condecl | Agda.Compiler.MAlonzo.Compiler
Condition | Agda.TypeChecking.MetaVars
conErased | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conFields | Agda.Syntax.Internal
configAgdaLibFiles | Agda.Interaction.Library.Base, Agda.Interaction.Library
configRoot | Agda.Interaction.Library.Base, Agda.Interaction.Library
Confirmed | Agda.Syntax.Parser.Monad
confirmLayout | Agda.Syntax.Parser.Layout
ConfluenceCheck | Agda.Interaction.Options
ConfluenceProblem | Agda.Interaction.Highlighting.Precise
conForced | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConGraph | Agda.TypeChecking.SizedTypes.WarshallSolver
ConGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
ConHead |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
conhqn | Agda.Compiler.MAlonzo.Misc
conInd | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conInductive | Agda.Syntax.Internal
ConInfo | Agda.Syntax.Internal
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Conj | Agda.TypeChecking.Conversion
ConK | Agda.Compiler.MAlonzo.Misc
conKindOfName | Agda.Syntax.Scope.Base
conKindOfName' | Agda.Syntax.Scope.Base
ConName | Agda.Syntax.Scope.Base
conName | Agda.Syntax.Internal
ConnectHandle | Agda.Auto.NarrowingSearch
connectInteractionPoint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
ConOCon | Agda.Syntax.Common
ConOfAbs | Agda.Syntax.Translation.AbstractToConcrete
ConORec | Agda.Syntax.Common
ConOrigin | Agda.Syntax.Common
ConOSplit | Agda.Syntax.Common
ConOSystem | Agda.Syntax.Common
ConP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Abstract
conPars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConPatEager | Agda.Syntax.Info
ConPatInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
conPatInfo | Agda.Syntax.Info
ConPatLazy |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
conPatLazy | Agda.Syntax.Info
conPatOrigin | Agda.Syntax.Info
ConPatternInfo |
1 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
conPFallThrough | Agda.Syntax.Internal
conPInfo | Agda.Syntax.Internal
conPLazy | Agda.Syntax.Internal
conPRecord | Agda.Syntax.Internal
conProj | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conPType | Agda.Syntax.Internal
Cons |
1 (Data Constructor) | Agda.Utils.IndexedList
2 (Data Constructor) | Agda.Interaction.EmacsCommand
cons | Agda.Utils.List1
consecutiveAndSeparated | Agda.Syntax.Position
ConsHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
consListT | Agda.Utils.ListT
ConsMap0 | Agda.Utils.TypeLevel
ConsMap1 | Agda.Utils.TypeLevel
consMListT | Agda.Utils.ListT
consOfHIT | Agda.TypeChecking.Datatypes
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
consS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
Const |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
3 (Data Constructor) | Agda.Auto.Syntax
Constant | Agda.Utils.TypeLevel
Constant0 | Agda.Utils.TypeLevel
Constant1 | Agda.Utils.TypeLevel
ConstDef |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
Constr |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
constrainedPrims | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
Constraint |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax
3 (Type/Class) | Agda.Utils.Warshall
4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Constraint' | Agda.TypeChecking.SizedTypes.Syntax
constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver
constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
constraintMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
constraintProblems | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Constraints |
1 (Type/Class) | Agda.Utils.Warshall
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConstraintStatus | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
constraintUnblocker | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConstRef | Agda.Auto.Syntax
Constructor |
1 (Data Constructor) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
4 (Type/Class) | Agda.Syntax.Abstract
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ConstructorBlock | Agda.Syntax.Concrete.Definitions.Types
constructorCoverageCode | Agda.Compiler.MAlonzo.Compiler
constructorForm |
1 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
2 (Function) | Agda.TypeChecking.Reduce.Monad
constructorForm' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
constructorImpossible | Agda.Auto.Typecheck
ConstructorInfo | Agda.TypeChecking.Datatypes
ConstructorName | Agda.Syntax.Scope.Base
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
constructorTagModifier | Agda.Interaction.JSON
constructPats | Agda.Auto.Convert
constructs | Agda.TypeChecking.Rules.Data
constTranspAxiom | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
containsAbsurdPattern | Agda.Syntax.Abstract.Pattern
containsAPattern | Agda.Syntax.Abstract.Pattern
containsAsPattern | Agda.Syntax.Abstract.Pattern
contains_constructor | Agda.Auto.Convert
content | Agda.TypeChecking.CompiledClause
contentsFieldName | Agda.Interaction.JSON
Context | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ContextLet | Agda.Interaction.Base
contextOfMeta | Agda.Interaction.BasicOps
contextSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
ContextVar | Agda.Interaction.Base
Continuous | Agda.Syntax.Common
continuous | Agda.Syntax.Position
continuousPerLine | Agda.Syntax.Position
Contravariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
conUseSizeLt | Agda.Termination.Monad
convError | Agda.TypeChecking.Conversion
Conversion | Agda.Auto.Convert
Convert | Agda.Interaction.Highlighting.Precise
convert |
1 (Function) | Agda.Interaction.Highlighting.Precise
2 (Function) | Agda.Auto.Convert
convertGuards | Agda.Compiler.Treeless.GuardsToPrims
CopatternMatching | Agda.Syntax.Common
CopatternMatchingAllowed | Agda.Syntax.Common
copatternMatchingAllowed | Agda.Syntax.Common
CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
copatternsNotImplemented | Agda.Auto.Convert
copyarg | Agda.Auto.Typecheck
copyDirContent | Agda.Utils.IO.Directory
copyRTEModules | Agda.Compiler.MAlonzo.Compiler
copyScope | Agda.Syntax.Scope.Monad
copyTerm | Agda.Syntax.Internal.Generic
CosplitCatchall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CosplitNoRecordType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CosplitNoTarget | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Cost |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
costAbsurdLam | Agda.Auto.SearchControl
costAddVarDepth | Agda.Auto.CaseSplit
costAppConstructor | Agda.Auto.SearchControl
costAppConstructorSingle | Agda.Auto.SearchControl
costAppExtraRef | Agda.Auto.SearchControl
costAppHint | Agda.Auto.SearchControl
costAppHintUsed | Agda.Auto.SearchControl
costAppRecCall | Agda.Auto.SearchControl
costAppRecCallUsed | Agda.Auto.SearchControl
costAppVar | Agda.Auto.SearchControl
costAppVarUsed | Agda.Auto.SearchControl
costCaseSplitHigh | Agda.Auto.CaseSplit
costCaseSplitLow | Agda.Auto.CaseSplit
costCaseSplitVeryHigh | Agda.Auto.CaseSplit
costEqCong | Agda.Auto.SearchControl
costEqEnd | Agda.Auto.SearchControl
costEqStep | Agda.Auto.SearchControl
costEqSym | Agda.Auto.SearchControl
costIncrease | Agda.Auto.SearchControl
costInferredTypeUnkown | Agda.Auto.SearchControl
costIotaStep | Agda.Auto.SearchControl
costLam | Agda.Auto.SearchControl
costLamUnfold | Agda.Auto.SearchControl
costPi | Agda.Auto.SearchControl
costSort | Agda.Auto.SearchControl
costUnification | Agda.Auto.SearchControl
costUnificationIf | Agda.Auto.SearchControl
costUnificationOccurs | Agda.Auto.SearchControl
count | Agda.Utils.Bag
CountPatternVars | Agda.Syntax.Internal.Pattern
countPatternVars | Agda.Syntax.Internal.Pattern
countWithArgs | Agda.TypeChecking.With
Covariant | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
CoverageCheck | Agda.Syntax.Common
coverageCheck |
1 (Function) | Agda.Syntax.Concrete.Definitions.Types
2 (Function) | Agda.TypeChecking.Coverage
coverageCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
CoverageIssue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoverageIssue_ | Agda.Interaction.Options.Warnings
CoverageNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
CoverageNoExactSplit_ | Agda.Interaction.Options.Warnings
CoverageProblem | Agda.Interaction.Highlighting.Precise
Covering |
1 (Type/Class) | Agda.TypeChecking.Coverage
2 (Data Constructor) | Agda.TypeChecking.Coverage
coveringRange | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
CoverK | Agda.Compiler.MAlonzo.Misc
covSplitArg | Agda.TypeChecking.Coverage
covSplitClauses | Agda.TypeChecking.Coverage
CPatternLike | Agda.Syntax.Concrete.Pattern
CPC | Agda.TypeChecking.Rules.Def
cpcPartialSplits | Agda.TypeChecking.Rules.Def
CPUTime |
1 (Type/Class) | Agda.Utils.Time
2 (Data Constructor) | Agda.Utils.Time
createMetaInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
createMetaInfo' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
createModule | Agda.Syntax.Scope.Monad
crInterface | Agda.Compiler.Backend, Agda.Interaction.Imports
crMode | Agda.Compiler.Backend, Agda.Interaction.Imports
crModuleInfo | Agda.Interaction.Imports
crSource | Agda.Interaction.Imports
crWarnings | Agda.Compiler.Backend, Agda.Interaction.Imports
CSAbsurd | Agda.Auto.CaseSplit
CSCtx | Agda.Auto.CaseSplit
CSOmittedArg | Agda.Auto.CaseSplit
CSPat | Agda.Auto.CaseSplit
CSPatConApp | Agda.Auto.CaseSplit
CSPatExp | Agda.Auto.CaseSplit
CSPatI | Agda.Auto.CaseSplit
CSPatVar | Agda.Auto.CaseSplit
CSWith | Agda.Auto.CaseSplit
CTChar | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTData | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTFloat | Agda.Syntax.Treeless, Agda.Compiler.Backend
cthandles | Agda.Auto.NarrowingSearch
CTInt | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTNat | Agda.Syntax.Treeless, Agda.Compiler.Backend
ctparent | Agda.Auto.NarrowingSearch
ctpriometa | Agda.Auto.NarrowingSearch
CTQName | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTrans | Agda.TypeChecking.SizedTypes.Syntax
CTree |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
cTreeless | Agda.Syntax.Treeless, Agda.Compiler.Backend
CTString | Agda.Syntax.Treeless, Agda.Compiler.Backend
ctsub | Agda.Auto.NarrowingSearch
Ctx | Agda.Auto.Syntax
CType | Agda.TypeChecking.Rules.Data
Cubical |
1 (Data Constructor) | Agda.Syntax.Common
2 (Type/Class) | Agda.Syntax.Common
curAgdaMod | Agda.Compiler.MAlonzo.Misc
curDefs | Agda.Compiler.Common
curHsMod | Agda.Compiler.MAlonzo.Misc
curIF | Agda.Compiler.Common
curIsMainModule | Agda.Compiler.MAlonzo.Misc
curMName | Agda.Compiler.Common
curOutFile | Agda.Compiler.MAlonzo.Compiler
curOutFileAndDir | Agda.Compiler.MAlonzo.Compiler
CurrentAccount | Agda.Utils.Benchmark
currentAccount | Agda.Utils.Benchmark
currentCxt | Agda.TypeChecking.Names
CurrentFile |
1 (Type/Class) | Agda.Interaction.Base
2 (Data Constructor) | Agda.Interaction.Base
currentFileArgs | Agda.Interaction.Base
currentFilePath | Agda.Interaction.Base
currentFileStamp | Agda.Interaction.Base
CurrentInput | Agda.Syntax.Parser.Alex
currentModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
currentModuleNameHash | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
currentOrFreshMutualBlock | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
CurrentTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
curriedApply | Agda.Compiler.JS.Substitution
curriedLambda | Agda.Compiler.JS.Substitution
curryAt | Agda.TypeChecking.Records
Currying | Agda.Utils.TypeLevel
currys | Agda.Utils.TypeLevel
CutOff |
1 (Type/Class) | Agda.Termination.CutOff
2 (Data Constructor) | Agda.Termination.CutOff
cxtSubst | Agda.TypeChecking.Names
cycle | Agda.Utils.List1
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad