| caf | Idris.Parser |
| calcTotality | Idris.Termination |
| CALL | IRTS.Bytecode |
| calls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CallsWho | |
| 1 (Data Constructor) | Idris.IdeMode |
| 2 (Data Constructor) | Idris.REPL.Commands |
| callsWho | Idris.WhoCalls |
| canBeDConName | Idris.Core.Evaluate |
| CantConvert | Idris.Core.TT |
| CantInferType | Idris.Core.TT |
| CantIntroduce | Idris.Core.TT |
| CantMatch | Idris.Core.TT |
| CantResolve | Idris.Core.TT |
| CantResolveAlts | Idris.Core.TT |
| CantSolveGoal | Idris.Core.TT |
| CantUnify | Idris.Core.TT |
| CASE | IRTS.Bytecode |
| Case | Idris.Core.CaseTree |
| CaseAlt | Idris.Core.CaseTree |
| caseAlt | IRTS.Bytecode |
| CaseAlt' | Idris.Core.CaseTree |
| CaseDef | |
| 1 (Type/Class) | Idris.Core.CaseTree |
| 2 (Data Constructor) | Idris.Core.CaseTree |
| CaseDefs | |
| 1 (Type/Class) | Idris.Core.Evaluate |
| 2 (Data Constructor) | Idris.Core.Evaluate |
| caseExpr | Idris.Parser.Expr, Idris.Parser |
| CaseInfo | |
| 1 (Type/Class) | Idris.Core.Evaluate |
| 2 (Data Constructor) | Idris.Core.Evaluate |
| CaseN | Idris.Core.TT |
| caseName | Idris.Core.TT |
| CaseOp | Idris.Core.Evaluate |
| caseOption | Idris.Parser.Expr, Idris.Parser |
| CaseSplit | Idris.IdeMode |
| CaseSplitAt | Idris.REPL.Commands |
| caseSplitAt | Idris.Interactive |
| cases_compiletime | Idris.Core.Evaluate |
| cases_runtime | Idris.Core.Evaluate |
| CaseTac | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| casetac | Idris.Core.Elaborate |
| CaseTree | Idris.Core.CaseTree |
| CaseType | Idris.Core.CaseTree |
| case_ | Idris.Elab.Term |
| case_alwaysinline | Idris.Core.Evaluate |
| case_decls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| case_inlinable | Idris.Core.Evaluate |
| catchError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| catchIO | Util.System |
| CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CGInfo | |
| 1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| cg_usedpos | Idris.ASTUtils |
| Ch | Idris.Core.TT |
| ChangeDirectory | Idris.REPL.Commands |
| char | Idris.Parser.Helpers, Idris.Parser |
| charLiteral | Idris.Parser.Helpers, Idris.Parser |
| Check | Idris.REPL.Commands |
| check | Idris.Core.Typecheck |
| check' | Idris.Core.Typecheck |
| checkAddDef | Idris.Elab.Utils |
| checkAllCovering | Idris.Termination |
| checkDeclFixity | Idris.Parser.Ops, Idris.Parser |
| checkDeclTotality | Idris.Termination |
| checkDef | Idris.Elab.Utils |
| checkDeprecated | Idris.Elab.Utils |
| checkDocs | Idris.Elab.Utils |
| checkDocstring | Idris.Docstrings |
| checkDSL | Idris.Parser.Data, Idris.Parser |
| Checked | Idris.Docstrings |
| checkFragile | Idris.Elab.Utils |
| checkIfGuarded | Idris.Termination |
| CheckIn | Idris.Core.ProofState, Idris.Core.Elaborate |
| checkInferred | Idris.Elab.Utils |
| checkInjective | Idris.Core.Elaborate |
| checkMP | Idris.Termination |
| checkNameFixity | Idris.Parser.Ops, Idris.Parser |
| checkPiGoal | Idris.Core.Elaborate |
| checkPkg | Idris.Package |
| checkPositive | Idris.Termination |
| checkPossible | Idris.Elab.Clause |
| checkPossibles | Idris.Elab.Clause |
| checkSizeChange | Idris.Termination |
| checkTotality | Idris.Termination |
| checkUndefined | Idris.AbsSyntax |
| checkUnique | Idris.Core.Typecheck |
| checkVisibility | Idris.Elab.Utils |
| check_in | Idris.Core.Elaborate |
| CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Claim | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| claim | Idris.Core.Elaborate |
| ClaimFn | Idris.Core.ProofState, Idris.Core.Elaborate |
| claimFn | Idris.Core.Elaborate |
| claimTy | Idris.Reflection |
| clause | Idris.Parser |
| clean | |
| 1 (Function) | IRTS.Bytecode |
| 2 (Function) | Idris.Package |
| cleanPkg | Idris.Package |
| clearErr | Idris.AbsSyntax |
| clearHighlights | Idris.Output |
| clearIBC | Idris.AbsSyntax |
| clearOrigPats | Idris.AbsSyntax |
| clearParserWarnings | Idris.Parser.Helpers, Idris.Parser |
| clearPTypes | Idris.AbsSyntax |
| clear_totcheck | Idris.AbsSyntax |
| Client | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| closeBlock | Idris.Parser.Helpers, Idris.Parser |
| CmdArg | Idris.Help |
| cmdOptType | Idris.AbsSyntax |
| Codata | Idris.Core.TT |
| codata | Idris.Core.TT |
| Code | Idris.Docstrings |
| CodeBlock | Idris.Docstrings |
| Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegen | Idris.AbsSyntax |
| CodegenArgs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| codegenC | IRTS.CodegenC |
| codegenCats | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| CodeGenerator | IRTS.CodegenCommon |
| CodegenInfo | |
| 1 (Type/Class) | IRTS.CodegenCommon |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| codegenJavaScript | IRTS.CodegenJavaScript |
| codegenNode | IRTS.CodegenJavaScript |
| codegen_ | Idris.Parser |
| collapse | Idris.Termination |
| collapse' | Idris.Termination |
| collapseNothing | Idris.Termination |
| collect | Idris.Parser.Helpers, Idris.Parser |
| collectDeferred | Idris.Elab.Term |
| colour | Idris.Colours |
| ColourArg | Idris.Help |
| colourise | |
| 1 (Function) | Idris.Colours |
| 2 (Function) | Idris.AbsSyntax |
| colouriseBound | Idris.Colours |
| colouriseData | Idris.Colours |
| colouriseFun | Idris.Colours |
| colouriseImplicit | Idris.Colours |
| colouriseKeyword | Idris.Colours |
| colouriseKwd | Idris.Colours |
| colourisePostulate | Idris.Colours |
| colourisePrompt | Idris.Colours |
| colouriseType | Idris.Colours |
| ColourOff | Idris.REPL.Commands |
| ColourOn | Idris.REPL.Commands |
| ColourREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ColourTheme | |
| 1 (Type/Class) | Idris.Colours |
| 2 (Data Constructor) | Idris.Colours |
| ColourType | Idris.Colours |
| ColsWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| columnNum | Idris.Parser.Helpers, Idris.Parser |
| Command | Idris.REPL.Commands |
| commaSeparated | Idris.Parser.Helpers, Idris.Parser |
| commentMarkers | Idris.Parser.Helpers, Idris.Parser |
| Compile | Idris.REPL.Commands |
| compile | IRTS.Compiler |
| compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compileJS | IRTS.JavaScript.AST |
| compileJS' | IRTS.JavaScript.AST |
| compileLibs | IRTS.CodegenCommon |
| compileObjs | IRTS.CodegenCommon |
| compilerFlags | IRTS.CodegenCommon |
| CompileTime | Idris.Core.CaseTree |
| Complete | Idris.Core.TT |
| CompleteFill | Idris.Core.ProofState, Idris.Core.Elaborate |
| complete_fill | Idris.Core.Elaborate |
| Compute | |
| 1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
| 2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| compute | Idris.Core.Elaborate |
| ComputeLet | Idris.Core.ProofState, Idris.Core.Elaborate |
| computeLet | Idris.Core.Elaborate |
| ConCase | Idris.Core.CaseTree |
| conCase | IRTS.Bytecode |
| conGuarded | Idris.Core.Evaluate |
| consoleDecorate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| consoleDisplayAnnotated | Idris.Output |
| ConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ConsoleWidthArg | Idris.Help |
| Const | Idris.Core.TT |
| constAlt | IRTS.Bytecode |
| Constant | Idris.Core.TT |
| constant | Idris.Parser.Expr, Idris.Parser |
| constants | Idris.Parser.Expr, Idris.Parser |
| CONSTCASE | IRTS.Bytecode |
| ConstCase | Idris.Core.CaseTree |
| constCase | IRTS.Bytecode |
| constDocs | Idris.Core.TT |
| constIsType | Idris.Core.TT |
| Constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraintAllowed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraintArg | Idris.Parser.Expr, Idris.Parser |
| ConstraintD | Idris.PartialEval |
| ConstraintFC | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | Idris.Core.TT |
| constraintList | Idris.Parser.Expr, Idris.Parser |
| constraintList1 | Idris.Parser.Expr, Idris.Parser |
| constraintNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constraintPi | Idris.Parser.Expr, Idris.Parser |
| ConstraintS | Idris.PartialEval |
| constraint_ns | Idris.Core.ProofState, Idris.Core.Elaborate |
| Constructor | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| constructor | Idris.Parser.Data, Idris.Parser |
| containsHole | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| containsText | Idris.Docstrings |
| Context | Idris.Core.Evaluate |
| context | Idris.Core.ProofState, Idris.Core.Elaborate |
| convEq | Idris.Core.Evaluate |
| convEq' | Idris.Core.Evaluate |
| converts | Idris.Core.Typecheck |
| convertsC | Idris.Core.Typecheck |
| convSExp | Idris.IdeMode |
| convType | Idris.Core.Typecheck |
| con_names | Idris.Core.TT |
| Core | Idris.REPL.Commands |
| coverage | Idris.AbsSyntax |
| CoverageCheck | Idris.Core.CaseTree |
| CoveringFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| Ctxt | Idris.Core.TT |
| ctxtAlist | Idris.Core.Evaluate |
| ctxt_lookup | Idris.ASTUtils |