C | Agda.Mimer.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 |
Call | |
1 (Type/Class) | Agda.Termination.CallGraph |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
callBackend | Agda.Compiler.Backend |
callByName | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CallComb | Agda.Termination.CallMatrix |
callCompiler | Agda.Compiler.CallCompiler |
callCompiler' | Agda.Compiler.CallCompiler |
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 |
callInfos | Agda.Termination.Monad |
callInfoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
callMain | Agda.Compiler.JS.Syntax |
CallMatrix | |
1 (Type/Class) | Agda.Termination.CallMatrix |
2 (Data Constructor) | Agda.Termination.CallMatrix |
CallMatrix' | Agda.Termination.CallMatrix |
CallMatrixAug | |
1 (Type/Class) | Agda.Termination.CallMatrix |
2 (Data Constructor) | Agda.Termination.CallMatrix |
callMatrixSet | Agda.Termination.CallGraph |
CallPath | |
1 (Type/Class) | Agda.Termination.Monad |
2 (Data Constructor) | Agda.Termination.Monad |
CallSite | Agda.Utils.CallStack |
CallSiteFilter | Agda.Utils.CallStack |
CallStack | Agda.Utils.CallStack |
callStack | Agda.Utils.CallStack |
camelTo2 | Agda.Interaction.JSON |
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 |
CandidateKind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateKind | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
candidateOverlap | 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 |
canDropRecursiveInstance | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
canHaveSuffixTest | Agda.Syntax.Scope.Monad |
CannotCreateMissingClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotEliminateWithPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotEliminateWithProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotResolveAmbiguousPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotRewriteByNonEquation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotSolveSizeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CannotTransp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
canonicalizeAbsolutePath | Agda.Utils.FileName |
canonicalizeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
canProject | Agda.TypeChecking.Substitute |
CantGeneralizeOverSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CantGeneralizeOverSorts_ | Agda.Interaction.Options.Warnings |
CantInvert | Agda.TypeChecking.MetaVars |
CantResolveOverloadedConstructorsTargetingSameDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cantSplitBlocker | 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 |
Carrier | Agda.Utils.Zipper |
Case | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.TypeChecking.CompiledClause |
3 (Type/Class) | Agda.TypeChecking.CompiledClause |
CaseContext | Agda.Interaction.MakeCase |
CaseDT | Agda.TypeChecking.DiscrimTree.Types |
caseEitherM | Agda.Utils.Either |
caseErased | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CaseInfo | |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend |
caseLazy | Agda.Syntax.Treeless, Agda.Compiler.Backend |
caseList | Agda.Utils.List |
caseListM | Agda.Utils.List |
caseListT | Agda.Utils.ListT |
caseMaybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
caseMaybeM | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
CaseSplit | Agda.Syntax.Common |
caseToSeq | Agda.Compiler.Treeless.Uncase |
CaseType | Agda.Syntax.Treeless, Agda.Compiler.Backend |
caseType | Agda.Syntax.Treeless, Agda.Compiler.Backend |
castConstraintToCurrentContext | Agda.TypeChecking.SizedTypes.Solve |
castConstraintToCurrentContext' | Agda.TypeChecking.SizedTypes.Solve |
cat | Agda.Syntax.Common.Pretty |
Catchall | Agda.Syntax.Concrete.Definitions.Types |
catchAll | Agda.TypeChecking.CompiledClause |
catchAllBranch | Agda.TypeChecking.CompiledClause |
CatchallClause | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
CatchallPragma | Agda.Syntax.Concrete |
catchallPragma | Agda.Syntax.Concrete.Definitions.Monad |
catchAndPrintImpossible | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
catchConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
catchIlltypedPatternBlockedOnMeta | Agda.TypeChecking.Rules.Term |
CatchImpossible | Agda.Utils.Impossible |
catchImpossible | Agda.Utils.Impossible |
catchImpossibleJust | Agda.Utils.Impossible |
CatchIO | Agda.Utils.IO |
catchIO | Agda.Utils.IO |
catchPatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
catMaybes | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
3 (Function) | Agda.Utils.List1 |
catMaybesMP | Agda.Utils.Monad |
CErased | Agda.Syntax.Common |
CFull | Agda.Syntax.Common |
Change | Agda.Utils.Update |
ChangeT | Agda.Utils.Update |
Char | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
char | Agda.Syntax.Common.Pretty |
chaseDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkAbsurdLambda | Agda.TypeChecking.Rules.Term |
checkAlias | Agda.TypeChecking.Rules.Def |
checkAndSetOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkApplication | Agda.TypeChecking.Rules.Application |
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.Application |
checkArguments_ | Agda.TypeChecking.Rules.Application |
checkAttributes | Agda.Syntax.Translation.ConcreteToAbstract |
checkAxiom | Agda.TypeChecking.Rules.Decl |
checkAxiom' | Agda.TypeChecking.Rules.Decl |
CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkClause | Agda.TypeChecking.Rules.Def |
checkClauseLHS | Agda.TypeChecking.Rules.Def |
checkClauseTelescopeBindings | Agda.Syntax.Translation.ReflectedToAbstract |
checkCoinductiveRecords | Agda.TypeChecking.Rules.Decl |
checkCompilerPragmas | Agda.Compiler.JS.Compiler |
CheckConArgFitsIn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckConfluence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkConfluenceOfClauses | Agda.TypeChecking.Rewriting.Confluence |
checkConfluenceOfRules | Agda.TypeChecking.Rewriting.Confluence |
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 |
checkConstructorCount | Agda.Compiler.MAlonzo.HaskellTypes |
CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkDataDef | Agda.TypeChecking.Rules.Data |
CheckDataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkDataSort | Agda.TypeChecking.Rules.Data |
checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
checkDeclCached | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TheTypeChecker |
checkDisplayPragma | Agda.TypeChecking.Rules.Display |
checkDomain | Agda.TypeChecking.Rules.Term |
checkDontExpandLast | Agda.TypeChecking.Rules.Term |
CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkEarlierThan | Agda.TypeChecking.Lock |
checkedMainDecl | Agda.Compiler.MAlonzo.Primitives |
checkedMainDef | Agda.Compiler.MAlonzo.Primitives |
CheckedMainFunctionDef | |
1 (Type/Class) | Agda.Compiler.MAlonzo.Primitives |
2 (Data Constructor) | Agda.Compiler.MAlonzo.Primitives |
CheckedTarget | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkEmptyTel | Agda.TypeChecking.Empty |
CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkExpr | Agda.TypeChecking.Rules.Term, Agda.TheTypeChecker |
checkExpr' | Agda.TypeChecking.Rules.Term |
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 |
checkForUniqueAttribute | Agda.Syntax.Parser.Helpers |
CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkFunDef | Agda.TypeChecking.Rules.Def |
checkFunDef' | Agda.TypeChecking.Rules.Def |
CheckFunDefCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkFunDefS | Agda.TypeChecking.Rules.Def |
checkGeneralize | Agda.TypeChecking.Rules.Decl |
checkGeneralizeTelescope | Agda.TypeChecking.Rules.Term |
CheckIApplyConfluence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkIApplyConfluence | Agda.TypeChecking.IApplyConfluence |
checkIApplyConfluence_ | Agda.TypeChecking.IApplyConfluence |
checkImportDirective | Agda.TypeChecking.Rules.Decl |
checkIndexSorts | Agda.TypeChecking.Rules.Data |
checkInjectivity | Agda.TypeChecking.Injectivity |
checkInjectivity' | Agda.TypeChecking.Injectivity |
checkInjectivity_ | Agda.TypeChecking.Rules.Decl |
CheckInternal | Agda.TypeChecking.CheckInternal |
checkInternal | Agda.TypeChecking.CheckInternal |
checkInternal' | Agda.TypeChecking.CheckInternal |
CheckIsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckK | Agda.Compiler.MAlonzo.Misc |
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 |
checkLambda' | Agda.TypeChecking.Rules.Term |
checkLazyMatch | Agda.TypeChecking.CompiledClause |
checkLeftHandSide | 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 |
checkLevel | Agda.TypeChecking.Rules.Term |
CheckLHS | |
1 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkLibraryFileNotTooFarDown | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkLinearity | Agda.TypeChecking.MetaVars |
checkLiteral | Agda.TypeChecking.Rules.Term |
CheckLock | Agda.Interaction.Base |
CheckLockedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkLockedVars | Agda.TypeChecking.Lock |
checkLoneSigs | Agda.Syntax.Concrete.Definitions.Monad |
checkMacroType | Agda.TypeChecking.Rules.Def |
checkMeta | Agda.TypeChecking.Rules.Term |
CheckMetaInst | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkMetaInst | Agda.TypeChecking.MetaVars |
CheckMetaSolution | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkModality | Agda.TypeChecking.Modalities |
checkModality' | Agda.TypeChecking.Modalities |
checkModalityArgs | Agda.TypeChecking.Modalities |
checkModuleArity | Agda.TypeChecking.Rules.Decl |
checkModuleName | Agda.Interaction.FindFile |
CheckModuleParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkMutual | Agda.TypeChecking.Rules.Decl |
checkNamedArg | Agda.TypeChecking.Rules.Term |
CheckNamedWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkNoFixityInRenamingModule | Agda.Syntax.Scope.Monad |
checkNoShadowing | Agda.Syntax.Scope.Monad |
checkOpts | Agda.Interaction.Options |
checkOrInferMeta | Agda.TypeChecking.Rules.Term |
checkOverapplication | Agda.TypeChecking.Injectivity |
CheckOverlap | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
checkPath | Agda.TypeChecking.Rules.Term |
CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPatternLinearity | Agda.Syntax.Abstract.Pattern |
CheckPatternLinearityType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckPatternLinearityValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPiDomain | Agda.TypeChecking.Rules.Term |
checkPiTelescope | Agda.TypeChecking.Rules.Term |
checkpoint | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckpointId | |
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 |
checkpointSubstitution | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkpointSubstitution' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPositivity_ | Agda.TypeChecking.Rules.Decl |
checkPostponedEquations | Agda.TypeChecking.Rewriting.NonLinMatch |
checkPostponedLambda | Agda.TypeChecking.Rules.Term |
checkPostponedLambda0 | Agda.TypeChecking.Rules.Term |
CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPragma | Agda.TypeChecking.Rules.Decl |
checkPragmaOptionConsistency | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkPrimitive | Agda.TypeChecking.Rules.Decl |
CheckProjAppToKnownPrincipalArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkProjAppToKnownPrincipalArg | Agda.TypeChecking.Rules.Application |
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 |
CheckResult | |
1 (Type/Class) | Agda.Interaction.Imports, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.Interaction.Imports, Agda.Compiler.Backend |
checkRewriteRule | Agda.TypeChecking.Rewriting |
CheckRHS | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
checkRHS | Agda.TypeChecking.Rules.Def |
checkSection | Agda.TypeChecking.Rules.Decl |
CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkSectionApplication | Agda.TypeChecking.Rules.Decl |
checkSectionApplication' | Agda.TypeChecking.Rules.Decl |
checkSig | Agda.TypeChecking.Rules.Decl |
CheckSizeLtSat | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkSizeLtSat | Agda.TypeChecking.SizedTypes |
checkSizeNeverZero | Agda.TypeChecking.SizedTypes |
checkSizeVarNeverZero | Agda.TypeChecking.SizedTypes |
checkSolutionForMeta | Agda.TypeChecking.MetaVars |
checkSortOfSplitVar | Agda.TypeChecking.Rules.LHS |
checkStrictlyPositive | Agda.TypeChecking.Positivity |
checkSubtypeIsEqual | Agda.TypeChecking.MetaVars |
checkSyntacticEquality | Agda.TypeChecking.SyntacticEquality |
checkSyntacticEquality' | Agda.TypeChecking.SyntacticEquality |
checkSystemCoverage | Agda.TypeChecking.Rules.Def |
checkTacticAttribute | Agda.TypeChecking.Rules.Term |
CheckTargetType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkTelePiSort | Agda.TypeChecking.Sort |
checkTelescope | Agda.TypeChecking.Rules.Term |
checkTelescope' | Agda.TypeChecking.Rules.Term |
checkTermination_ | Agda.TypeChecking.Rules.Decl |
CheckType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkType | Agda.TypeChecking.CheckInternal |
checkTypeCheckingProblem | Agda.TypeChecking.Constraints |
checkTypedBindings | Agda.TypeChecking.Rules.Term |
checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
checkTypeOfMain' | Agda.Compiler.MAlonzo.Primitives |
checkTypeSignature | Agda.TypeChecking.Rules.Decl |
checkTypeSignature' | Agda.TypeChecking.Rules.Decl |
checkUnderscore | Agda.TypeChecking.Rules.Term |
checkUnquoteDecl | Agda.TypeChecking.Rules.Decl |
checkUnquoteDef | Agda.TypeChecking.Rules.Decl |
checkWhere | Agda.TypeChecking.Rules.Def |
checkWithFunction | Agda.TypeChecking.Rules.Def |
CheckWithFunctionType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
checkWithRHS | Agda.TypeChecking.Rules.Def |
choice | Agda.TypeChecking.Unquote |
choiceP | Agda.Utils.Parser.MemoisedCPS |
ChooseEither | Agda.TypeChecking.Rules.LHS.Problem |
ChooseFlex | Agda.TypeChecking.Rules.LHS.Problem |
chooseFlex | Agda.TypeChecking.Rules.LHS.Problem |
chooseHighlightingMethod | Agda.Interaction.Highlighting.Common |
ChooseLeft | Agda.TypeChecking.Rules.LHS.Problem |
ChooseRight | Agda.TypeChecking.Rules.LHS.Problem |
chop | Agda.Utils.List |
chopWhen | Agda.Utils.List |
Chr | Agda.Syntax.Common.Pretty |
Cl | |
1 (Type/Class) | Agda.TypeChecking.CompiledClause.Compile |
2 (Data Constructor) | Agda.TypeChecking.CompiledClause.Compile |
cl | Agda.TypeChecking.Names |
cl' | Agda.TypeChecking.Names |
ClashesViaRenaming | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClashesViaRenaming_ | Agda.Interaction.Options.Warnings |
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.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Reflected |
5 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
6 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Types, Agda.Syntax.Concrete.Definitions |
7 (Type/Class) | Agda.Syntax.Abstract |
8 (Data Constructor) | Agda.Syntax.Abstract |
Clause' | Agda.Syntax.Abstract |
clauseArgs | Agda.Syntax.Internal.Pattern |
clauseBody | Agda.Syntax.Internal |
clauseCatchall | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.Syntax.Abstract |
clauseElims | Agda.Syntax.Internal.Pattern |
clauseEllipsis | Agda.Syntax.Internal |
clauseExact | Agda.Syntax.Internal |
clauseFullRange | Agda.Syntax.Internal |
clauseLHS | Agda.Syntax.Abstract |
clauseLHSRange | Agda.Syntax.Internal |
clausePats | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.Syntax.Reflected |
clausePerm | Agda.Syntax.Internal.Pattern |
clauseQName | Agda.TypeChecking.Rewriting.Clause |
clauseRecursive | Agda.Syntax.Internal |
clauseRHS | |
1 (Function) | Agda.Syntax.Reflected |
2 (Function) | Agda.Syntax.Abstract |
ClauseS | Agda.Syntax.Abstract |
ClauseSpine | Agda.Syntax.Abstract |
clauseSpine | Agda.Syntax.Abstract |
ClausesPostChecks | Agda.TypeChecking.Rules.Def |
clauseStrippedPats | Agda.Syntax.Abstract |
clauseTel | |
1 (Function) | Agda.Syntax.Internal |
2 (Function) | Agda.Syntax.Reflected |
clauseToRewriteRule | Agda.TypeChecking.Rewriting.Clause |
clauseToSplitClause | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
clauseType | Agda.Syntax.Internal |
clauseUnreachable | Agda.Syntax.Internal |
clauseWhereDecls | Agda.Syntax.Abstract |
clauseWhereModule | Agda.Syntax.Internal |
ClauseZipper | Agda.Interaction.MakeCase |
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 |
clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clearRunningInfo | Agda.Interaction.EmacsCommand |
clearUnknownInstance | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clearWarning | Agda.Interaction.EmacsCommand |
clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
clModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ClockTime | Agda.Utils.Time |
closed | Agda.TypeChecking.Free |
ClosedLevel | Agda.Syntax.Internal |
closedTermToTreeless | Agda.Compiler.ToTreeless |
ClosedType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
closeVerboseBracket | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
closeVerboseBracketException | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
cluster1 | Agda.Utils.Cluster |
cluster1' | Agda.Utils.Cluster |
clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CMaybe | Agda.Utils.Singleton |
cMaybe | Agda.Utils.Singleton |
Cmd_abort | Agda.Interaction.Base |
Cmd_autoAll | Agda.Interaction.Base |
Cmd_autoOne | Agda.Interaction.Base |
Cmd_compile | Agda.Interaction.Base |
Cmd_compute | Agda.Interaction.Base |
Cmd_compute_toplevel | Agda.Interaction.Base |
Cmd_constraints | Agda.Interaction.Base |
Cmd_context | Agda.Interaction.Base |
Cmd_elaborate_give | Agda.Interaction.Base |
Cmd_exit | Agda.Interaction.Base |
Cmd_give | Agda.Interaction.Base |
Cmd_goal_type | Agda.Interaction.Base |
Cmd_goal_type_context | Agda.Interaction.Base |
cmd_goal_type_context_and | Agda.Interaction.InteractionTop |
Cmd_goal_type_context_check | Agda.Interaction.Base |
Cmd_goal_type_context_infer | Agda.Interaction.Base |
Cmd_helper_function | Agda.Interaction.Base |
Cmd_highlight | Agda.Interaction.Base |
Cmd_infer | Agda.Interaction.Base |
Cmd_infer_toplevel | Agda.Interaction.Base |
Cmd_intro | Agda.Interaction.Base |
Cmd_load | Agda.Interaction.Base |
cmd_load' | Agda.Interaction.InteractionTop |
Cmd_load_highlighting_info | Agda.Interaction.Base |
Cmd_make_case | Agda.Interaction.Base |
Cmd_metas | Agda.Interaction.Base |
Cmd_no_metas | Agda.Interaction.Base |
Cmd_refine | Agda.Interaction.Base |
Cmd_refine_or_intro | Agda.Interaction.Base |
Cmd_search_about_toplevel | Agda.Interaction.Base |
Cmd_show_module_contents | Agda.Interaction.Base |
Cmd_show_module_contents_toplevel | Agda.Interaction.Base |
Cmd_show_version | Agda.Interaction.Base |
Cmd_solveAll | Agda.Interaction.Base |
Cmd_solveOne | Agda.Interaction.Base |
Cmd_tokenHighlighting | Agda.Interaction.Base |
Cmd_why_in_scope | Agda.Interaction.Base |
Cmd_why_in_scope_toplevel | Agda.Interaction.Base |
Cmp | Agda.TypeChecking.SizedTypes.Syntax |
cmp | Agda.TypeChecking.SizedTypes.Syntax |
CmpElim | Agda.Interaction.Base |
CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CmpInType | Agda.Interaction.Base |
CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CmpLevels | Agda.Interaction.Base |
CmpSorts | Agda.Interaction.Base |
CmpTeles | Agda.Interaction.Base |
CmpTypes | Agda.Interaction.Base |
CMSet | |
1 (Type/Class) | Agda.Termination.CallMatrix |
2 (Data Constructor) | Agda.Termination.CallMatrix |
cmSet | Agda.Termination.CallMatrix |
CoConName | Agda.Syntax.Scope.Base |
Code | Agda.Syntax.Parser.Literate |
code | Agda.Syntax.Parser.Lexer |
CoDomain | Agda.Utils.TypeLevel |
CoDomain' | Agda.Utils.TypeLevel |
codomainUniv | Agda.Syntax.Internal.Univ, Agda.Syntax.Internal |
coerce | Agda.TypeChecking.Conversion |
coerceAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
coerceSize | Agda.TypeChecking.Conversion |
coerceView | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Cohesion | Agda.Syntax.Common |
CohesionAttribute | Agda.Syntax.Concrete.Attribute |
cohesionAttributeTable | Agda.Syntax.Concrete.Attribute |
CoinductionKit | |
1 (Type/Class) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Data Constructor) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
coinductionKit | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
coinductionKit' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoInductive | Agda.Syntax.Common.Aspect, Agda.Syntax.Common |
CoinductiveDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoinductiveEtaRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoinductiveEtaRecord_ | Agda.Interaction.Options.Warnings |
Coinfective | Agda.Interaction.Options |
CoInfectiveImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoInfectiveImport_ | Agda.Interaction.Options.Warnings |
col | Agda.Termination.SparseMatrix |
coldescr | Agda.Utils.Warshall |
collapseDefault | Agda.Utils.WithDefault |
collapseO | Agda.Termination.Order |
Collection | Agda.Utils.Singleton |
collectStats | Agda.TypeChecking.Serialise.Base |
colon | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
cols | Agda.Termination.SparseMatrix |
Column | Agda.Syntax.Parser.Monad |
ComatchingDisabledForRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
combineHashes | Agda.Utils.Hash |
combineSys | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
combineSys' | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
comma | |
1 (Function) | Agda.Syntax.Common.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
Command | |
1 (Type/Class) | Agda.Interaction.Base |
2 (Data Constructor) | Agda.Interaction.Base |
3 (Type/Class) | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
Command' | Agda.Interaction.Base |
CommandError | Agda.Interaction.ExitCode |
commandLineFlags | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
CommandLineOptions | Agda.Interaction.Options |
commandLineOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CommandM | Agda.Interaction.InteractionTop |
commandMToIO | Agda.Interaction.InteractionTop |
CommandQueue | |
1 (Type/Class) | Agda.Interaction.Base |
2 (Data Constructor) | Agda.Interaction.Base |
commandQueue | Agda.Interaction.Base |
commands | Agda.Interaction.Base |
CommandState | |
1 (Type/Class) | Agda.Interaction.Base |
2 (Data Constructor) | Agda.Interaction.Base |
Comment | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
3 (Data Constructor) | Agda.Syntax.Parser.Literate |
4 (Type/Class) | Agda.Compiler.JS.Syntax |
5 (Data Constructor) | Agda.Compiler.JS.Syntax |
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 |
Compaction | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
compactP | Agda.Utils.Permutation |
Comparable | Agda.Utils.PartialOrd |
comparable | Agda.Utils.PartialOrd |
comparableOrd | Agda.Utils.PartialOrd |
Compare | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
compareArgs | Agda.TypeChecking.Conversion |
CompareAs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
compareAs | Agda.TypeChecking.Conversion |
compareAs' | Agda.TypeChecking.Conversion |
compareAsDir | 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 |
compareInterval | Agda.TypeChecking.Conversion |
compareIrrelevant | Agda.TypeChecking.Conversion |
compareLevel | Agda.TypeChecking.Conversion |
compareMaxViews | Agda.TypeChecking.SizedTypes |
compareMetas | Agda.TypeChecking.Conversion |
compareOffset | Agda.TypeChecking.SizedTypes.Syntax |
CompareResult | Agda.Utils.Favorites |
compareSizes | Agda.TypeChecking.SizedTypes |
compareSizeViews | Agda.TypeChecking.SizedTypes |
compareSort | Agda.TypeChecking.Conversion |
compareTerm | Agda.TypeChecking.Conversion |
compareTerm' | Agda.TypeChecking.Conversion |
compareTermOnFace | Agda.TypeChecking.Conversion |
compareTermOnFace' | Agda.TypeChecking.Conversion |
compareType | Agda.TypeChecking.Conversion |
compareWithFavorites | Agda.Utils.Favorites |
compareWithPol | Agda.TypeChecking.Conversion |
Comparison | Agda.TypeChecking.Monad.Base, Agda.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 |
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 |
compileDef | Agda.Compiler.Backend.Base, Agda.Compiler.Backend |
compileDir | Agda.Compiler.Common |
CompiledRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CompilePragma | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
compilePrim | Agda.Compiler.JS.Compiler |
CompilerBackend | Agda.Interaction.Base |
CompilerPass | |
1 (Type/Class) | Agda.Compiler.ToTreeless |
2 (Data Constructor) | Agda.Compiler.ToTreeless |
compilerPass | Agda.Compiler.ToTreeless |
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 |
compileWithSplitTree | Agda.TypeChecking.CompiledClause.Compile |
CompKit | |
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 |
complement | |
1 (Function) | Agda.Utils.BoolSet |
2 (Function) | Agda.Utils.SmallSet |
complete | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
2 (Function) | Agda.Termination.CallGraph |
completeIter | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
completionStep | Agda.Termination.CallGraph |
compose | Agda.TypeChecking.SizedTypes.Utils |
composeCohesion | Agda.Syntax.Common |
composeErased | Agda.Syntax.Common |
composeFlexRig | Agda.TypeChecking.Free.Lazy |
composeModality | Agda.Syntax.Common |
composeP | Agda.Utils.Permutation |
composePol | Agda.TypeChecking.Polarity |
composeQuantity | Agda.Syntax.Common |
composeRelevance | Agda.Syntax.Common |
composeRetract | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
composeS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
composeVarOcc | Agda.TypeChecking.Free.Lazy |
composeWith | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
ComposeZip | Agda.Utils.Zipper |
ComposeZipper | Agda.Utils.Zipper |
Compress | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
computeDefType | Agda.TypeChecking.ProjectionLike |
computeEdges | Agda.TypeChecking.Positivity |
computeElimHeadType | Agda.TypeChecking.Conversion |
computeErasedConstructorArgs | Agda.Compiler.Treeless.Erase |
computeFixitiesAndPolarities | Agda.Syntax.Scope.Monad |
computeForcingAnnotations | Agda.TypeChecking.Forcing |
computeIgnoreAbstract | Agda.Interaction.BasicOps |
ComputeMode | Agda.Interaction.Base |
computeNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
ComputeOccurrences | Agda.TypeChecking.Positivity |
computeOccurrences | Agda.TypeChecking.Positivity |
computeOccurrences' | Agda.TypeChecking.Positivity |
computePolarity | Agda.TypeChecking.Polarity |
computeSizeConstraint | Agda.TypeChecking.SizedTypes.Solve |
computeUnsolvedInfo | Agda.Interaction.Highlighting.Generate |
computeWrapInput | Agda.Interaction.BasicOps |
Con | |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Abstract |
conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conApp | Agda.TypeChecking.Substitute |
conArgs | Agda.TypeChecking.MetaVars.Occurs |
ConArgType | Agda.TypeChecking.Positivity.Occurrence |
conArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conBranches | Agda.TypeChecking.CompiledClause |
conCase | Agda.TypeChecking.CompiledClause |
Concat | Agda.TypeChecking.Positivity |
concat | Agda.Utils.List1 |
Concat' | Agda.TypeChecking.Positivity |
concatListT | Agda.Utils.ListT |
concatMap1 | Agda.Utils.List1 |
concatMapM | Agda.Utils.Monad |
conComp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConcreteDef | Agda.Syntax.Common |
ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConcreteNames | 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 |
conDataRecord | Agda.Syntax.Internal |
ConDecl | |
1 (Type/Class) | Agda.Utils.Haskell.Syntax |
2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
Condition | Agda.TypeChecking.MetaVars |
ConEndpoint | Agda.TypeChecking.Positivity.Occurrence |
conErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conErasure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conFields | Agda.Syntax.Internal |
configAbove | Agda.Interaction.Library.Base, Agda.Interaction.Library |
configAgdaLibFiles | Agda.Interaction.Library.Base, Agda.Interaction.Library |
configRoot | Agda.Interaction.Library.Base, Agda.Interaction.Library |
Confirmed | Agda.Syntax.Parser.Monad |
confirmLayout | Agda.Syntax.Parser.Layout |
Conflict | Agda.TypeChecking.Rules.LHS.Unify.Types |
conflictAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
conflictDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types |
ConflictingPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConflictingPragmaOptions_ | Agda.Interaction.Options.Warnings |
conflictLeft | Agda.TypeChecking.Rules.LHS.Unify.Types |
conflictParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
conflictRight | Agda.TypeChecking.Rules.LHS.Unify.Types |
conflictType | Agda.TypeChecking.Rules.LHS.Unify.Types |
ConfluenceCheck | Agda.Interaction.Options |
ConfluenceCheckingIncompleteBecauseOfMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConfluenceCheckingIncompleteBecauseOfMeta_ | Agda.Interaction.Options.Warnings |
ConfluenceForCubicalNotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConfluenceForCubicalNotSupported_ | Agda.Interaction.Options.Warnings |
ConfluenceProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
conForced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
conidView' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conInductive | Agda.Syntax.Internal |
ConInfo | Agda.Syntax.Internal |
conInline | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConInsteadOfDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Conj | Agda.TypeChecking.Conversion |
ConK | Agda.Compiler.MAlonzo.Misc |
conKindOfName | Agda.Syntax.Scope.Base |
conKindOfName' | Agda.Syntax.Scope.Base |
ConName | Agda.Syntax.Scope.Base |
conName | Agda.Syntax.Internal |
connectInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConOCon | Agda.Syntax.Common |
ConOfAbs | Agda.Syntax.Translation.AbstractToConcrete |
ConORec | Agda.Syntax.Common |
ConOrigin | Agda.Syntax.Common |
ConOSplit | Agda.Syntax.Common |
ConOSystem | Agda.Syntax.Common |
ConP | |
1 (Data Constructor) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Reflected |
3 (Data Constructor) | Agda.Syntax.Abstract |
conPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConPatEager | Agda.Syntax.Info |
ConPatInfo | |
1 (Type/Class) | Agda.Syntax.Info |
2 (Data Constructor) | Agda.Syntax.Info |
conPatInfo | Agda.Syntax.Info |
ConPatLazy | |
1 (Type/Class) | Agda.Syntax.Info |
2 (Data Constructor) | Agda.Syntax.Info |
conPatLazy | Agda.Syntax.Info |
conPatOrigin | Agda.Syntax.Info |
ConPatternInfo | |
1 (Type/Class) | Agda.Syntax.Internal |
2 (Data Constructor) | Agda.Syntax.Internal |
conPFallThrough | Agda.Syntax.Internal |
conPInfo | Agda.Syntax.Internal |
conPLazy | Agda.Syntax.Internal |
conPRecord | Agda.Syntax.Internal |
conProj | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conPType | Agda.Syntax.Internal |
Cons | |
1 (Data Constructor) | Agda.Utils.IndexedList |
2 (Data Constructor) | Agda.Interaction.EmacsCommand |
3 (Data Constructor) | Agda.TypeChecking.Serialise.Base |
cons | |
1 (Function) | Agda.Utils.List1 |
2 (Function) | Agda.Utils.List2 |
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 |
consOfHIT | Agda.TypeChecking.Datatypes |
conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
consS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
Const | |
1 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Data Constructor) | Agda.Compiler.JS.Syntax |
Constant | Agda.Utils.TypeLevel |
Constant0 | Agda.Utils.TypeLevel |
Constant1 | Agda.Utils.TypeLevel |
ConstK | Agda.TypeChecking.DiscrimTree.Types |
Constr | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Common |
constrainedPrims | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
constraintMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constraintProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Constraints | |
1 (Data Constructor) | Agda.Utils.ProfileOptions |
2 (Type/Class) | Agda.Utils.Warshall |
3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstraintStatus | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constraintUnblocker | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Constructor | |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstructorBlock | Agda.Syntax.Concrete.Definitions.Types |
ConstructorData | |
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 |
ConstructorDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstructorDoesNotFitInData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstructorDoesNotFitInData_ | Agda.Interaction.Options.Warnings |
constructorForm | |
1 (Function) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
2 (Function) | Agda.TypeChecking.Reduce.Monad |
constructorForm' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstructorInfo | Agda.TypeChecking.Datatypes |
ConstructorName | Agda.Syntax.Scope.Base |
ConstructorParametersNotGeneral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constructorTagModifier | Agda.Interaction.JSON |
ConstructorType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
constructs | Agda.TypeChecking.Rules.Data |
constTranspAxiom | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
contains | Agda.Utils.Lens |
containsAbsurdPattern | Agda.Syntax.Abstract.Pattern |
containsAPattern | Agda.Syntax.Abstract.Pattern |
containsAsPattern | Agda.Syntax.Abstract.Pattern |
containsProfileOption | Agda.Utils.ProfileOptions |
ContainsUnsolvedMetaVariables | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
content | Agda.TypeChecking.CompiledClause |
contentsFieldName | Agda.Interaction.JSON |
ContentWithoutField | Agda.Interaction.Library.Base |
Context | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ContextEntry | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ContextLet | Agda.Interaction.Base |
contextOfMeta | Agda.Interaction.BasicOps |
contextSize | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ContextVar | Agda.Interaction.Base |
Continuous | Agda.Syntax.Common |
continuous | Agda.Syntax.Position |
continuousPerLine | Agda.Syntax.Position |
ContradictorySizeConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
conUseSizeLt | Agda.Termination.Monad |
convError | Agda.TypeChecking.Conversion |
Conversion | Agda.Utils.ProfileOptions |
Convert | Agda.Interaction.Highlighting.Precise |
convert | Agda.Interaction.Highlighting.Precise |
convertGuards | Agda.Compiler.Treeless.GuardsToPrims |
CopatternMatching | Agda.Syntax.Common |
CopatternMatchingAllowed | Agda.Syntax.Common |
copatternMatchingAllowed | Agda.Syntax.Common |
CopatternReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
copyDirContent | Agda.Utils.IO.Directory |
copyIfChanged | Agda.Utils.IO.Directory |
copyName | Agda.Syntax.Scope.Monad |
copyScope | Agda.Syntax.Scope.Monad |
copyTerm | Agda.Syntax.Internal.Generic |
CosplitCatchall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CosplitNoRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CosplitNoTarget | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
count | Agda.Utils.Bag |
CountPatternVars | Agda.Syntax.Internal.Pattern |
countPatternVars | Agda.Syntax.Internal.Pattern |
countWithArgs | Agda.TypeChecking.With |
Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Coverage | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
CoverageCheck | Agda.Syntax.Common |
coverageCheck | |
1 (Function) | Agda.Syntax.Concrete.Definitions.Types |
2 (Function) | Agda.TypeChecking.Coverage |
coverageCheckPragma | Agda.Syntax.Concrete.Definitions.Monad |
CoverageIssue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoverageIssue_ | Agda.Interaction.Options.Warnings |
CoverageNoExactSplit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CoverageNoExactSplit_ | Agda.Interaction.Options.Warnings |
CoverageProblem | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
Covering | |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
coveringRange | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
CoverK | Agda.Compiler.MAlonzo.Misc |
coverMissingClauses | Agda.TypeChecking.Coverage.SplitClause |
coverNoExactClauses | Agda.TypeChecking.Coverage.SplitClause |
coverPatterns | Agda.TypeChecking.Coverage.SplitClause |
CoverResult | |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitClause |
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitClause |
coverSplitTree | Agda.TypeChecking.Coverage.SplitClause |
coverUsedClauses | Agda.TypeChecking.Coverage.SplitClause |
covFillTele | Agda.TypeChecking.Coverage.Cubical |
covSplitArg | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
covSplitClauses | Agda.TypeChecking.Coverage.SplitClause, Agda.TypeChecking.Coverage |
CPatternLike | Agda.Syntax.Concrete.Pattern |
CPC | Agda.TypeChecking.Rules.Def |
cpcPartialSplits | Agda.TypeChecking.Rules.Def |
CPUTime | |
1 (Type/Class) | Agda.Utils.Time |
2 (Data Constructor) | Agda.Utils.Time |
createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
createMetaInfo' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
createMissingConIdClause | Agda.TypeChecking.Coverage.Cubical |
createMissingHCompClause | Agda.TypeChecking.Coverage.Cubical |
createMissingIndexedClauses | Agda.TypeChecking.Coverage.Cubical |
createMissingTrXConClause | Agda.TypeChecking.Coverage.Cubical |
createMissingTrXHCompClause | Agda.TypeChecking.Coverage.Cubical |
createMissingTrXTrXClause | Agda.TypeChecking.Coverage.Cubical |
createModule | Agda.Syntax.Scope.Monad |
crInterface | Agda.Interaction.Imports, Agda.Compiler.Backend |
crMode | Agda.Interaction.Imports, Agda.Compiler.Backend |
crModuleInfo | Agda.Interaction.Imports |
crSource | Agda.Interaction.Imports |
crWarnings | Agda.Interaction.Imports, Agda.Compiler.Backend |
CTChar | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTData | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTFloat | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTInt | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTNat | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTQName | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTrans | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
cTreeless | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CTString | Agda.Syntax.Treeless, Agda.Compiler.Backend |
CType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
Cubical | |
1 (Data Constructor) | Agda.Syntax.Common |
2 (Type/Class) | Agda.Syntax.Common |
cubicalCompatibleOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
cubicalOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CubicalPrimitiveNotFullyApplied | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
curAgdaMod | Agda.Compiler.MAlonzo.Misc |
curDefs | Agda.Compiler.Common |
curHsMod | Agda.Compiler.MAlonzo.Misc |
curIF | Agda.Compiler.Common |
curIsMainModule | Agda.Compiler.MAlonzo.Misc |
curMName | Agda.Compiler.Common |
CurrentAccount | Agda.Utils.Benchmark |
currentAccount | Agda.Utils.Benchmark |
currentCxt | Agda.TypeChecking.Names |
CurrentFile | |
1 (Type/Class) | Agda.Interaction.Base |
2 (Data Constructor) | Agda.Interaction.Base |
currentFileArgs | Agda.Interaction.Base |
currentFileModule | Agda.Interaction.Base |
currentFilePath | Agda.Interaction.Base |
currentFileStamp | Agda.Interaction.Base |
CurrentInput | Agda.Syntax.Parser.Alex |
currentModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
currentModuleNameHash | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
currentOrFreshMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
currentTopLevelModule | Agda.TypeChecking.Monad.State, 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 |
CustomBackendError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CustomBackendWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
CustomBackendWarning_ | Agda.Interaction.Options.Warnings |
CutOff | |
1 (Type/Class) | Agda.Termination.CutOff |
2 (Data Constructor) | Agda.Termination.CutOff |
cxtSubst | Agda.TypeChecking.Names |
Cycle | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycle | Agda.Utils.List1 |
cycleAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycleDatatype | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycleOccursIn | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycleParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycleType | Agda.TypeChecking.Rules.LHS.Unify.Types |
cycleVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |