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 |
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 |
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 |
CGConf | |
1 (Type/Class) | IRTS.JavaScript.Codegen |
2 (Data Constructor) | IRTS.JavaScript.Codegen |
CGInfo | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CGStats | |
1 (Type/Class) | IRTS.JavaScript.Codegen |
2 (Data Constructor) | IRTS.JavaScript.Codegen |
cg_usedpos | Idris.ASTUtils |
Ch | Idris.Core.TT |
ChangeDirectory | Idris.REPL.Commands |
char | Idris.Parser.Helpers |
charLiteral | Idris.Parser.Helpers |
Check | Idris.REPL.Commands |
check | Idris.Core.Typecheck |
check' | Idris.Core.Typecheck |
checkAddDef | Idris.Elab.Utils |
checkAllCovering | Idris.Termination |
checkDeclFixity | Idris.Parser.Ops |
checkDeclTotality | Idris.Termination |
checkDef | Idris.Elab.Utils |
checkDeprecated | Idris.Elab.Utils |
checkDocs | Idris.Elab.Utils |
checkDocstring | Idris.Docstrings |
checkDSL | Idris.Parser.Data |
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 |
checkNameFixity | Idris.Parser.Ops |
checkPiGoal | Idris.Core.Elaborate |
checkPkg | Idris.Package |
checkPositive | Idris.Termination |
checkPossible | Idris.Elab.Clause |
checkPossibles | Idris.Elab.Clause |
checkSizeChange | 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 |
clause | Idris.Package.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.Options |
closeBlock | Idris.Parser.Helpers |
CmdArg | Idris.Help |
cmdOptType | Idris.AbsSyntax |
Codata | Idris.Core.TT |
codata | Idris.Core.TT |
Code | Idris.Docstrings |
CodeBlock | Idris.Docstrings |
Codegen | Idris.Options |
codegen | Idris.AbsSyntax |
CodegenArgs | Idris.Options |
codegenC | IRTS.CodegenC |
codegenCats | Idris.Options |
CodeGenerator | IRTS.CodegenCommon |
CodegenInfo | |
1 (Type/Class) | IRTS.CodegenCommon |
2 (Data Constructor) | IRTS.CodegenCommon |
codegenJavaScript | IRTS.CodegenJavaScript |
codegenJs | IRTS.JavaScript.Codegen |
codegenNode | IRTS.CodegenJavaScript |
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.Options |
ColourTheme | |
1 (Type/Class) | Idris.Colours |
2 (Data Constructor) | Idris.Colours |
ColourType | Idris.Colours |
ColsWide | Idris.Options |
Command | Idris.REPL.Commands |
commaSep | Idris.Package.Parser |
commaSeparated | Idris.Parser.Helpers |
commentMarkers | Idris.Parser.Ops |
Compile | Idris.REPL.Commands |
compile | IRTS.Compiler |
compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
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 |
ConsoleWidth | Idris.Options |
ConsoleWidthArg | Idris.Help |
Const | Idris.Core.TT |
constAlt | IRTS.Bytecode |
Constant | Idris.Core.TT |
constant | Idris.Parser.Expr |
constants | Idris.Parser.Expr |
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 |
ConstraintD | Idris.PartialEval |
ConstraintFC | |
1 (Type/Class) | Idris.Core.TT |
2 (Data Constructor) | Idris.Core.TT |
constraintList | Idris.Parser.Expr |
constraintList1 | Idris.Parser.Expr |
constraintNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
constraintPi | Idris.Parser.Expr |
ConstraintS | Idris.PartialEval |
constraint_ns | Idris.Core.ProofState, Idris.Core.Elaborate |
Constructor | Idris.AbsSyntaxTree, Idris.AbsSyntax |
constructor | Idris.Parser.Data |
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 |