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 |
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 |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
callInfoCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
callInfoRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
callInfos | Agda.Termination.Monad |
callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CallMatrix | |
1 (Type/Class) | Agda.Termination.CallMatrix |
2 (Data Constructor) | Agda.Termination.CallMatrix |
callMatrix | 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 | Agda.TypeChecking.InstanceArguments |
Candidates | Agda.TypeChecking.InstanceArguments |
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
canonicalizeSizeConstraint | |
1 (Function) | Agda.TypeChecking.SizedTypes |
2 (Function) | Agda.TypeChecking.SizedTypes.Solve |
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
canProject | Agda.TypeChecking.Substitute |
CantInvert | Agda.TypeChecking.MetaVars |
CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CantSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cantSplitConIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cantSplitConName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cantSplitGivenIdx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cantSplitTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Case | |
1 (Type/Class) | Agda.Compiler.JS.Case |
2 (Data Constructor) | Agda.Compiler.JS.Case |
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
4 (Data Constructor) | Agda.TypeChecking.CompiledClause |
5 (Type/Class) | Agda.TypeChecking.CompiledClause |
CaseContext | Agda.Interaction.MakeCase |
casee | Agda.Compiler.Epic.AuxAST |
caseEitherM | Agda.Utils.Either |
caseList | Agda.Utils.List |
caseListT | Agda.Utils.ListT |
caseMaybe | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
caseMaybeM | |
1 (Function) | Agda.Utils.Maybe.Strict |
2 (Function) | Agda.Utils.Maybe |
caseOpts | Agda.Compiler.Epic.CaseOpts |
caseOptsExpr | Agda.Compiler.Epic.CaseOpts |
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.Utils.Except |
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
catchException | Agda.TypeChecking.Monad.Exception |
catchImpossible | Agda.Utils.Impossible |
categorizedecl | Agda.Auto.Syntax |
catMaybes | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
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 |
chainr | Agda.Utils.ReadP |
chainr1 | Agda.Utils.ReadP |
Change | Agda.Utils.Update |
Char | Agda.Compiler.JS.Syntax |
char | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.Utils.ReadP |
chatty | Agda.Utils.QuickCheck |
checkAbsurdLambda | Agda.TypeChecking.Rules.Term |
checkAlias | Agda.TypeChecking.Rules.Def |
checkApplication | Agda.TypeChecking.Rules.Term |
CheckArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
checkCandidates | Agda.TypeChecking.InstanceArguments |
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkClause | Agda.TypeChecking.Rules.Def |
checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl |
CheckConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkDataDef | Agda.TypeChecking.Rules.Data |
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
checkDontExpandLast | Agda.TypeChecking.Rules.Term |
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkDotPattern | Agda.TypeChecking.Rules.LHS |
checkeliminand | Agda.Auto.Typecheck |
checkEqualities | Agda.TypeChecking.Rules.LHS.Unify |
checkEquality | Agda.TypeChecking.Rules.LHS.Unify |
checkEqualityHH | Agda.TypeChecking.Rules.LHS.Unify |
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
CheckExprCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkExtendedLambda | Agda.TypeChecking.Rules.Term |
checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkFunDef | Agda.TypeChecking.Rules.Def |
checkFunDef' | 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 |
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CheckLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkLambda | Agda.TypeChecking.Rules.Term |
checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkLetBinding | Agda.TypeChecking.Rules.Term |
checkLetBindings | Agda.TypeChecking.Rules.Term |
checkLHS | Agda.TypeChecking.Rules.LHS |
checkLinearity | Agda.TypeChecking.MetaVars |
checkLiteral | Agda.TypeChecking.Rules.Term |
checkMeta | Agda.TypeChecking.Rules.Term |
checkModuleArity | Agda.TypeChecking.Rules.Decl |
checkModuleName | Agda.Interaction.FindFile |
checkMutual | Agda.TypeChecking.Rules.Decl |
checkOpts | Agda.Interaction.Options |
checkOrInferMeta | Agda.TypeChecking.Rules.Term |
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
checkPragma | Agda.TypeChecking.Rules.Decl |
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkPrimitive | Agda.TypeChecking.Rules.Decl |
checkProjectionLikeness_ | Agda.TypeChecking.Rules.Decl |
CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkRecDef | Agda.TypeChecking.Rules.Record |
checkRecordExpression | Agda.TypeChecking.Rules.Term |
checkRecordProjections | Agda.TypeChecking.Rules.Record |
checkRecordUpdate | Agda.TypeChecking.Rules.Term |
checkSection | Agda.TypeChecking.Rules.Decl |
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
checkSectionApplication | Agda.TypeChecking.Rules.Decl |
checkSectionApplication' | Agda.TypeChecking.Rules.Decl |
checkSizeIndex | Agda.TypeChecking.Polarity |
checkStrictlyPositive | Agda.TypeChecking.Positivity |
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 |
checkUnquoteDecl | Agda.TypeChecking.Rules.Decl |
checkWhere | Agda.TypeChecking.Rules.Def |
checkWithFunction | Agda.TypeChecking.Rules.Def |
CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Choice | Agda.Auto.NarrowingSearch |
choice | |
1 (Function) | Agda.Utils.ReadP |
2 (Function) | Agda.TypeChecking.Coverage.Match |
3 (Function) | Agda.TypeChecking.Unquote |
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.Compile |
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.Concrete.Definitions |
3 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Data Constructor) | Agda.Syntax.Abstract |
6 (Type/Class) | Agda.Syntax.Internal |
7 (Data Constructor) | Agda.Syntax.Internal |
clause | |
1 (Function) | Agda.Compiler.JS.Compiler |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
Clause' | Agda.Syntax.Abstract |
clauseArgs | Agda.Syntax.Internal.Pattern |
ClauseBody | Agda.Syntax.Internal |
clauseBody | Agda.Syntax.Internal |
clausebody | Agda.Compiler.MAlonzo.Compiler |
ClauseBodyF | Agda.Syntax.Internal |
clauseElims | Agda.Syntax.Internal.Pattern |
clauseLHS | Agda.Syntax.Abstract |
clausePats | Agda.Syntax.Internal |
clausePerm | Agda.Syntax.Internal |
clauseRange | Agda.Syntax.Internal |
clauseRHS | Agda.Syntax.Abstract |
clauseTel | Agda.Syntax.Internal |
clauseToSplitClause | Agda.TypeChecking.Coverage |
clauseType | Agda.Syntax.Internal |
clauseWhereDecls | Agda.Syntax.Abstract |
clearAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
clearBlockingVarCons | Agda.TypeChecking.Coverage.Match |
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
clearRunningInfo | Agda.Interaction.EmacsCommand |
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ClockTime | Agda.Utils.Time |
Clos | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
closeBrace | Agda.Syntax.Parser.Layout |
ClosedLevel | Agda.Syntax.Internal |
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.Compile |
clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cluster | Agda.Utils.Cluster |
cluster' | Agda.Utils.Cluster |
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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_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_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_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 |
CmpInType | Agda.Interaction.BasicOps |
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
CName | |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree |
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree |
cnvh | Agda.Auto.Convert |
CoArbitrary | Agda.Utils.QuickCheck |
coarbitrary | Agda.Utils.QuickCheck |
coarbitraryEnum | Agda.Utils.QuickCheck |
coarbitraryIntegral | Agda.Utils.QuickCheck |
coarbitraryReal | Agda.Utils.QuickCheck |
coarbitraryShow | Agda.Utils.QuickCheck |
Codata | Agda.Syntax.Concrete.Definitions |
code | |
1 (Function) | Agda.Syntax.Parser.Lexer |
2 (Function) | Agda.Interaction.Highlighting.HTML |
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 |
CoInductive | Agda.Syntax.Common |
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
col | Agda.Termination.SparseMatrix |
coldescr | Agda.Utils.Warshall |
collapseO | Agda.Termination.Order |
collect | Agda.Utils.QuickCheck |
colOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
colon | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
Color | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
3 (Type/Class) | Agda.Syntax.Internal |
ColoredTypedBinding | Agda.Syntax.Concrete |
ColorMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cols | Agda.Termination.SparseMatrix |
combineHashes | Agda.Utils.Hash |
comma | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
Command | Agda.Interaction.CommandLine |
CommandLineOptions | Agda.Interaction.Options |
commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
CommandM | Agda.Interaction.InteractionTop |
commandMToIO | Agda.Interaction.InteractionTop |
CommandState | |
1 (Type/Class) | Agda.Interaction.InteractionTop |
2 (Data Constructor) | Agda.Interaction.InteractionTop |
Comment | |
1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
2 (Type/Class) | Agda.Compiler.Epic.AuxAST |
commonPreds | Agda.TypeChecking.SizedTypes.WarshallSolver |
commonPrefix | Agda.Utils.List |
commonSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
commonSuffix | Agda.Utils.List |
commutative | Agda.Utils.TestHelpers |
comp' | Agda.Auto.Typecheck |
compactP | Agda.Utils.Permutation |
compactS | Agda.TypeChecking.Substitute |
Comparable | Agda.Utils.PartialOrd |
comparable | Agda.Utils.PartialOrd |
comparableOrd | Agda.Utils.PartialOrd |
Compare | Agda.TypeChecking.Monad.Base.Benchmark, 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 |
compareElims | Agda.TypeChecking.Conversion |
compareFavorites | Agda.Utils.Favorites |
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 |
CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Compile | Agda.Compiler.Epic.CompileState |
compile | |
1 (Function) | Agda.TypeChecking.CompiledClause.Compile |
2 (Function) | Agda.Compiler.JS.Compiler |
3 (Function) | Agda.Compiler.MAlonzo.Compiler |
compileClauses | |
1 (Function) | Agda.TypeChecking.CompiledClause.Compile |
2 (Function) | Agda.Compiler.Epic.FromAgda |
CompiledClauses | Agda.TypeChecking.CompiledClause |
CompiledDataPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compiledEpic | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CompiledEpicPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledExportPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compiledHaskell | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
compileDir | |
1 (Function) | Agda.Compiler.JS.Compiler |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
compiledJS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CompiledJSPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compiledModules | Agda.Compiler.Epic.CompileState |
CompiledPragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
CompiledRep | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CompiledTypePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compilerMain | |
1 (Function) | Agda.Compiler.Epic.Compiler |
2 (Function) | Agda.Compiler.JS.Compiler |
3 (Function) | Agda.Compiler.MAlonzo.Compiler |
CompileState | |
1 (Type/Class) | Agda.Compiler.Epic.CompileState |
2 (Data Constructor) | Agda.Compiler.Epic.CompileState |
compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile |
complete | Agda.Termination.CallGraph |
completionStep | Agda.Termination.CallGraph |
compose | Agda.TypeChecking.SizedTypes.Utils |
composeP | Agda.Utils.Permutation |
composePol | Agda.TypeChecking.Polarity |
composeRelevance | Agda.TypeChecking.Irrelevance |
composeS | Agda.TypeChecking.Substitute |
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Compress | Agda.TypeChecking.Monad.Base.Benchmark, 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 |
computeEdge | Agda.TypeChecking.Positivity |
computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
ComputeOccurrences | Agda.TypeChecking.Positivity |
computeOccurrences | Agda.TypeChecking.Positivity |
computePolarity | Agda.TypeChecking.Polarity |
computeSizeConstraint | |
1 (Function) | Agda.TypeChecking.SizedTypes |
2 (Function) | Agda.TypeChecking.SizedTypes.Solve |
computeSizeConstraints | Agda.TypeChecking.SizedTypes |
computeUnsolvedConstraints | Agda.Interaction.Highlighting.Generate |
computeUnsolvedMetaWarnings | Agda.Interaction.Highlighting.Generate |
Con | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
conApp | Agda.TypeChecking.Substitute |
ConArgType | Agda.TypeChecking.Positivity |
conArity | Agda.Compiler.Epic.Interface |
conArityAndPars | Agda.Compiler.MAlonzo.Compiler |
conBranches | Agda.TypeChecking.CompiledClause |
conCase | Agda.TypeChecking.CompiledClause |
concatargs | Agda.Auto.CaseSplit |
concatListT | Agda.Utils.ListT |
concatOccurs | Agda.TypeChecking.Positivity |
ConcreteDef | Agda.Syntax.Common |
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract |
conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ConDBP | Agda.Termination.Monad |
condecl | Agda.Compiler.MAlonzo.Compiler |
Condition | Agda.TypeChecking.MetaVars |
conFields | Agda.Syntax.Internal |
conFreq | Agda.TypeChecking.Test.Generators |
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 |
conInductive | Agda.Syntax.Internal |
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
conjoin | Agda.Utils.QuickCheck |
ConMP | Agda.TypeChecking.Coverage.Match |
ConName | |
1 (Data Constructor) | Agda.Syntax.Scope.Base |
2 (Type/Class) | Agda.TypeChecking.Test.Generators |
3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
conName | Agda.Syntax.Internal |
ConnectHandle | Agda.Auto.NarrowingSearch |
connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
ConP | |
1 (Data Constructor) | Agda.Syntax.Abstract |
2 (Data Constructor) | Agda.Syntax.Internal |
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 | Agda.Interaction.EmacsCommand |
ConsHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
consListT | Agda.Utils.ListT |
consMListT | Agda.Utils.ListT |
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
consS | Agda.TypeChecking.Substitute |
consSplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
Const | |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
3 (Data Constructor) | Agda.Compiler.JS.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.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 |
Constraint' | Agda.TypeChecking.SizedTypes.Syntax |
constraintGraph | Agda.TypeChecking.SizedTypes.WarshallSolver |
constraintGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
constraintProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Constraints | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ConstRef | Agda.Auto.Syntax |
constrGroup | Agda.Compiler.Epic.Injection |
constrInScope | Agda.Compiler.Epic.CompileState |
constrTags | Agda.Compiler.Epic.Interface |
Constructor | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Type/Class) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
4 (Type/Class) | Agda.Syntax.Abstract |
5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
constructorArity | Agda.Compiler.Epic.CompileState |
constructorForm | |
1 (Function) | Agda.TypeChecking.Monad.Builtin |
2 (Function) | Agda.TypeChecking.Reduce.Monad |
constructorForm' | Agda.TypeChecking.Monad.Builtin |
constructorImpossible | Agda.Auto.Typecheck |
ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
constructorMismatchHH | Agda.TypeChecking.Rules.LHS.Unify |
ConstructorName | Agda.Syntax.Scope.Monad |
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
constructPats | Agda.Auto.Convert |
constructs | Agda.TypeChecking.Rules.Data |
Cont | Agda.Utils.Monad |
containsAbsurdPattern | Agda.TypeChecking.Rules.Def |
contains_constructor | Agda.Auto.Convert |
content | Agda.TypeChecking.CompiledClause |
Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
contextOfMeta | Agda.Interaction.BasicOps |
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 |
conUseSizeLt | Agda.Termination.Monad |
ConvColor | Agda.TypeChecking.Rules.Term |
convColor | Agda.TypeChecking.Rules.Term |
convError | Agda.TypeChecking.Conversion |
copatternsNotImplemented | Agda.Auto.Convert |
copyarg | Agda.Auto.Typecheck |
copyScope | Agda.Syntax.Scope.Monad |
copyTerm | Agda.Syntax.Internal.Generic |
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 | |
1 (Function) | Agda.Utils.ReadP |
2 (Function) | Agda.Utils.Bag |
counterexample | Agda.Utils.QuickCheck |
countTelVars | Agda.Syntax.Concrete |
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
cover | Agda.Utils.QuickCheck |
Coverage | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
CoverageCantSplitIrrelevantType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
coverageCheck | Agda.TypeChecking.Coverage |
CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
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 |
cthandles | Agda.Auto.NarrowingSearch |
ctparent | Agda.Auto.NarrowingSearch |
ctpriometa | Agda.Auto.NarrowingSearch |
CTrans | Agda.TypeChecking.SizedTypes.Syntax |
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 |
curFun | Agda.Compiler.Epic.CompileState |
curHsMod | Agda.Compiler.MAlonzo.Misc |
curIF | Agda.Compiler.MAlonzo.Misc |
curMName | Agda.Compiler.MAlonzo.Misc |
curModule | |
1 (Function) | Agda.Compiler.Epic.CompileState |
2 (Function) | Agda.Compiler.JS.Compiler |
currentAccount | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
CurrentInput | Agda.Syntax.Parser.Alex |
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
currentProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
curriedApply | Agda.Compiler.JS.Substitution |
curriedLambda | Agda.Compiler.JS.Substitution |
curryAt | Agda.TypeChecking.Records |
curSig | Agda.Compiler.MAlonzo.Misc |
CutOff | |
1 (Type/Class) | Agda.Termination.CutOff |
2 (Data Constructor) | Agda.Termination.CutOff |
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |