CA | Idris.ElabDecls |
caf | Idris.Parser |
calcProd | Idris.Coverage |
calcTotality | Idris.Coverage |
CALL | IRTS.Bytecode |
call | IRTS.Java.ASTBuilding |
Callable | IRTS.Java.ASTBuilding |
callableType | IRTS.Java.JTypes |
calls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CantConvert | Core.TT |
CantInferType | Core.TT |
CantIntroduce | Core.TT |
CantResolve | Core.TT |
CantResolveAlts | Core.TT |
CantUnify | Core.TT |
CASE | IRTS.Bytecode |
Case | Core.CaseTree |
CaseAlt | Core.CaseTree |
caseAlt | IRTS.Bytecode |
CaseAlt' | Core.CaseTree |
CaseDef | |
1 (Type/Class) | Core.CaseTree |
2 (Data Constructor) | Core.CaseTree |
CaseDefs | |
1 (Type/Class) | Core.Evaluate |
2 (Data Constructor) | Core.Evaluate |
caseExpr | Idris.ParseExpr, Idris.Parser |
CaseInfo | |
1 (Type/Class) | Core.Evaluate |
2 (Data Constructor) | Core.Evaluate |
CaseN | Core.TT |
CaseOp | Core.Evaluate |
caseOption | Idris.ParseExpr, Idris.Parser |
CaseSplit | Idris.IdeSlave |
CaseSplitAt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
cases_compiletime | Core.Evaluate |
cases_inlined | Core.Evaluate |
cases_runtime | Core.Evaluate |
cases_totcheck | Core.Evaluate |
CaseTrans | Idris.Transforms |
CaseTree | Core.CaseTree |
case_inlinable | Core.Evaluate |
cat | Util.Pretty |
catchIO | Util.System |
CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CGInfo | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Ch | Core.TT |
ChangeDirectory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
char | |
1 (Function) | Util.Pretty |
2 (Function) | Idris.ParseHelpers, Idris.Parser |
charLiteral | Idris.ParseHelpers, Idris.Parser |
charType | IRTS.Java.JTypes |
Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
check | Core.Typecheck |
check' | Core.Typecheck |
CheckConv | Core.TT |
checkDeclTotality | Idris.Coverage |
checkDef | Idris.ElabDecls |
checkDefs | IRTS.Simplified |
checkDSL | Idris.ParseData, Idris.Parser |
CheckIn | Core.ProofState, Core.Elaborate |
checkInferred | Idris.ElabDecls |
checkInjective | Core.Elaborate |
checkMP | Idris.Coverage |
checkPiGoal | Core.Elaborate |
checkPositive | Idris.Coverage |
checkPossible | Idris.ElabDecls |
checkProgram | Core.Typecheck |
checkSizeChange | Idris.Coverage |
checkTotality | Idris.Coverage |
checkUndefined | Idris.AbsSyntax |
check_in | Core.Elaborate |
Chr | Util.Pretty |
CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Claim | Core.ProofState, Core.Elaborate |
claim | Core.Elaborate |
ClassDoc | Idris.Docs |
ClassInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
classInfo | Idris.REPL |
class_ | Idris.Parser |
class_defaults | Idris.AbsSyntaxTree, Idris.AbsSyntax |
class_instances | Idris.AbsSyntaxTree, Idris.AbsSyntax |
class_methods | Idris.AbsSyntaxTree, Idris.AbsSyntax |
class_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
clause | Idris.Parser |
clean | |
1 (Function) | IRTS.Bytecode |
2 (Function) | Pkg.Package |
cleanPkg | Pkg.Package |
clearErr | Idris.AbsSyntax |
clearIBC | Idris.AbsSyntax |
clear_totcheck | Idris.AbsSyntax |
Client | Idris.AbsSyntaxTree, Idris.AbsSyntax |
closeBlock | Idris.ParseHelpers, Idris.Parser |
closure | IRTS.Java.ASTBuilding |
CmdArg | Idris.Help |
cmdOptType | Idris.AbsSyntax |
codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
codegen | Idris.AbsSyntax |
codegenC | IRTS.CodegenC |
codegenJava | IRTS.CodegenJava |
codegenJavaScript | IRTS.CodegenJavaScript |
codegenLLVM | Util.LLVMStubs |
codegen_ | Idris.Parser |
Coinductive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
collapse | Idris.Coverage |
collapse' | Idris.Coverage |
collapseCons | Idris.DataOpts |
collapseNothing | Idris.Coverage |
collapsible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
collect | Idris.ParseHelpers, Idris.Parser |
collectDeferred | Idris.ElabTerm |
colon | Util.Pretty |
colour | Idris.Colours |
ColourArg | Idris.Help |
colourise | Idris.AbsSyntax |
colouriseBound | Idris.Colours |
colouriseData | Idris.Colours |
colouriseFun | Idris.Colours |
colouriseImplicit | Idris.Colours |
colouriseKwd | Idris.Colours |
colourisePrompt | Idris.Colours |
colouriseType | Idris.Colours |
ColourOff | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ColourOn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ColourREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ColourTheme | |
1 (Type/Class) | Idris.Colours |
2 (Data Constructor) | Idris.Colours |
ColourType | Idris.Colours |
columnNum | Idris.ParseHelpers, Idris.Parser |
comma | Util.Pretty |
Command | |
1 (Type/Class) | Core.Elaborate |
2 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Compile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
compile | IRTS.Compiler |
compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CompileTime | Core.CaseTree |
CompleteFill | Core.ProofState, Core.Elaborate |
complete_fill | Core.Elaborate |
comprehension | Idris.ParseExpr, Idris.Parser |
Compute | |
1 (Data Constructor) | Core.ProofState, Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
compute | Core.Elaborate |
ComputeLet | Core.ProofState, Core.Elaborate |
computeLet | Core.Elaborate |
ConCase | Core.CaseTree |
conCase | IRTS.Bytecode |
Const | Core.TT |
constAlt | IRTS.Bytecode |
Constant | Core.TT |
constant | Idris.ParseExpr, Idris.Parser |
CONSTCASE | IRTS.Bytecode |
ConstCase | Core.CaseTree |
constCase | IRTS.Bytecode |
Constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
constraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
constraintArg | Idris.ParseExpr, Idris.Parser |
constraintList | Idris.ParseExpr, Idris.Parser |
constructor | Idris.ParseData, Idris.Parser |
constType | IRTS.Java.JTypes |
Context | Core.Evaluate |
context | Core.ProofState, Core.Elaborate |
contextArray | IRTS.Java.JTypes |
contextParam | IRTS.Java.JTypes |
convEq | Core.Evaluate |
convEq' | Core.Evaluate |
converts | Core.Typecheck |
convertsC | Core.Typecheck |
convSExp | Idris.IdeSlave |
con_names | Idris.AbsSyntaxTree, Idris.AbsSyntax |
coverage | Idris.AbsSyntax |
Ctxt | Core.TT |
ctxtAlist | Core.Evaluate |