C | |
1 (Type/Class) | Agda.Utils.Cluster |
2 (Data Constructor) | Agda.Auto.Options |
cacheCurrentLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CachedTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cachingStarts | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
callBackend | Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
callInfoCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
callInfoRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
callInfos | Agda.Termination.Monad |
callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
CALNil | Agda.Auto.Syntax |
Candidate | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateEti | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateOverlappable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
canProject | Agda.TypeChecking.Substitute |
CantInvert | Agda.TypeChecking.MetaVars |
CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitConIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitConName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitFailures | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitGivenIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cArgUsage | Agda.Syntax.Treeless, Agda.Compiler.Backend |
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 |
caseList | 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 |
castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve |
castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve |
cat | Agda.Utils.Pretty |
catchAll | Agda.TypeChecking.CompiledClause |
catchAllBranch | Agda.TypeChecking.CompiledClause |
CatchallClause | Agda.Interaction.Highlighting.Precise |
CatchallPragma | Agda.Syntax.Concrete |
catchConstraint | Agda.TypeChecking.Constraints |
catchError | Agda.Utils.Except |
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term |
catchImpossible | Agda.Utils.Impossible |
CatchIO | Agda.Utils.IO |
catchIO | Agda.Utils.IO |
categorizedecl | Agda.Auto.Syntax |
catMaybes | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
CC | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Solve |
2 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
CCContext | Agda.Compiler.MAlonzo.Compiler |
ccCxt | Agda.Compiler.MAlonzo.Compiler |
CCEnv | |
1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
ccNameSupply | Agda.Compiler.MAlonzo.Compiler |
cdcont | Agda.Auto.Syntax |
cddeffreevars | Agda.Auto.Syntax |
cdecl | Agda.Compiler.MAlonzo.Compiler |
cdname | Agda.Auto.Syntax |
cdorigin | Agda.Auto.Syntax |
cdtype | Agda.Auto.Syntax |
CExp | Agda.Auto.Syntax |
chainl | Agda.Utils.Parser.ReadP |
chainl1 | Agda.Utils.Parser.ReadP |
chainr | Agda.Utils.Parser.ReadP |
chainr1 | Agda.Utils.Parser.ReadP |
Change | Agda.Utils.Update |
Char | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
char | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Utils.Parser.ReadP |
chaseDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
chaseMsg | Agda.Interaction.Imports |
checkAbsurdLambda | Agda.TypeChecking.Rules.Term |
checkAlias | Agda.TypeChecking.Rules.Def |
checkApplication | Agda.TypeChecking.Rules.Term |
CheckArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkArguments | Agda.TypeChecking.Rules.Term |
checkArguments' | Agda.TypeChecking.Rules.Term |
checkArguments_ | Agda.TypeChecking.Rules.Term |
checkAxiom | Agda.TypeChecking.Rules.Decl |
checkCandidates | Agda.TypeChecking.InstanceArguments |
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkClause | Agda.TypeChecking.Rules.Def |
checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl |
checkCompilerPragmas | Agda.Compiler.JS.Compiler |
CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkConstructor | Agda.TypeChecking.Rules.Data |
checkConstructorApplication | Agda.TypeChecking.Rules.Term |
checkConstructorCount | Agda.Compiler.MAlonzo.HaskellTypes |
checkConstructorType | Agda.Compiler.MAlonzo.Compiler |
checkCover | Agda.Compiler.MAlonzo.Compiler |
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
checkDontExpandLast | Agda.TypeChecking.Rules.Term |
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkDotPattern | Agda.TypeChecking.Rules.LHS |
checkeliminand | Agda.Auto.Typecheck |
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkExtendedLambda | Agda.TypeChecking.Rules.Term |
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkFunDef | Agda.TypeChecking.Rules.Def |
checkFunDef' | Agda.TypeChecking.Rules.Def |
checkFunDefS | Agda.TypeChecking.Rules.Def |
checkHeadApplication | Agda.TypeChecking.Rules.Term |
checkImport | Agda.TypeChecking.Rules.Decl |
checkInjectivity | Agda.TypeChecking.Injectivity |
checkInjectivity_ | Agda.TypeChecking.Rules.Decl |
checkInternal | Agda.TypeChecking.CheckInternal |
checkInternal' | Agda.TypeChecking.CheckInternal |
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkKnownArgument | Agda.TypeChecking.Rules.Term |
checkKnownArguments | Agda.TypeChecking.Rules.Term |
CheckLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkLambda | Agda.TypeChecking.Rules.Term |
checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
checkLeftoverDotPatterns | Agda.TypeChecking.Rules.LHS |
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkLetBinding | Agda.TypeChecking.Rules.Term |
checkLetBindings | Agda.TypeChecking.Rules.Term |
CheckLHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
checkLHS | Agda.TypeChecking.Rules.LHS |
checkLinearity | Agda.TypeChecking.MetaVars |
checkLiteral | Agda.TypeChecking.Rules.Term |
checkMacroType | Agda.TypeChecking.Rules.Def |
checkMeta | Agda.TypeChecking.Rules.Term |
checkModuleArity | Agda.TypeChecking.Rules.Decl |
checkModuleName | Agda.Interaction.FindFile |
checkMutual | Agda.TypeChecking.Rules.Decl |
checkNamedArg | Agda.TypeChecking.Rules.Term |
checkOpts | Agda.Interaction.Options |
checkOrInferMeta | Agda.TypeChecking.Rules.Term |
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPiTelescope | Agda.TypeChecking.Rules.Term |
checkPositivity_ | Agda.TypeChecking.Rules.Decl |
checkPostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch |
checkPostponedLambda | Agda.TypeChecking.Rules.Term |
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPragma | Agda.TypeChecking.Rules.Decl |
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPrimitive | Agda.TypeChecking.Rules.Decl |
checkProjApp | Agda.TypeChecking.Rules.Term |
CheckProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl |
checkQuestionMark | Agda.TypeChecking.Rules.Term |
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkRecDef | Agda.TypeChecking.Rules.Record |
checkRecordExpression | Agda.TypeChecking.Rules.Term |
checkRecordProjections | Agda.TypeChecking.Rules.Record |
checkRecordUpdate | Agda.TypeChecking.Rules.Term |
CheckRHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
checkRHS | Agda.TypeChecking.Rules.Def |
checkSection | Agda.TypeChecking.Rules.Decl |
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkSectionApplication | Agda.TypeChecking.Rules.Decl |
checkSectionApplication' | Agda.TypeChecking.Rules.Decl |
checkSizeIndex | Agda.TypeChecking.Polarity |
CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkSizeLtSat | Agda.TypeChecking.SizedTypes |
checkSizeNeverZero | Agda.TypeChecking.SizedTypes |
checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes |
checkStrictlyPositive | Agda.TypeChecking.Positivity |
checkStrippedDotPattern | Agda.TypeChecking.Rules.LHS |
checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality |
checkTelescope | Agda.TypeChecking.Rules.Term |
checkTelescope' | Agda.TypeChecking.Rules.Term |
checkTermination_ | Agda.TypeChecking.Rules.Decl |
checkType | Agda.TypeChecking.CheckInternal |
checkTypeCheckingProblem | Agda.TypeChecking.Constraints |
checkTypedBinding | Agda.TypeChecking.Rules.Term |
checkTypedBindings | Agda.TypeChecking.Rules.Term |
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
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.TypeChecking.Monad, Agda.Compiler.Backend |
checkWithRHS | Agda.TypeChecking.Rules.Def |
Choice | Agda.Auto.NarrowingSearch |
choice | |
1 (Function) | Agda.Utils.Parser.ReadP |
2 (Function) | Agda.TypeChecking.Coverage.Match |
3 (Function) | 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 |
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 |
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.Reflected |
3 (Data Constructor) | Agda.Syntax.Reflected |
4 (Type/Class) | Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Syntax.Internal |
6 (Type/Class) | Agda.Syntax.Abstract |
7 (Data Constructor) | Agda.Syntax.Abstract |
8 (Type/Class) | Agda.Syntax.Concrete.Definitions |
9 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
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 |
clauseFullRange | Agda.Syntax.Internal |
clauseLHS | Agda.Syntax.Abstract |
clauseLHSRange | Agda.Syntax.Internal |
clauseNamedDots | Agda.Syntax.Abstract |
clausePats | Agda.Syntax.Internal |
clausePerm | Agda.Syntax.Internal.Pattern |
clauseRHS | Agda.Syntax.Abstract |
clauseStrippedDots | Agda.Syntax.Abstract |
clauseTel | Agda.Syntax.Internal |
clauseToSplitClause | Agda.TypeChecking.Coverage |
clauseType | Agda.Syntax.Internal |
clauseUnreachable | Agda.Syntax.Internal |
clauseWhereDecls | Agda.Syntax.Abstract |
clBody | Agda.TypeChecking.CompiledClause.Compile |
Clean | Agda.TypeChecking.Unquote |
clean | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
cleanCachedLog | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clearAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clearBlockingVarCons | Agda.TypeChecking.Coverage.Match |
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clearRunningInfo | Agda.Interaction.EmacsCommand |
clearWarning | Agda.Interaction.EmacsCommand |
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clModuleParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClockTime | Agda.Utils.Time |
Clos | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
closeBrace | Agda.Syntax.Parser.Layout |
closed | Agda.TypeChecking.Free |
ClosedLevel | Agda.Syntax.Internal |
closedTerm | Agda.Compiler.MAlonzo.Compiler |
closedTermToTreeless | Agda.Compiler.ToTreeless |
closify | Agda.Auto.Syntax |
Closure | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clPats | Agda.TypeChecking.CompiledClause.Compile |
Cls | Agda.TypeChecking.CompiledClause.Compile |
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cluster | Agda.Utils.Cluster |
cluster' | Agda.Utils.Cluster |
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Cmd_abort | Agda.Interaction.InteractionTop |
Cmd_auto | Agda.Interaction.InteractionTop |
Cmd_compile | Agda.Interaction.InteractionTop |
Cmd_compute | Agda.Interaction.InteractionTop |
Cmd_compute_toplevel | Agda.Interaction.InteractionTop |
Cmd_constraints | Agda.Interaction.InteractionTop |
Cmd_context | Agda.Interaction.InteractionTop |
Cmd_give | Agda.Interaction.InteractionTop |
Cmd_goal_type | Agda.Interaction.InteractionTop |
Cmd_goal_type_context | Agda.Interaction.InteractionTop |
cmd_goal_type_context_and | Agda.Interaction.InteractionTop |
Cmd_goal_type_context_check | Agda.Interaction.InteractionTop |
Cmd_goal_type_context_infer | Agda.Interaction.InteractionTop |
Cmd_helper_function | Agda.Interaction.InteractionTop |
cmd_helper_function | Agda.Interaction.InteractionTop |
Cmd_highlight | Agda.Interaction.InteractionTop |
Cmd_infer | Agda.Interaction.InteractionTop |
Cmd_infer_toplevel | Agda.Interaction.InteractionTop |
Cmd_intro | Agda.Interaction.InteractionTop |
Cmd_load | Agda.Interaction.InteractionTop |
cmd_load' | Agda.Interaction.InteractionTop |
Cmd_load_highlighting_info | Agda.Interaction.InteractionTop |
Cmd_make_case | Agda.Interaction.InteractionTop |
Cmd_metas | Agda.Interaction.InteractionTop |
Cmd_refine | Agda.Interaction.InteractionTop |
Cmd_refine_or_intro | Agda.Interaction.InteractionTop |
Cmd_search_about_toplevel | Agda.Interaction.InteractionTop |
Cmd_show_module_contents | Agda.Interaction.InteractionTop |
Cmd_show_module_contents_toplevel | Agda.Interaction.InteractionTop |
Cmd_show_version | Agda.Interaction.InteractionTop |
Cmd_solveAll | Agda.Interaction.InteractionTop |
Cmd_solveOne | Agda.Interaction.InteractionTop |
Cmd_warnings | Agda.Interaction.InteractionTop |
Cmd_why_in_scope | Agda.Interaction.InteractionTop |
Cmd_why_in_scope_toplevel | Agda.Interaction.InteractionTop |
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.BasicOps |
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CmpInType | Agda.Interaction.BasicOps |
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CmpLevels | Agda.Interaction.BasicOps |
CmpSorts | Agda.Interaction.BasicOps |
CmpTeles | Agda.Interaction.BasicOps |
CmpTypes | Agda.Interaction.BasicOps |
CMRigid | Agda.Auto.Typecheck |
CMSet | |
1 (Type/Class) | Agda.Termination.CallMatrix |
2 (Data Constructor) | Agda.Termination.CallMatrix |
cmSet | Agda.Termination.CallMatrix |
Codata | Agda.Syntax.Concrete.Definitions |
Code | Agda.Syntax.Parser.Literate |
code | |
1 (Function) | Agda.Syntax.Parser.Lexer |
2 (Function) | Agda.Interaction.Highlighting.HTML |
CoDomain | Agda.Utils.TypeLevel |
CoDomain' | Agda.Utils.TypeLevel |
coerce | Agda.TypeChecking.Conversion |
coerceSize | Agda.TypeChecking.Conversion |
CoinductionKit | |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin |
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin |
coinductionKit | Agda.TypeChecking.Monad.Builtin |
coinductionKit' | Agda.TypeChecking.Monad.Builtin |
CoInductive | Agda.Syntax.Common |
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
col | Agda.Termination.SparseMatrix |
coldescr | Agda.Utils.Warshall |
collapseO | Agda.Termination.Order |
collectStats | Agda.TypeChecking.Serialise.Base |
colon | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
cols | Agda.Termination.SparseMatrix |
combineHashes | Agda.Utils.Hash |
comma | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
Command | |
1 (Type/Class) | Agda.Interaction.CommandLine |
2 (Type/Class) | Agda.Interaction.InteractionTop |
3 (Data Constructor) | Agda.Interaction.InteractionTop |
commandLineFlags | Agda.Compiler.Backend |
CommandLineOptions | Agda.Interaction.Options |
commandLineOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CommandM | Agda.Interaction.InteractionTop |
commandMToIO | Agda.Interaction.InteractionTop |
CommandQueue | Agda.Interaction.InteractionTop |
commandQueue | Agda.Interaction.InteractionTop |
CommandState | |
1 (Type/Class) | Agda.Interaction.InteractionTop |
2 (Data Constructor) | Agda.Interaction.InteractionTop |
Comment | |
1 (Data Constructor) | Agda.Syntax.Parser.Literate |
2 (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 |
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 |
compareAtom | Agda.TypeChecking.Conversion |
compareAtomDir | Agda.TypeChecking.Conversion |
compareBelowMax | Agda.TypeChecking.SizedTypes |
CompareDirection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
compareDom | Agda.TypeChecking.Conversion |
compareElims | Agda.TypeChecking.Conversion |
compareFavorites | Agda.Utils.Favorites |
compareFloat | Agda.Syntax.Literal |
compareIrrelevant | Agda.TypeChecking.Conversion |
compareLevel | Agda.TypeChecking.Conversion |
compareMaxViews | Agda.TypeChecking.SizedTypes |
compareOffset | Agda.TypeChecking.SizedTypes.Syntax |
compareRelevance | Agda.TypeChecking.Conversion |
CompareResult | Agda.Utils.Favorites |
compareSizes | Agda.TypeChecking.SizedTypes |
compareSizeViews | Agda.TypeChecking.SizedTypes |
compareSort | Agda.TypeChecking.Conversion |
compareTel | Agda.TypeChecking.Conversion |
compareTerm | Agda.TypeChecking.Conversion |
compareTerm' | Agda.TypeChecking.Conversion |
compareTermDir | Agda.TypeChecking.Conversion |
compareType | Agda.TypeChecking.Conversion |
compareWithFavorites | Agda.Utils.Favorites |
compareWithPol | Agda.TypeChecking.Conversion |
Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
compile | Agda.TypeChecking.CompiledClause.Compile |
compileAlt | Agda.Compiler.JS.Compiler |
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 |
CompiledDataPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledDataUHCPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compileDef | Agda.Compiler.Backend |
CompiledExportPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compileDir | Agda.Compiler.Common |
CompiledJSPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CompiledTypePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compiledTypeSynonym | Agda.Compiler.MAlonzo.Compiler |
CompiledUHCPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
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.InteractionTop |
CompilerPragma | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
compileTerm | Agda.Compiler.JS.Compiler |
compileTerm' | Agda.Compiler.JS.Compiler |
compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile |
complete | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
2 (Function) | Agda.Termination.CallGraph |
completionStep | Agda.Termination.CallGraph |
compose | Agda.TypeChecking.SizedTypes.Utils |
composeFlexRig | Agda.TypeChecking.Free.Lazy |
composeP | Agda.Utils.Permutation |
composePol | Agda.TypeChecking.Polarity |
composeRelevance | Agda.Syntax.Common |
composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
composeVarOcc | Agda.TypeChecking.Free.Lazy |
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
compress | Agda.Interaction.Highlighting.Precise |
CompressedFile | |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
compressedFileInvariant | Agda.Interaction.Highlighting.Precise |
compressPointerChain | Agda.Syntax.Internal |
computeEdges | Agda.TypeChecking.Positivity |
computeElimHeadType | Agda.TypeChecking.Conversion |
computeErasedConstructorArgs | Agda.Compiler.Treeless.Erase |
computeIgnoreAbstract | Agda.Interaction.BasicOps |
ComputeMode | Agda.Interaction.BasicOps |
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 |
computeUnsolvedConstraints | Agda.Interaction.Highlighting.Generate |
computeUnsolvedMetaWarnings | Agda.Interaction.Highlighting.Generate |
computeWrapInput | Agda.Interaction.BasicOps |
Con | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Syntax.Abstract |
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conApp | Agda.TypeChecking.Substitute |
ConArgType | Agda.TypeChecking.Positivity.Occurrence |
conArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conArityAndPars | Agda.Compiler.Common |
conBranches | Agda.TypeChecking.CompiledClause |
conCase | Agda.TypeChecking.CompiledClause |
Concat | Agda.TypeChecking.Positivity |
Concat' | Agda.TypeChecking.Positivity |
concatargs | Agda.Auto.CaseSplit |
concatListT | Agda.Utils.ListT |
ConcreteDef | Agda.Syntax.Common |
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
concreteNamesInScope | Agda.Syntax.Scope.Base |
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract |
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
conFields | Agda.Syntax.Internal |
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.TypeChecking.Monad, Agda.Compiler.Backend |
conInductive | Agda.Syntax.Internal |
ConInfo | Agda.Syntax.Internal |
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConName | Agda.Syntax.Scope.Base |
conName | Agda.Syntax.Internal |
ConnectHandle | Agda.Auto.NarrowingSearch |
connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConOCon | Agda.Syntax.Common |
ConORec | Agda.Syntax.Common |
ConOrigin | Agda.Syntax.Common |
ConOSplit | Agda.Syntax.Common |
ConOSystem | Agda.Syntax.Common |
ConP | |
1 (Data Constructor) | Agda.Syntax.Reflected |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Abstract |
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConPatInfo | |
1 (Type/Class) | Agda.Syntax.Info |
2 (Data Constructor) | Agda.Syntax.Info |
ConPatternInfo | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
conPRecord | Agda.Syntax.Internal |
conPType | Agda.Syntax.Internal |
Cons | |
1 (Data Constructor) | Agda.Utils.IndexedList |
2 (Data Constructor) | Agda.Interaction.EmacsCommand |
consecutiveAndSeparated | Agda.Syntax.Position |
ConsHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
consListT | Agda.Utils.ListT |
ConsMap0 | Agda.Utils.TypeLevel |
ConsMap1 | Agda.Utils.TypeLevel |
consMListT | Agda.Utils.ListT |
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
consS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
consSplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
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 |
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.TypeChecking.Monad, Agda.Compiler.Backend |
Constraint' | Agda.TypeChecking.SizedTypes.Syntax |
constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
constraintProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Constraints | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstraintStatus | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstRef | Agda.Auto.Syntax |
constructIScope | Agda.Interaction.Imports |
Constructor | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constructorCoverageCode | Agda.Compiler.MAlonzo.Compiler |
constructorForm | |
1 (Function) | Agda.TypeChecking.Monad.Builtin |
2 (Function) | Agda.TypeChecking.Reduce.Monad |
constructorForm' | Agda.TypeChecking.Monad.Builtin |
constructorImpossible | Agda.Auto.Typecheck |
ConstructorInfo | Agda.TypeChecking.Datatypes |
ConstructorName | Agda.Syntax.Scope.Monad |
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constructPats | Agda.Auto.Convert |
constructs | Agda.TypeChecking.Rules.Data |
containsAbsurdPattern | Agda.Syntax.Abstract.Pattern |
containsAPattern | Agda.Syntax.Abstract.Pattern |
containsAsPattern | Agda.Syntax.Abstract.Pattern |
contains_constructor | Agda.Auto.Convert |
content | Agda.TypeChecking.CompiledClause |
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
contextOfMeta | Agda.Interaction.BasicOps |
contextSize | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Continue | Agda.Interaction.CommandLine |
continueAfter | Agda.Interaction.CommandLine |
ContinueIn | Agda.Interaction.CommandLine |
continuous | Agda.Syntax.Position |
continuousPerLine | Agda.Syntax.Position |
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conUseSizeLt | Agda.Termination.Monad |
convError | Agda.TypeChecking.Conversion |
Conversion | Agda.Auto.Convert |
convert | Agda.Auto.Convert |
convertGuards | Agda.Compiler.Treeless.GuardsToPrims |
CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
copatternsNotImplemented | Agda.Auto.Convert |
copyarg | Agda.Auto.Typecheck |
copyDirContent | Agda.Utils.IO.Directory |
copyRTEModules | |
1 (Function) | Agda.Compiler.MAlonzo.Compiler |
2 (Function) | Agda.Compiler.JS.Compiler |
copyScope | Agda.Syntax.Scope.Monad |
copyTerm | Agda.Syntax.Internal.Generic |
CoreCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 | |
1 (Function) | Agda.Utils.Bag |
2 (Function) | Agda.Utils.Parser.ReadP |
countTelVars | Agda.Syntax.Concrete |
countWithArgs | Agda.TypeChecking.With |
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
coverageCheck | Agda.TypeChecking.Coverage |
CoverageIssue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoverageNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoverageProblem | Agda.Interaction.Highlighting.Precise |
Covering | |
1 (Type/Class) | Agda.TypeChecking.Coverage |
2 (Data Constructor) | Agda.TypeChecking.Coverage |
covSplitArg | Agda.TypeChecking.Coverage |
covSplitClauses | Agda.TypeChecking.Coverage |
CPUTime | |
1 (Type/Class) | Agda.Utils.Time |
2 (Data Constructor) | Agda.Utils.Time |
createInterface | Agda.Interaction.Imports |
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
createModule | Agda.Syntax.Scope.Monad |
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 | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ctxEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CtxId | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
curDefs | Agda.Compiler.Common |
curHsMod | Agda.Compiler.MAlonzo.Misc |
curIF | Agda.Compiler.Common |
curMName | Agda.Compiler.Common |
curModule | Agda.Compiler.JS.Compiler |
CurrentAccount | Agda.Utils.Benchmark |
currentAccount | Agda.Utils.Benchmark |
CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CurrentInput | Agda.Syntax.Parser.Alex |
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CurrentTypeCheckLog | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
curriedApply | Agda.Compiler.JS.Substitution |
curriedLambda | Agda.Compiler.JS.Substitution |
curryAt | Agda.TypeChecking.Records |
Currying | Agda.Utils.TypeLevel |
currys | Agda.Utils.TypeLevel |
curSig | Agda.Compiler.Common |
CutOff | |
1 (Type/Class) | Agda.Termination.CutOff |
2 (Data Constructor) | Agda.Termination.CutOff |
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |