CAction | Agda.Auto.Syntax |
calc | Agda.Auto.NarrowingSearch |
calcEqRState | Agda.Auto.Typecheck |
CALConcat | Agda.Auto.Syntax |
Call | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Type/Class) | Agda.Termination.CallGraph |
3 (Data Constructor) | Agda.Termination.CallGraph |
callGHC | Agda.Compiler.MAlonzo.Compiler |
CallGraph | Agda.Termination.CallGraph |
callGraphInvariant | Agda.Termination.CallGraph |
callInvariant | Agda.Termination.CallGraph |
CallMatrix | |
1 (Type/Class) | Agda.Termination.CallGraph |
2 (Data Constructor) | Agda.Termination.CallGraph |
callMatrixInvariant | Agda.Termination.CallGraph |
calls | Agda.Termination.Lexicographic |
CALNil | Agda.Auto.Syntax |
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
CantSplit | Agda.TypeChecking.Coverage |
Case | |
1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
2 (Data Constructor) | Agda.TypeChecking.CompiledClause |
3 (Type/Class) | Agda.TypeChecking.CompiledClause |
caseSplitSearch | Agda.Auto.CaseSplit |
caseSplitSearch' | Agda.Auto.CaseSplit |
cat | Agda.Utils.Pretty |
catchAll | Agda.TypeChecking.CompiledClause |
catchAllBranch | Agda.TypeChecking.CompiledClause |
catchConstraint | Agda.TypeChecking.Constraints |
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
catchException | Agda.TypeChecking.Monad.Exception |
catchImpossible | Agda.Utils.Impossible |
categorizedecl | Agda.Auto.Syntax |
catMaybes | Agda.Utils.Maybe |
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.ReadP |
chainl1 | Agda.Utils.ReadP |
chainl1' | Agda.Syntax.Concrete.Operators.Parser |
chainr | Agda.Utils.ReadP |
chainr1 | Agda.Utils.ReadP |
chainr1' | Agda.Syntax.Concrete.Operators.Parser |
char | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Utils.ReadP |
chatty | Agda.Utils.QuickCheck |
checkArgs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkArguments | Agda.TypeChecking.Rules.Term |
checkArguments' | Agda.TypeChecking.Rules.Term |
checkArguments_ | Agda.TypeChecking.Rules.Term |
checkAxiom | Agda.TypeChecking.Rules.Decl |
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkClause | Agda.TypeChecking.Rules.Def |
CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkConstructor | Agda.TypeChecking.Rules.Data |
checkConstructorApplication | Agda.TypeChecking.Rules.Term |
checkConstructorType | Agda.Compiler.MAlonzo.Compiler |
checkCover | Agda.Compiler.MAlonzo.Compiler |
checkCoverage | Agda.TypeChecking.Coverage |
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkDataDef | Agda.TypeChecking.Rules.Data |
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
checkDefinition | Agda.TypeChecking.Rules.Decl |
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkDotPattern | Agda.TypeChecking.Rules.LHS |
checkeliminand | Agda.Auto.Typecheck |
checkEqualities | Agda.TypeChecking.Rules.LHS.Unify |
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkFunDef | Agda.TypeChecking.Rules.Def |
checkHeadApplication | Agda.TypeChecking.Rules.Term |
checkImport | Agda.TypeChecking.Rules.Decl |
checkInjectivity | Agda.TypeChecking.Injectivity |
checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkLetBinding | Agda.TypeChecking.Rules.Term |
checkLetBindings | Agda.TypeChecking.Rules.Term |
checkLiteral | Agda.TypeChecking.Rules.Term |
checkModuleArity | Agda.TypeChecking.Rules.Decl |
checkModuleName | Agda.Interaction.FindFile |
checkMutual | Agda.TypeChecking.Rules.Decl |
checkOpts | Agda.Interaction.Options |
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkPragma | Agda.TypeChecking.Rules.Decl |
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkPrimitive | Agda.TypeChecking.Rules.Decl |
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkRecDef | Agda.TypeChecking.Rules.Record |
checkRecordProjections | Agda.TypeChecking.Rules.Record |
checkSection | Agda.TypeChecking.Rules.Decl |
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkSectionApplication | Agda.TypeChecking.Rules.Decl |
checkSizeIndex | Agda.TypeChecking.Polarity |
checkStrictlyPositive | Agda.TypeChecking.Positivity |
checkTelescope | Agda.TypeChecking.Rules.Term |
checkTelescope_ | Agda.TypeChecking.Rules.Term |
checkTypedBinding | Agda.TypeChecking.Rules.Term |
checkTypedBindings | Agda.TypeChecking.Rules.Term |
checkTypedBindings_ | Agda.TypeChecking.Rules.Term |
checkTypedBinding_ | Agda.TypeChecking.Rules.Term |
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
checkTypeSignature | Agda.TypeChecking.Rules.Decl |
checkWhere | Agda.TypeChecking.Rules.Def |
checkWithFunction | Agda.TypeChecking.Rules.Def |
Choice | Agda.Auto.NarrowingSearch |
choice | |
1 (Function) | Agda.Utils.ReadP |
2 (Function) | Agda.TypeChecking.Coverage.Match |
choose | |
1 (Function) | Agda.Utils.QuickCheck |
2 (Function) | Agda.Auto.NarrowingSearch |
choosePrioMeta | Agda.Auto.NarrowingSearch |
chop | Agda.Utils.List |
Chr | Agda.Utils.Pretty |
Cl | Agda.TypeChecking.CompiledClause |
ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
classify | Agda.Utils.QuickCheck |
Clause | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Type/Class) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Data Constructor) | Agda.Syntax.Abstract |
6 (Type/Class) | Agda.Syntax.Concrete.Definitions |
7 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
clause | Agda.Compiler.MAlonzo.Compiler |
ClauseBody | Agda.Syntax.Internal |
clauseBody | Agda.Syntax.Internal |
clausebody | Agda.Compiler.MAlonzo.Compiler |
clausePats | Agda.Syntax.Internal |
clausePerm | Agda.Syntax.Internal |
clauseRange | Agda.Syntax.Internal |
Clauses | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
clausesAbove | Agda.Compiler.Epic.Forcing |
clauseTel | Agda.Syntax.Internal |
clauseToFix | Agda.Compiler.Epic.Forcing |
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Clos | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
closeBrace | Agda.Syntax.Parser.Layout |
ClosedLevel | Agda.TypeChecking.Level |
closify | Agda.Auto.Syntax |
Closure | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Cls | Agda.TypeChecking.CompiledClause |
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cm | Agda.Termination.CallGraph |
cmd_auto | Agda.Interaction.GhciTop |
cmd_compile | Agda.Interaction.GhciTop |
cmd_compute | Agda.Interaction.GhciTop |
cmd_compute_toplevel | Agda.Interaction.GhciTop |
cmd_constraints | Agda.Interaction.GhciTop |
cmd_context | Agda.Interaction.GhciTop |
cmd_give | Agda.Interaction.GhciTop |
cmd_goal_type | Agda.Interaction.GhciTop |
cmd_goal_type_context | Agda.Interaction.GhciTop |
cmd_goal_type_context_and | Agda.Interaction.GhciTop |
cmd_goal_type_context_infer | Agda.Interaction.GhciTop |
cmd_infer | Agda.Interaction.GhciTop |
cmd_infer_toplevel | Agda.Interaction.GhciTop |
cmd_intro | Agda.Interaction.GhciTop |
cmd_load | Agda.Interaction.GhciTop |
cmd_load' | Agda.Interaction.GhciTop |
cmd_make_case | Agda.Interaction.GhciTop |
cmd_metas | Agda.Interaction.GhciTop |
cmd_refine | Agda.Interaction.GhciTop |
cmd_refine_or_intro | Agda.Interaction.GhciTop |
cmd_show_module_contents | Agda.Interaction.GhciTop |
cmd_show_module_contents_toplevel | Agda.Interaction.GhciTop |
cmd_solveAll | Agda.Interaction.GhciTop |
cmd_write_highlighting_info | Agda.Interaction.GhciTop |
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 |
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CmpInType | Agda.Interaction.BasicOps |
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CmpLevels | Agda.Interaction.BasicOps |
CmpSorts | Agda.Interaction.BasicOps |
CmpTeles | Agda.Interaction.BasicOps |
CmpTerms | Agda.Interaction.BasicOps |
CmpTypes | Agda.Interaction.BasicOps |
CMRigid | Agda.Auto.Typecheck |
cnvh | Agda.Auto.Convert |
CoArbitrary | Agda.Utils.QuickCheck |
coarbitrary | Agda.Utils.QuickCheck |
coarbitraryIntegral | Agda.Utils.QuickCheck |
coarbitraryReal | Agda.Utils.QuickCheck |
coarbitraryShow | Agda.Utils.QuickCheck |
Codata | Agda.Syntax.Concrete.Definitions |
code | Agda.Syntax.Parser.Lexer |
CoinductionKit | |
1 (Type/Class) | Agda.TypeChecking.Rules.Builtin.Coinduction |
2 (Data Constructor) | Agda.TypeChecking.Rules.Builtin.Coinduction |
coinductionKit | Agda.TypeChecking.Rules.Builtin.Coinduction |
CoInductive | Agda.Syntax.Common |
CoinductiveDatatype | Agda.TypeChecking.Coverage |
col | |
1 (Function) | Agda.Termination.SparseMatrix |
2 (Function) | Agda.Termination.Matrix |
coldescr | Agda.Utils.Warshall |
collect | Agda.Utils.QuickCheck |
colon | Agda.Utils.Pretty |
cols | |
1 (Function) | Agda.Termination.SparseMatrix |
2 (Function) | Agda.Termination.Matrix |
Column | Agda.Termination.Lexicographic |
columns | Agda.Termination.Lexicographic |
comma | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
Command | Agda.Interaction.CommandLine.CommandLine |
command | Agda.Interaction.GhciTop |
CommandLineOptions | Agda.Interaction.Options |
commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
Comment | |
1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
commutative | Agda.Utils.TestHelpers |
commuteM | Agda.Utils.Monad |
comp' | Agda.Auto.Typecheck |
compactP | Agda.Utils.Permutation |
compareArgs | Agda.TypeChecking.Conversion |
compareAtom | Agda.TypeChecking.Conversion |
compareLevel | Agda.TypeChecking.UniversePolymorphism |
compareSizes | Agda.TypeChecking.SizedTypes |
compareSort | Agda.TypeChecking.Conversion |
compareTel | Agda.TypeChecking.Conversion |
compareTerm | Agda.TypeChecking.Conversion |
compareType | Agda.TypeChecking.Conversion |
Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Compile | Agda.Compiler.Epic.CompileState |
compile | |
1 (Function) | Agda.TypeChecking.CompiledClause |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
compileClauses | |
1 (Function) | Agda.TypeChecking.CompiledClause |
2 (Function) | Agda.Compiler.Epic.FromAgda |
CompiledClauses | Agda.TypeChecking.CompiledClause |
CompiledDataPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledEpicPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compileDir | Agda.Compiler.MAlonzo.Compiler |
CompiledPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledTypePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compilerMain | |
1 (Function) | Agda.Compiler.Epic.Compiler |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
CompileState | |
1 (Type/Class) | Agda.Compiler.Epic.CompileState |
2 (Data Constructor) | Agda.Compiler.Epic.CompileState |
complete | Agda.Termination.CallGraph |
composeP | Agda.Utils.Permutation |
composePol | Agda.TypeChecking.Polarity |
compress | Agda.Interaction.Highlighting.Precise |
CompressedFile | Agda.Interaction.Highlighting.Precise |
computeEdge | Agda.TypeChecking.Positivity |
computeNeighbourhood | Agda.TypeChecking.Coverage |
ComputeOccurrences | Agda.TypeChecking.Positivity |
computeOccurrences | Agda.TypeChecking.Positivity |
computePolarity | Agda.TypeChecking.Polarity |
computeSizeConstraint | Agda.TypeChecking.SizedTypes |
Con | |
1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Abstract |
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ConArgType | Agda.TypeChecking.Positivity |
conBranches | Agda.TypeChecking.CompiledClause |
conCase | Agda.TypeChecking.CompiledClause |
concatargs | Agda.Auto.CaseSplit |
concatMapM | Agda.Utils.Monad |
concatOccurs | Agda.TypeChecking.Positivity |
ConcreteDef | Agda.Syntax.Common |
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
condecl | Agda.Compiler.MAlonzo.Compiler |
conFreq | Agda.TypeChecking.Test.Generators |
ConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
conhqn | Agda.Compiler.MAlonzo.Misc |
conHsCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
conjoin | Agda.Utils.QuickCheck |
ConMP | Agda.TypeChecking.Coverage.Match |
ConName | |
1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
2 (Type/Class) | Agda.TypeChecking.Test.Generators |
3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
ConnectHandle | Agda.Auto.NarrowingSearch |
ConP | |
1 (Data Constructor) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Abstract |
conPars | |
1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Function) | Agda.Compiler.Epic.CompileState |
ConPos | Agda.TypeChecking.With |
Cons | Agda.Interaction.GhciTop |
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Const | Agda.Auto.Syntax |
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.Monad.Base, Agda.TypeChecking.Monad |
2 (Type/Class) | Agda.Utils.Warshall |
ConstraintClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Constraints | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Type/Class) | Agda.Utils.Warshall |
ConstRef | Agda.Auto.Syntax |
constrIrr | Agda.Compiler.Epic.ConstructorIrrelevancy |
constrType | Agda.Compiler.Epic.Forcing |
Constructor | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Type/Class) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
constructorArity | |
1 (Function) | Agda.Compiler.Epic.CompileState |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
constructorForm | Agda.TypeChecking.Primitive |
constructorImpossible | Agda.Auto.Typecheck |
ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
ConstructorName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
constructorsInClause | Agda.TypeChecking.With |
constructorsInClauses | Agda.TypeChecking.With |
constructPats | Agda.Auto.Convert |
constructs | Agda.TypeChecking.Rules.Data |
Cont | Agda.Utils.Monad |
containsAbsurdPattern | Agda.TypeChecking.Rules.Def |
contains_constructor | Agda.Auto.Convert |
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
contextOfMeta | Agda.Interaction.BasicOps |
Continue | Agda.Interaction.CommandLine.CommandLine |
continueAfter | Agda.Interaction.CommandLine.CommandLine |
ContinueIn | Agda.Interaction.CommandLine.CommandLine |
continuous | Agda.Syntax.Position, Agda.Interaction.GhciTop |
continuousPerLine | Agda.Syntax.Position, Agda.Interaction.GhciTop |
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
convertLineEndings | Agda.Utils.Unicode |
copyarg | Agda.Auto.Typecheck |
copyScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
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 |
costUnificationOccurs | Agda.Auto.SearchControl |
count | Agda.Utils.ReadP |
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cover | |
1 (Function) | Agda.Utils.QuickCheck |
2 (Function) | Agda.TypeChecking.Coverage |
CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Covering | Agda.TypeChecking.Coverage |
CoverM | Agda.TypeChecking.Coverage |
createInterface | Agda.Interaction.Imports |
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
createModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
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 |
cthandles | Agda.Auto.NarrowingSearch |
ctparent | Agda.Auto.NarrowingSearch |
ctpriometa | Agda.Auto.NarrowingSearch |
CTree | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
ctsub | Agda.Auto.NarrowingSearch |
Ctx | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ctxEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CtxId | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
curDefs | Agda.Compiler.MAlonzo.Misc |
curHsMod | Agda.Compiler.MAlonzo.Misc |
curIF | Agda.Compiler.MAlonzo.Misc |
curMName | Agda.Compiler.MAlonzo.Misc |
CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
CurrentInput | Agda.Syntax.Parser.Alex |
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
currentMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
curSig | Agda.Compiler.MAlonzo.Misc |
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |