<> | IRTS.Java.ASTBuilding |
@! | IRTS.Java.ASTBuilding |
@:= | IRTS.Java.ASTBuilding |
Abandon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
accData | Idris.ParseHelpers, Idris.Parser |
Accessibility | Idris.Core.Evaluate |
accessibility | Idris.ParseHelpers, Idris.Parser |
addAcc | Idris.ParseHelpers, Idris.Parser |
addAlist | Idris.Core.TT |
addApps | IRTS.Defunctionalise |
addBinder | Idris.Core.TT |
addCasedef | Idris.Core.Evaluate |
addClass | Idris.AbsSyntax |
AddClause | Idris.IdeSlave |
AddClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
addCoercion | Idris.AbsSyntax |
addConstraints | Idris.AbsSyntax |
addCtxtDef | Idris.Core.Evaluate |
addDatatype | Idris.Core.Evaluate |
addDef | Idris.Core.TT |
addDeferred | Idris.AbsSyntax |
addDeferred' | Idris.AbsSyntax |
addDeferredTyCon | Idris.AbsSyntax |
addDocStr | Idris.AbsSyntax |
addDyLib | Idris.AbsSyntax |
addErrRev | Idris.AbsSyntax |
addFlag | Idris.AbsSyntax |
addFn | IRTS.Lang, IRTS.Defunctionalise |
addFunctionErrorHandlers | Idris.AbsSyntax |
addHdr | Idris.AbsSyntax |
addHides | Idris.Parser |
addIBC | Idris.AbsSyntax |
addImpl | Idris.AbsSyntax |
addImpl' | Idris.AbsSyntax |
addImplBound | Idris.AbsSyntax |
addImplBoundInf | Idris.AbsSyntax |
addImplPat | Idris.AbsSyntax |
addImportDir | Idris.AbsSyntax |
addInstance | Idris.AbsSyntax |
addInternalApp | Idris.AbsSyntax |
addLangExt | Idris.AbsSyntax |
addLib | Idris.AbsSyntax |
AddMissing | |
1 (Data Constructor) | Idris.IdeSlave |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
addNameHint | Idris.AbsSyntax |
addNameIdx | Idris.AbsSyntax |
addNameIdx' | Idris.AbsSyntax |
addObjectFile | Idris.AbsSyntax |
addOperator | Idris.Core.Evaluate |
AddProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
AddProofClause | Idris.IdeSlave |
AddProofClauseFrom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
addStatics | Idris.AbsSyntax |
addTags | IRTS.Lang, IRTS.Defunctionalise |
addToBlock | IRTS.Java.ASTBuilding |
addToCalledG | Idris.AbsSyntax |
addToCG | Idris.AbsSyntax |
addToCtxt | Idris.Core.Evaluate |
ADDTOP | IRTS.Bytecode |
addTrans | Idris.AbsSyntax |
addTyDecl | Idris.Core.Evaluate |
addUsingConstraints | Idris.AbsSyntax |
aiFn | Idris.AbsSyntax |
allImportDirs | Idris.AbsSyntax |
allNames | Idris.AbsSyntax |
allNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
allNothing | Idris.Coverage |
allowImp | Idris.ParseExpr, Idris.Parser |
AlreadyDefined | Idris.Core.TT |
alt | Idris.ParseExpr, Idris.Parser |
AnnBoundName | Idris.Core.TT |
AnnConstData | Idris.Core.TT |
AnnConstType | Idris.Core.TT |
AnnFC | Idris.Core.TT |
AnnName | Idris.Core.TT |
AnySyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
App | Idris.Core.TT |
app | Idris.ParseExpr, Idris.Parser |
apply | Idris.Core.Elaborate |
apply' | Idris.Core.Elaborate |
apply2 | Idris.Core.Elaborate |
ApplyCase | IRTS.Defunctionalise |
applyDataOpt | Idris.DataOpts |
applyDataOptRT | Idris.DataOpts |
applyOpts | Idris.DataOpts |
ApplyTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
apply_elab | Idris.Core.Elaborate |
arg | |
1 (Function) | Idris.Core.Elaborate |
2 (Function) | Idris.ParseExpr, Idris.Parser |
argExpr | Idris.Parser |
ArgOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
argopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
argsdef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
argsused | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ArithTy | Idris.Core.TT |
arithTyToJType | IRTS.Java.JTypes |
arity | Idris.Core.TT |
array | IRTS.Java.JTypes |
arrayInitExps | IRTS.Java.ASTBuilding |
arraysType | IRTS.Java.JTypes |
AssertTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ASSIGN | IRTS.Bytecode |
assign | IRTS.Bytecode |
ASSIGNCONST | IRTS.Bytecode |
assumptionNames | Idris.Prover |
At | Idris.Core.TT |
ATFloat | Idris.Core.TT |
ATInt | Idris.Core.TT |
Attack | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
attack | Idris.Core.Elaborate |
AType | Idris.Core.TT |
AutomaticWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
AutoWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
B16 | Idris.Core.TT |
B16V | Idris.Core.TT |
B32 | Idris.Core.TT |
B32V | Idris.Core.TT |
B64 | Idris.Core.TT |
B64V | Idris.Core.TT |
B8 | Idris.Core.TT |
B8V | Idris.Core.TT |
backtick | Idris.ParseOps, Idris.Parser |
banner | Idris.REPL |
BASETOP | IRTS.Bytecode |
BC | |
1 (Type/Class) | IRTS.BCImp |
2 (Type/Class) | IRTS.Bytecode |
bc | |
1 (Function) | IRTS.BCImp |
2 (Function) | IRTS.Bytecode |
BCAsm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
bdecode | Idris.IBC |
BE | IRTS.Lang, IRTS.Defunctionalise |
BelieveMe | Idris.Core.Evaluate |
bencode | Idris.IBC |
BI | Idris.Core.TT |
bi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Bigger | Idris.AbsSyntaxTree, Idris.AbsSyntax |
bigInteger | IRTS.Java.ASTBuilding |
bigIntegerType | IRTS.Java.JTypes |
binary | Idris.ParseOps, Idris.Parser |
Bind | Idris.Core.TT |
bindAll | Idris.Core.TT |
Binder | Idris.Core.TT |
binderTy | Idris.Core.TT |
binderVal | Idris.Core.TT |
Binding | Idris.AbsSyntaxTree, Idris.AbsSyntax |
bindingOf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
bindList | Idris.ParseHelpers, Idris.Parser |
bindTyArgs | Idris.Core.TT |
bold | Idris.Colours |
BoolAtom | Idris.IdeSlave |
Bound | Idris.Core.TT |
boundNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
BoundVarColour | Idris.Colours |
boundVarColour | Idris.Colours |
box | IRTS.Java.JTypes |
brace_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
bracketed | Idris.ParseExpr, Idris.Parser |
bracketedExpr | Idris.ParseExpr, Idris.Parser |
BufferType | Idris.Core.TT |
bugaddr | Idris.Delaborate |
build | |
1 (Function) | Idris.ElabTerm |
2 (Function) | IRTS.Compiler |
buildMods | Pkg.Package |
buildPkg | Pkg.Package |
buildSCG | Idris.Coverage |
buildSCG' | Idris.Coverage |
buildTC | Idris.ElabTerm |
buildTree | Idris.Chaser |
ByReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Bytecode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
byteType | IRTS.Java.JTypes |
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 | Idris.Core.TT |
CantInferType | Idris.Core.TT |
CantIntroduce | 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.ParseExpr, Idris.Parser |
CaseInfo | |
1 (Type/Class) | Idris.Core.Evaluate |
2 (Data Constructor) | Idris.Core.Evaluate |
CaseN | Idris.Core.TT |
CaseOp | Idris.Core.Evaluate |
caseOption | Idris.ParseExpr, Idris.Parser |
CaseSplit | Idris.IdeSlave |
CaseSplitAt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
cases_compiletime | Idris.Core.Evaluate |
cases_inlined | Idris.Core.Evaluate |
cases_runtime | Idris.Core.Evaluate |
cases_totcheck | Idris.Core.Evaluate |
CaseTrans | Idris.Transforms |
CaseTree | Idris.Core.CaseTree |
case_inlinable | Idris.Core.Evaluate |
CExport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CGInfo | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Ch | Idris.Core.TT |
ChangeDirectory | Idris.AbsSyntaxTree, Idris.AbsSyntax |
char | Idris.ParseHelpers, Idris.Parser |
charLiteral | Idris.ParseHelpers, Idris.Parser |
charType | IRTS.Java.JTypes |
Check | Idris.AbsSyntaxTree, Idris.AbsSyntax |
check | Idris.Core.Typecheck |
check' | Idris.Core.Typecheck |
CheckConv | Idris.Core.TT |
checkDeclTotality | Idris.Coverage |
checkDef | Idris.ElabDecls |
checkDefs | IRTS.Simplified |
checkDSL | Idris.ParseData, Idris.Parser |
CheckIn | Idris.Core.ProofState, Idris.Core.Elaborate |
checkInferred | Idris.ElabDecls |
checkInjective | Idris.Core.Elaborate |
checkMP | Idris.Coverage |
checkPiGoal | Idris.Core.Elaborate |
checkPkg | Pkg.Package |
checkPositive | Idris.Coverage |
checkPossible | Idris.ElabDecls |
checkSizeChange | Idris.Coverage |
checkTotality | Idris.Coverage |
checkUndefined | Idris.AbsSyntax |
check_in | Idris.Core.Elaborate |
CI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Claim | Idris.Core.ProofState, Idris.Core.Elaborate |
claim | Idris.Core.Elaborate |
classBlock | Idris.Parser |
ClassDoc | Idris.Docs |
ClassInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
classInfo | Idris.REPL |
class_ | Idris.Parser |
class_defaults | Idris.AbsSyntaxTree, Idris.AbsSyntax |
class_default_superclasses | 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 |
clearOrigPats | Idris.AbsSyntax |
clearPTypes | 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 |
codata | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
codegen | Idris.AbsSyntax |
codegenC | IRTS.CodegenC |
codegenJava | IRTS.CodegenJava |
codegenJavaScript | IRTS.CodegenJavaScript |
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 |
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 |
ColsWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
columnNum | Idris.ParseHelpers, Idris.Parser |
Command | |
1 (Type/Class) | Idris.Core.Elaborate |
2 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Compile | Idris.AbsSyntaxTree, Idris.AbsSyntax |
compile | IRTS.Compiler |
compiled_so | Idris.AbsSyntaxTree, Idris.AbsSyntax |
CompileTime | Idris.Core.CaseTree |
CompleteFill | Idris.Core.ProofState, Idris.Core.Elaborate |
complete_fill | Idris.Core.Elaborate |
comprehension | Idris.ParseExpr, Idris.Parser |
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 |
Conditional | Idris.AbsSyntaxTree, Idris.AbsSyntax |
consoleDecorate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
consoleDisplayAnnotated | Idris.AbsSyntax |
ConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ConsoleWidthArg | Idris.Help |
Const | Idris.Core.TT |
constAlt | IRTS.Bytecode |
Constant | Idris.Core.TT |
constant | Idris.ParseExpr, Idris.Parser |
CONSTCASE | IRTS.Bytecode |
ConstCase | Idris.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 | Idris.Core.Evaluate |
context | Idris.Core.ProofState, Idris.Core.Elaborate |
contextArray | IRTS.Java.JTypes |
contextParam | IRTS.Java.JTypes |
convEq | Idris.Core.Evaluate |
convEq' | Idris.Core.Evaluate |
converts | Idris.Core.Typecheck |
convertsC | Idris.Core.Typecheck |
convSExp | Idris.IdeSlave |
con_names | Idris.AbsSyntaxTree, Idris.AbsSyntax |
coverage | Idris.AbsSyntax |
Ctxt | Idris.Core.TT |
ctxtAlist | Idris.Core.Evaluate |
DAlt | IRTS.Defunctionalise |
DApp | IRTS.Defunctionalise |
Data | Idris.Core.TT |
DataColour | Idris.Colours |
dataColour | Idris.Colours |
DataDoc | Idris.Docs |
DataErrRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dataI | Idris.ParseData, Idris.Parser |
DataMI | Idris.Core.Evaluate |
DataOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DataOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dataOpts | Idris.ParseData, Idris.Parser |
DataOutput | Idris.Core.TT |
Datatype | Idris.Core.TT |
data_ | Idris.ParseData, Idris.Parser |
data_opts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DbgLevel | IRTS.CodegenCommon |
DC | IRTS.Defunctionalise |
DCase | IRTS.Defunctionalise |
DChkCase | IRTS.Defunctionalise |
DCon | Idris.Core.TT |
DConCase | IRTS.Defunctionalise |
DConst | IRTS.Defunctionalise |
DConstCase | IRTS.Defunctionalise |
DConstructor | IRTS.Defunctionalise |
DDecl | IRTS.Defunctionalise |
DDefaultCase | IRTS.Defunctionalise |
DDefs | IRTS.Defunctionalise |
debind | Idris.DSL |
debindApp | Idris.DSL |
DEBUG | IRTS.CodegenCommon |
DebugInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
decl | Idris.Parser |
decl' | Idris.Parser |
declare | IRTS.Defunctionalise |
declared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
declareFinalObjectArray | IRTS.Java.ASTBuilding |
declArgs | IRTS.Compiler |
decorateid | Idris.ElabDecls |
decoration | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Def | Idris.Core.Evaluate |
defaultAlt | IRTS.Bytecode |
DefaultCase | Idris.Core.CaseTree |
DefaultEliminator | Idris.AbsSyntaxTree, Idris.AbsSyntax |
defaultOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DefaultPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
defaultSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
defaultTheme | Idris.Colours |
DefaultTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
default_access | Idris.AbsSyntaxTree, Idris.AbsSyntax |
default_total | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Defer | Idris.Core.ProofState, Idris.Core.Elaborate |
defer | Idris.Core.Elaborate |
deferred | Idris.Core.ProofState, Idris.Core.Elaborate |
DeferType | Idris.Core.ProofState, Idris.Core.Elaborate |
deferType | Idris.Core.Elaborate |
defer_totcheck | Idris.AbsSyntax |
defined | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Defn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
defunctionalise | IRTS.Defunctionalise |
delab | Idris.Delaborate |
delab' | Idris.Delaborate |
delabMV | Idris.Delaborate |
delabTy | Idris.Delaborate |
delabTy' | Idris.Delaborate |
DError | IRTS.Defunctionalise |
desugar | Idris.DSL |
DExp | IRTS.Defunctionalise |
DForeign | IRTS.Defunctionalise |
DFun | IRTS.Defunctionalise |
Dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dictionary | Idris.AbsSyntaxTree, Idris.AbsSyntax |
directive | Idris.Parser |
disallowImp | Idris.ParseExpr, Idris.Parser |
disamb | Idris.ParseExpr, Idris.Parser |
discard | Idris.Core.TT |
displayHelp | Idris.REPL |
DLet | IRTS.Defunctionalise |
DNothing | IRTS.Defunctionalise |
DoBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DoBindP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
doBlock | Idris.ParseExpr, Idris.Parser |
Doc | |
1 (Type/Class) | Idris.Docs |
2 (Data Constructor) | Idris.Docs |
docClass | Idris.Docs |
docComment | Idris.ParseHelpers, Idris.Parser |
docData | Idris.Docs |
docFun | Idris.Docs |
DocStr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DoExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DoLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DoLetP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
done | Idris.Core.ProofState, Idris.Core.Elaborate |
dontunify | Idris.Core.ProofState, Idris.Core.Elaborate |
DOp | IRTS.Defunctionalise |
DoProofSearch | Idris.AbsSyntaxTree, Idris.AbsSyntax |
doubleType | IRTS.Java.JTypes |
do_ | Idris.ParseExpr, Idris.Parser |
DProj | IRTS.Defunctionalise |
dropGiven | Idris.Core.ProofState, Idris.Core.Elaborate |
DSL | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl | Idris.ParseData, Idris.Parser |
DSL' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_apply | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_bind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_info | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_lambda | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_let | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_pure | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_return | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dsl_var | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dumpBC | IRTS.DumpBC |
DumpCases | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dumpDefaultInstance | Idris.REPL |
DumpDefun | Idris.AbsSyntaxTree, Idris.AbsSyntax |
dumpDefuns | IRTS.Defunctionalise |
dumpInstance | Idris.REPL |
dumpMethod | Idris.REPL |
dumpprobs | Idris.Core.Elaborate |
dumpState | Idris.Prover |
DUpdate | IRTS.Defunctionalise |
DV | IRTS.Defunctionalise |
Dynamic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
DynamicLib | Util.DynamicLinker |
DynamicLink | Idris.AbsSyntaxTree, Idris.AbsSyntax |
d_cons | |
1 (Function) | Idris.Core.TT |
2 (Function) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
d_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
d_tcon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
d_type | Idris.Core.TT |
d_typename | Idris.Core.TT |
d_typetag | Idris.Core.TT |
EA | Idris.ElabDecls |
EAll | Idris.ElabDecls |
EDefns | Idris.ElabDecls |
Edit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
edit | Idris.REPL |
eEVAL | IRTS.Defunctionalise |
EInfo | Idris.ElabTerm |
EitherErr | Idris.AbsSyntax |
Elab | Idris.Core.Elaborate |
elab | Idris.ElabTerm |
Elab' | Idris.Core.Elaborate |
elabCaseBlock | Idris.ElabDecls |
elabClass | Idris.ElabDecls |
elabClause | Idris.ElabDecls |
elabClauses | Idris.ElabDecls |
elabCon | Idris.ElabDecls |
ElabD | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elabData | Idris.ElabDecls |
elabDecl | Idris.ElabDecls |
elabDecl' | Idris.ElabDecls |
elabDecls | Idris.ElabDecls |
elabEliminator | Idris.ElabDecls |
ElabInfo | Idris.ElabTerm |
elabInstance | Idris.ElabDecls |
elaborate | Idris.Core.Elaborate |
Elaborating | Idris.Core.TT |
elabPE | Idris.ElabDecls |
elabPostulate | Idris.ElabDecls |
elabPrims | Idris.ElabDecls |
elabProvider | Idris.ElabDecls |
elabRecord | Idris.ElabDecls |
ElabState | Idris.Core.Elaborate |
elabStep | Idris.Prover |
elabTransform | Idris.ElabDecls |
elabType | Idris.ElabDecls |
elabType' | Idris.ElabDecls |
elabVal | Idris.ElabDecls |
elabValBind | Idris.ElabDecls |
ElabWhat | Idris.ElabDecls |
elimDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EliminatorState | Idris.ElabDecls |
elimMethElim | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elimMethElimTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ElimN | Idris.Core.TT |
elimName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
elog | Idris.Core.Elaborate |
emptyContext | Idris.Core.TT |
emptyFC | Idris.Core.TT |
EmptyMI | Idris.Core.Evaluate |
Endianness | IRTS.Lang, IRTS.Defunctionalise |
EndUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
end_unify | Idris.Core.Elaborate |
Env | Idris.Core.TT |
envAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
environment | IRTS.CodegenCommon |
envlen | Idris.Core.TT |
EnvTT | Idris.Core.TT |
envTupleType | Idris.ElabTerm |
eol | Idris.ParseHelpers, Idris.Parser |
eqCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
eqProp | Idris.ParseHelpers, Idris.Parser |
eqTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Equiv | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
equiv | Idris.Core.Elaborate |
Erased | Idris.Core.TT |
Err | Idris.Core.TT |
Err' | Idris.Core.TT |
errAt | Idris.Core.Elaborate |
ErrContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
errContext | Idris.AbsSyntax |
errEnv | Idris.Core.Typecheck |
errLine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ERROR | IRTS.Bytecode |
Error | Idris.Core.TC, Idris.Core.TT |
ErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrorReflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ErrorReportPart | Idris.Core.TT |
ErrorReverse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
errReverse | Idris.ErrReverse |
erun | Idris.Core.Elaborate |
ES | Idris.Core.Elaborate |
ETypes | Idris.ElabDecls |
Eval | |
1 (Data Constructor) | Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
EvalApply | IRTS.Defunctionalise |
EvalCase | IRTS.Defunctionalise |
evalD | IRTS.Inliner |
EvalIn | Idris.Core.ProofState, Idris.Core.Elaborate |
eval_in | Idris.Core.Elaborate |
Exact | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
exact | Idris.Core.Elaborate |
exceptionType | IRTS.Java.JTypes |
execElab | Idris.Core.Elaborate |
execScript | Idris.REPL |
Executable | IRTS.CodegenCommon |
Execute | Idris.AbsSyntaxTree, Idris.AbsSyntax |
execute | Idris.Core.Execute |
ExecVal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
existsCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Exp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandDo | Idris.DSL |
ExpandLet | Idris.Core.ProofState, Idris.Core.Elaborate |
expandLet | Idris.Core.Elaborate |
expandNS | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expandParams | Idris.AbsSyntax |
expandParamsD | Idris.AbsSyntax |
expl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
explicit | Idris.Core.Elaborate |
ExplicitD | Idris.PartialEval |
explicitNames | Idris.Core.TT |
ExplicitS | Idris.PartialEval |
expl_param | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Expr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
expr | Idris.ParseExpr, Idris.Parser |
expr' | Idris.ParseExpr, Idris.Parser |
ExprArg | Idris.Help |
extendWithNull | IRTS.Java.ASTBuilding |
Extension | Idris.AbsSyntaxTree, Idris.AbsSyntax |
extension | Idris.ParseExpr, Idris.Parser |
extensions | Idris.ParseExpr, Idris.Parser |
externalExpr | Idris.ParseExpr, Idris.Parser |
extraHelp | Idris.Help |
failMsg | Idris.Core.TT |
Fails | Idris.Core.Unify |
falseDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
falseOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
falseTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fancifyAnnots | Idris.AbsSyntax |
FAny | IRTS.Lang, IRTS.Defunctionalise |
FArith | IRTS.Lang, IRTS.Defunctionalise |
FC | |
1 (Type/Class) | Idris.Core.TT |
2 (Data Constructor) | Idris.Core.TT |
FC' | |
1 (Type/Class) | Idris.Core.TT |
2 (Data Constructor) | Idris.Core.TT |
FCallType | IRTS.Lang, IRTS.Defunctionalise |
FConstructor | IRTS.Lang, IRTS.Defunctionalise |
fc_column | Idris.Core.TT |
fc_fname | Idris.Core.TT |
fc_line | Idris.Core.TT |
FFunction | IRTS.Lang, IRTS.Defunctionalise |
FFunctionIO | IRTS.Lang, IRTS.Defunctionalise |
FileArg | Idris.Help |
fileFC | Idris.Core.TT |
Filename | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fileName | Idris.ParseHelpers, Idris.Parser |
Fill | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fill | Idris.Core.Elaborate |
finalise | Idris.Core.TT |
findCalls | Idris.Core.CaseTree |
findFC | Idris.Parser |
findImport | Idris.Imports |
findInPath | Idris.Imports |
findInstances | Idris.ElabTerm |
findStatics | Idris.AbsSyntax |
findUnusedArgs | Idris.UnusedArgs |
findUsedArgs | Idris.Core.CaseTree |
Fix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fixColour | Idris.REPL |
FixDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fixErrorMsg | Idris.ParseHelpers, Idris.Parser |
Fixity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fixity | Idris.ParseOps, Idris.Parser |
fixityType | Idris.ParseOps, Idris.Parser |
Fl | Idris.Core.TT |
FLang | IRTS.Lang, IRTS.Defunctionalise |
float | Idris.ParseHelpers, Idris.Parser |
fmapMB | Idris.Core.TT |
FnCase | Idris.Core.CaseTree |
fnDecl | Idris.Parser |
fnDecl' | Idris.Parser |
fnName | Idris.ParseOps, Idris.Parser |
FnOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
FnOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
fnOpts | Idris.Parser |
fnub | Idris.Coverage |
fnub' | Idris.Coverage |
FObject | IRTS.Lang, IRTS.Defunctionalise |
Focus | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
focus | Idris.Core.Elaborate |
Forall | Idris.Core.ProofState, Idris.Core.Elaborate |
forall | Idris.Core.Elaborate |
Forceability | Idris.AbsSyntaxTree, Idris.AbsSyntax |
forceable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
forceArgs | Idris.DataOpts |
forcedArgSeq | Idris.DataOpts |
forcedCnt | Idris.DataOpts |
ForceMap | Idris.DataOpts |
force_term | Idris.Core.Elaborate |
forCodegen | Idris.AbsSyntax |
FOREIGNCALL | IRTS.Bytecode |
foreignType | IRTS.Java.JTypes |
foreignWrapperType | IRTS.Java.JTypes |
forget | Idris.Core.TT |
Forgot | Idris.Core.TT |
FPtr | IRTS.Lang, IRTS.Defunctionalise |
freeNames | Idris.Core.TT |
fromTTMaybe | Idris.ElabTerm |
Frozen | Idris.Core.Evaluate |
FStatic | IRTS.Lang, IRTS.Defunctionalise |
FString | IRTS.Lang, IRTS.Defunctionalise |
FType | IRTS.Lang, IRTS.Defunctionalise |
fullExpr | Idris.ParseExpr, Idris.Parser |
fullTactic | Idris.ParseExpr, Idris.Parser |
Function | Idris.Core.Evaluate |
FunctionColour | Idris.Colours |
functionColour | Idris.Colours |
FunDoc | |
1 (Data Constructor) | Idris.Docs |
2 (Type/Class) | Idris.Docs |
FUnit | IRTS.Lang, IRTS.Defunctionalise |
FunOutput | Idris.Core.TT |
GD | Idris.Core.ProofState, Idris.Core.Elaborate |
genAll | Idris.Coverage |
genArgs | IRTS.Defunctionalise |
genClauses | Idris.Coverage |
getAll | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getAllNames | Idris.AbsSyntax |
getArgTys | Idris.Core.TT |
getAux | Idris.Core.Elaborate |
getBC | Idris.REPL |
getCC | IRTS.System |
getClause | Idris.CaseSplit |
getCmdLine | Idris.AbsSyntax |
getCodegen | Idris.REPL |
getCoercionsTo | Idris.AbsSyntax |
getColour | Idris.REPL |
getConsts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getContext | Idris.AbsSyntax |
getCPU | Idris.REPL |
getDocs | Idris.Docs |
getDumpCases | Idris.AbsSyntax |
getDumpDefun | Idris.AbsSyntax |
getErrColumn | Idris.Error |
getErrLine | Idris.Error |
getExecScript | Idris.REPL |
getExecutablePom | IRTS.System |
getExps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getFargpos | Idris.UnusedArgs |
getFC | Idris.ParseHelpers, Idris.Parser |
getFile | Idris.REPL |
getFlags | Idris.AbsSyntax |
getFn | IRTS.Defunctionalise |
getForcedArgs | Idris.DataOpts |
getFTypes | IRTS.Compiler |
getFunctionErrorHandlers | Idris.AbsSyntax |
getHdrs | Idris.AbsSyntax |
getIBCSubDir | Idris.REPL |
getIdrisLibDir | IRTS.System |
getIdrisUserDataDir | Idris.REPL |
getImportDir | Idris.REPL |
getImps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getIncFlags | IRTS.System |
getInferTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getInferType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getInitScript | Idris.REPL |
getInternalApp | Idris.AbsSyntax |
getIState | Idris.AbsSyntax |
getLanguageExt | Idris.REPL |
getLibFlags | IRTS.System |
getLibs | Idris.AbsSyntax |
getLog | Idris.Core.Elaborate |
getModuleFiles | Idris.Chaser |
getMvn | IRTS.System |
getName | Idris.AbsSyntax |
getNameFrom | Idris.Core.Elaborate |
getNameHints | Idris.AbsSyntax |
getNextName | IRTS.Lang, IRTS.Defunctionalise |
getNoBanner | Idris.AbsSyntax |
getObjectFiles | Idris.AbsSyntax |
getOptLevel | Idris.REPL |
getOutput | Idris.REPL |
getOutputTy | Idris.REPL |
getPArity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getPBtys | Idris.ElabDecls |
getPkg | Idris.REPL |
getPkgCheck | Idris.REPL |
getPkgClean | Idris.REPL |
getPkgDir | Idris.REPL |
getPkgREPL | Idris.REPL |
getPrim | IRTS.Compiler |
getPriority | Idris.AbsSyntax |
getProofClause | Idris.CaseSplit |
getProvided | Idris.Providers |
getQuiet | Idris.AbsSyntax |
getRetTy | Idris.Core.TT |
getScreenWidth | Util.ScreenSize |
getScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getSO | Idris.AbsSyntax |
getSpecApps | Idris.PartialEval |
getTargetDir | IRTS.System |
getTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
getTotality | Idris.AbsSyntax |
getTriple | Idris.REPL |
getUndefined | Idris.AbsSyntax |
getUnifyLog | Idris.Core.Elaborate |
getUniq | Idris.CaseSplit |
getWidth | Idris.AbsSyntax |
get_context | Idris.Core.Elaborate |
get_deferred | Idris.Core.Elaborate |
get_env | Idris.Core.Elaborate |
get_guess | Idris.Core.Elaborate |
get_holes | Idris.Core.Elaborate |
get_instances | Idris.Core.Elaborate |
get_probs | Idris.Core.Elaborate |
get_term | Idris.Core.Elaborate |
get_type | Idris.Core.Elaborate |
get_type_val | Idris.Core.Elaborate |
GHole | Idris.Core.TT |
Glob | IRTS.Lang, IRTS.Defunctionalise |
globalContext | IRTS.Java.JTypes |
globalContextID | IRTS.Java.JTypes |
Goal | Idris.Core.ProofState, Idris.Core.Elaborate |
goal | Idris.Core.Elaborate |
goalAtFocus | Idris.Core.ProofState, Idris.Core.Elaborate |
GoalType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
goalType | Idris.Core.ProofState, Idris.Core.Elaborate |
groupsOf | IRTS.Defunctionalise |
gteProp | Idris.ParseHelpers, Idris.Parser |
gtProp | Idris.ParseHelpers, Idris.Parser |
Guess | Idris.Core.TT |
Help | Idris.AbsSyntaxTree, Idris.AbsSyntax |
help | Idris.Help |
helphead | Idris.REPL |
Hidden | Idris.Core.Evaluate |
HideDisplay | Idris.AbsSyntaxTree, Idris.AbsSyntax |
hide_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
HNF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
hnf | Idris.Core.Evaluate |
HNF_Compute | Idris.Core.ProofState, Idris.Core.Elaborate |
hnf_compute | Idris.Core.Elaborate |
Hole | Idris.Core.TT |
holes | Idris.Core.ProofState, Idris.Core.Elaborate |
hsimpleExpr | Idris.ParseExpr, Idris.Parser |
hvar | IRTS.Simplified |
I | Idris.Core.TT |
IA | Idris.ElabDecls |
IBC | Idris.Imports |
ibc | Idris.IBC |
IBCAccess | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCCG | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCCGFlag | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCCoercion | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCData | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCDef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCDoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCDyLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCErrRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCFile | |
1 (Type/Class) | Idris.IBC |
2 (Data Constructor) | Idris.IBC |
IBCFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCFlags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCFunctionErrorHandler | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCHeader | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCKeyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCLib | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCLineApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCMetaInformation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCNameHint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCObj | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ibcPath | Idris.Imports |
ibcPathNoFallback | Idris.Imports |
ibcPathWithFallback | Idris.Imports |
IBCStatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCSubDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCTotal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IBCTrans | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ibcVersion | Idris.IBC |
IBCWrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ibc_access | Idris.IBC |
ibc_cg | Idris.IBC |
ibc_cgflags | Idris.IBC |
ibc_classes | Idris.IBC |
ibc_coercions | Idris.IBC |
ibc_datatypes | Idris.IBC |
ibc_defs | Idris.IBC |
ibc_docstrings | Idris.IBC |
ibc_dsls | Idris.IBC |
ibc_dynamic_libs | Idris.IBC |
ibc_errorhandlers | Idris.IBC |
ibc_errRev | Idris.IBC |
ibc_fixes | Idris.IBC |
ibc_flags | Idris.IBC |
ibc_function_errorhandlers | Idris.IBC |
ibc_hdrs | Idris.IBC |
ibc_implicits | Idris.IBC |
ibc_imports | Idris.IBC |
ibc_instances | Idris.IBC |
ibc_keywords | Idris.IBC |
ibc_libs | Idris.IBC |
ibc_lineapps | Idris.IBC |
ibc_metainformation | Idris.IBC |
ibc_namehints | Idris.IBC |
ibc_objs | Idris.IBC |
ibc_optimise | Idris.IBC |
ibc_statics | Idris.IBC |
ibc_syntax | Idris.IBC |
ibc_total | Idris.IBC |
ibc_transforms | Idris.IBC |
ibc_write | Idris.AbsSyntaxTree, Idris.AbsSyntax |
identifier | Idris.ParseHelpers, Idris.Parser |
IdeSlave | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Ideslave | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ideslave | Idris.REPL |
IdeSlaveCommand | Idris.IdeSlave |
ideslaveProcess | Idris.REPL |
ideslavePutSExp | Idris.AbsSyntax |
ideSlaveReturnAnnotated | Idris.AbsSyntax |
ideslaveStart | Idris.REPL |
idiom | Idris.ParseExpr, Idris.Parser |
IDR | Idris.Imports |
Idris | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris | Idris.REPL |
idrisCatch | Idris.Error |
idrisClosureType | IRTS.Java.JTypes |
IdrisColour | |
1 (Type/Class) | Idris.Colours |
2 (Data Constructor) | Idris.Colours |
idrisInit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IdrisInnerParser | |
1 (Type/Class) | Idris.ParseHelpers, Idris.Parser |
2 (Data Constructor) | Idris.ParseHelpers, Idris.Parser |
idrisMain | Idris.REPL |
idrisObjectType | IRTS.Java.JTypes |
IdrisParser | Idris.ParseHelpers, Idris.Parser |
idrisStyle | Idris.ParseHelpers, Idris.Parser |
idrisTailCallClosureType | IRTS.Java.JTypes |
idris_calledgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_callgraph | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_cgflags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_classes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_coercions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_colourRepl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_colourTheme | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_consolewidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_constraints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_datatypes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_defertotcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_docstrings | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_dsls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_dynamic_libs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_errRev | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_flags | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_function_errorhandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_hdrs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_implicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_infixes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_language_extensions | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_libs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_lineapps | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_name | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_namehints | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_nameIdx | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_objs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_optimisation | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_options | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_outh | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_outputmode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_patdefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_scprims | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_statics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_totcheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
idris_transforms | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ierror | Idris.Error |
ifail | Idris.Error |
IFileType | Idris.Imports |
ihPrintError | Idris.AbsSyntax |
ihPrintFunTypes | Idris.AbsSyntax |
ihPrintResult | Idris.AbsSyntax |
ihPrintTermWithType | Idris.AbsSyntax |
ihputStrLn | Idris.AbsSyntax |
ihRenderResult | Idris.AbsSyntax |
ihWarn | Idris.AbsSyntax |
iLOG | Idris.AbsSyntax |
Imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
impl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Implicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
implicit | Idris.AbsSyntax |
implicit' | Idris.AbsSyntax |
implicitable | Idris.Core.TT |
implicitAllowed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
implicitArg | Idris.ParseExpr, Idris.Parser |
ImplicitColour | Idris.Colours |
implicitColour | Idris.Colours |
ImplicitD | Idris.PartialEval |
implicitise | Idris.AbsSyntax |
ImplicitS | Idris.PartialEval |
ImportDir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
imported | Idris.AbsSyntaxTree, Idris.AbsSyntax |
import_ | Idris.Parser |
Impossible | Idris.Core.TT |
ImpossibleCase | Idris.Core.CaseTree |
impShow | Idris.AbsSyntax |
Inaccessible | Idris.Core.TT |
iName | Idris.ParseHelpers, Idris.Parser |
inblock | Idris.ElabTerm |
IncompleteTerm | Idris.Core.TT |
indent | |
1 (Function) | IRTS.DumpBC |
2 (Function) | Idris.ParseHelpers, Idris.Parser |
indented | Idris.ParseHelpers, Idris.Parser |
indentedBlock | Idris.ParseHelpers, Idris.Parser |
indentedBlock1 | Idris.ParseHelpers, Idris.Parser |
indentedBlockS | Idris.ParseHelpers, Idris.Parser |
IndentProperty | |
1 (Type/Class) | Idris.ParseHelpers, Idris.Parser |
2 (Data Constructor) | Idris.ParseHelpers, Idris.Parser |
indentPropHolds | Idris.ParseHelpers, Idris.Parser |
indent_stack | Idris.AbsSyntaxTree, Idris.AbsSyntax |
index_first | Idris.AbsSyntaxTree, Idris.AbsSyntax |
index_next | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Induction | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
induction | Idris.Core.Elaborate |
inferCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
inferDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
inferOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
inferredDiff | Idris.ElabDecls |
inferTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
InfinitelyWide | Idris.AbsSyntaxTree, Idris.AbsSyntax |
InfiniteUnify | Idris.Core.TT |
Infixl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
InfixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Infixr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Info | Idris.AbsSyntaxTree, Idris.AbsSyntax |
infP | Idris.AbsSyntaxTree, Idris.AbsSyntax |
infTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
initContext | Idris.Core.Evaluate |
initDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
initElaborator | Idris.Core.Elaborate |
initEval | Idris.Core.Evaluate |
initIBC | Idris.IBC |
initNextNameFrom | Idris.Core.Elaborate |
initScript | Idris.REPL |
initsEndAt | Idris.ParseHelpers, Idris.Parser |
injective | Idris.Core.ProofState, Idris.Core.Elaborate |
inl | IRTS.Inliner |
Inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
inlinable | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Inline | IRTS.Lang, IRTS.Defunctionalise |
inline | IRTS.Inliner |
inlineDef | Idris.Inliner |
inlineTerm | Idris.Inliner |
inPattern | Idris.AbsSyntaxTree, Idris.AbsSyntax |
insertScript | Idris.REPL |
installIBC | Pkg.Package |
installObj | Pkg.Package |
installPkg | Pkg.Package |
Instance | Idris.Core.ProofState, Idris.Core.Elaborate |
instanceArg | Idris.Core.Elaborate |
instanceBlock | Idris.Parser |
InstanceN | Idris.Core.TT |
instanceName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
instances | Idris.Core.ProofState, Idris.Core.Elaborate |
instance_ | Idris.Parser |
instantiate | Idris.Core.TT |
integer | Idris.ParseHelpers, Idris.Parser |
IntegerAtom | Idris.IdeSlave |
integerType | IRTS.Java.JTypes |
interMap | IRTS.DumpBC |
internalExpr | Idris.ParseExpr, Idris.Parser |
InternalMsg | Idris.Core.TT |
Interpret | Idris.IdeSlave |
InterpretScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Intro | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
intro | Idris.Core.Elaborate |
Intros | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IntroTy | Idris.Core.ProofState, Idris.Core.Elaborate |
introTy | Idris.Core.Elaborate |
IntTy | Idris.Core.TT |
intTyName | Idris.Core.TT |
intTyToJType | IRTS.Java.JTypes |
intTyWidth | Idris.Core.TT |
InvocationTarget | IRTS.Java.ASTBuilding |
IOption | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
iPrintError | Idris.AbsSyntax |
iPrintResult | Idris.AbsSyntax |
iputGoal | Idris.AbsSyntax |
iputStrLn | Idris.AbsSyntax |
ir | IRTS.Compiler |
iRender | Idris.AbsSyntax |
irMain | IRTS.Compiler |
isArray | IRTS.Java.JTypes |
isCon | IRTS.Compiler |
isConName | Idris.Core.Evaluate |
isConst | IRTS.Bytecode |
isDConName | Idris.Core.Evaluate |
isDocCommentMarker | Idris.ParseHelpers, Idris.Parser |
isEol | Idris.ParseHelpers, Idris.Parser |
isetPrompt | Idris.AbsSyntax |
isFloating | IRTS.Java.JTypes |
isFnName | Idris.Core.Evaluate |
isInjective | Idris.Core.TT |
isnewtype | Idris.AbsSyntaxTree, Idris.AbsSyntax |
isPrimitive | IRTS.Java.JTypes |
isString | IRTS.Java.JTypes |
IState | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
isTConName | Idris.Core.Evaluate |
IsTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
IsType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
isType | Idris.Core.Typecheck |
isUndefined | Idris.AbsSyntax |
IT16 | Idris.Core.TT |
IT32 | Idris.Core.TT |
IT64 | Idris.Core.TT |
IT8 | Idris.Core.TT |
italic | Idris.Colours |
ITBig | Idris.Core.TT |
itBitsName | Idris.Core.TT |
ITChar | Idris.Core.TT |
ITFixed | Idris.Core.TT |
ITNative | Idris.Core.TT |
Itself | Idris.Core.Evaluate |
ITVec | Idris.Core.TT |
iucheck | Idris.Error |
iWarn | Idris.AbsSyntax |
JavaScript | IRTS.CodegenJavaScript |
jConst | IRTS.Java.ASTBuilding |
jInt | IRTS.Java.ASTBuilding |
jName | IRTS.Java.ASTBuilding |
jReturn | IRTS.Java.ASTBuilding |
JSTarget | IRTS.CodegenJavaScript |
jString | IRTS.Java.ASTBuilding |
keepGiven | Idris.Core.ProofState, Idris.Core.Elaborate |
keepTerminator | Idris.ParseHelpers, Idris.Parser |
Keyword | Idris.AbsSyntaxTree, Idris.AbsSyntax |
KeywordColour | Idris.Colours |
keywordColour | Idris.Colours |
L | |
1 (Data Constructor) | IRTS.BCImp |
2 (Data Constructor) | IRTS.Bytecode |
LAllocate | IRTS.Lang, IRTS.Defunctionalise |
LAlt | IRTS.Lang, IRTS.Defunctionalise |
Lam | Idris.Core.TT |
lambda | Idris.ParseExpr, Idris.Parser |
lambdaLift | IRTS.Lang, IRTS.Defunctionalise |
LAnd | IRTS.Lang, IRTS.Defunctionalise |
LanguageExt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
LANG_C | IRTS.Lang, IRTS.Defunctionalise |
LANG_JAVA | IRTS.Lang, IRTS.Defunctionalise |
LApp | IRTS.Lang, IRTS.Defunctionalise |
LAppend | IRTS.Lang, IRTS.Defunctionalise |
LAppendBuffer | IRTS.Lang, IRTS.Defunctionalise |
LASHR | IRTS.Lang, IRTS.Defunctionalise |
lastIndent | Idris.ParseHelpers, Idris.Parser |
lastParse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Lazy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
lazyarg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
LBitCast | IRTS.Lang, IRTS.Defunctionalise |
LCase | IRTS.Lang, IRTS.Defunctionalise |
lchar | Idris.ParseHelpers, Idris.Parser |
LChInt | IRTS.Lang, IRTS.Defunctionalise |
LCompl | IRTS.Lang, IRTS.Defunctionalise |
LCon | IRTS.Lang, IRTS.Defunctionalise |
LConCase | IRTS.Lang, IRTS.Defunctionalise |
LConst | IRTS.Lang, IRTS.Defunctionalise |
LConstCase | IRTS.Lang, IRTS.Defunctionalise |
LConstructor | IRTS.Lang, IRTS.Defunctionalise |
LDecl | IRTS.Lang, IRTS.Defunctionalise |
LDefaultCase | IRTS.Lang, IRTS.Defunctionalise |
LDefs | IRTS.Lang, IRTS.Defunctionalise |
ldefs | IRTS.Simplified |
LE | IRTS.Lang, IRTS.Defunctionalise |
LeftErr | Idris.AbsSyntax |
LEq | IRTS.Lang, IRTS.Defunctionalise |
LError | IRTS.Lang, IRTS.Defunctionalise |
Let | Idris.Core.TT |
LetBind | Idris.Core.ProofState, Idris.Core.Elaborate |
letbind | Idris.Core.Elaborate |
LetTac | Idris.AbsSyntaxTree, Idris.AbsSyntax |
LetTacTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
let_ | Idris.ParseExpr, Idris.Parser |
LExp | IRTS.Lang, IRTS.Defunctionalise |
LFACos | IRTS.Lang, IRTS.Defunctionalise |
LFASin | IRTS.Lang, IRTS.Defunctionalise |
LFATan | IRTS.Lang, IRTS.Defunctionalise |
LFCeil | IRTS.Lang, IRTS.Defunctionalise |
LFCos | IRTS.Lang, IRTS.Defunctionalise |
LFExp | IRTS.Lang, IRTS.Defunctionalise |
LFFloor | IRTS.Lang, IRTS.Defunctionalise |
LFloatInt | IRTS.Lang, IRTS.Defunctionalise |
LFloatStr | IRTS.Lang, IRTS.Defunctionalise |
LFLog | IRTS.Lang, IRTS.Defunctionalise |
LForce | IRTS.Lang, IRTS.Defunctionalise |
LForeign | IRTS.Lang, IRTS.Defunctionalise |
LFork | IRTS.Lang, IRTS.Defunctionalise |
LFSin | IRTS.Lang, IRTS.Defunctionalise |
LFSqrt | IRTS.Lang, IRTS.Defunctionalise |
LFTan | IRTS.Lang, IRTS.Defunctionalise |
LFun | IRTS.Lang, IRTS.Defunctionalise |
LGe | IRTS.Lang, IRTS.Defunctionalise |
LGt | IRTS.Lang, IRTS.Defunctionalise |
Lib | Util.DynamicLinker |
lib_handle | Util.DynamicLinker |
lib_name | Util.DynamicLinker |
LIDR | Idris.Imports |
LIdxVec | IRTS.Lang, IRTS.Defunctionalise |
lift | IRTS.Lang, IRTS.Defunctionalise |
liftAll | IRTS.Lang, IRTS.Defunctionalise |
lifte | Idris.Prover |
liftname | Idris.ElabTerm |
liftParsed | IRTS.Java.Mangling |
LiftState | IRTS.Lang, IRTS.Defunctionalise |
lineNum | Idris.ParseHelpers, Idris.Parser |
LIntCh | IRTS.Lang, IRTS.Defunctionalise |
LIntFloat | IRTS.Lang, IRTS.Defunctionalise |
LIntStr | IRTS.Lang, IRTS.Defunctionalise |
ListDynamic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ListErrorHandlers | Idris.AbsSyntaxTree, Idris.AbsSyntax |
listExpr | Idris.ParseExpr, Idris.Parser |
lit | Idris.REPL |
LLam | IRTS.Lang, IRTS.Defunctionalise |
LLazyApp | IRTS.Lang, IRTS.Defunctionalise |
LLazyExp | IRTS.Lang, IRTS.Defunctionalise |
LLe | IRTS.Lang, IRTS.Defunctionalise |
LLet | IRTS.Lang, IRTS.Defunctionalise |
LLSHR | IRTS.Lang, IRTS.Defunctionalise |
LLt | IRTS.Lang, IRTS.Defunctionalise |
LMinus | IRTS.Lang, IRTS.Defunctionalise |
LMkVec | IRTS.Lang, IRTS.Defunctionalise |
lname | IRTS.Lang, IRTS.Defunctionalise |
LNoOp | IRTS.Lang, IRTS.Defunctionalise |
LNothing | IRTS.Lang, IRTS.Defunctionalise |
LNullPtr | IRTS.Lang, IRTS.Defunctionalise |
Load | Idris.AbsSyntaxTree, Idris.AbsSyntax |
LoadFile | Idris.IdeSlave |
loadFromIFile | Idris.Parser |
loadIBC | Idris.IBC |
LoadingFailed | Idris.Core.TT |
loadInputs | Idris.REPL |
loadModule | Idris.Parser |
loadModule' | Idris.Parser |
loadSource | Idris.Parser |
loadSource' | Idris.Parser |
loadState | Idris.Core.Elaborate |
Loc | IRTS.Lang, IRTS.Defunctionalise |
localContext | IRTS.Java.JTypes |
localContextID | IRTS.Java.JTypes |
localVar | IRTS.Java.ASTBuilding |
logLevel | Idris.AbsSyntax |
LogLvl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
logLvl | Idris.AbsSyntax |
longType | IRTS.Java.JTypes |
lookAheadMatches | Idris.ParseHelpers, Idris.Parser |
lookupCtxt | Idris.Core.TT |
lookupCtxtExact | Idris.Core.TT |
lookupCtxtName | Idris.Core.TT |
lookupDef | Idris.Core.Evaluate |
lookupDefAcc | Idris.Core.Evaluate |
lookupMetaInformation | Idris.Core.Evaluate |
lookupNames | Idris.Core.Evaluate |
lookupNameTotal | Idris.Core.Evaluate |
lookupP | Idris.Core.Evaluate |
lookupTotal | Idris.Core.Evaluate |
lookupTy | Idris.Core.Evaluate |
lookupTyEnv | Idris.Core.Evaluate |
lookupVal | Idris.Core.Evaluate |
LOp | IRTS.Lang, IRTS.Defunctionalise |
LOpt | IRTS.Lang, IRTS.Defunctionalise |
LOr | IRTS.Lang, IRTS.Defunctionalise |
LPar | IRTS.Lang, IRTS.Defunctionalise |
LPeek | IRTS.Lang, IRTS.Defunctionalise |
LPlus | IRTS.Lang, IRTS.Defunctionalise |
LPrintNum | IRTS.Lang, IRTS.Defunctionalise |
LPrintStr | IRTS.Lang, IRTS.Defunctionalise |
LProj | IRTS.Lang, IRTS.Defunctionalise |
LReadStr | IRTS.Lang, IRTS.Defunctionalise |
LS | IRTS.Lang, IRTS.Defunctionalise |
LSDiv | IRTS.Lang, IRTS.Defunctionalise |
LSExt | IRTS.Lang, IRTS.Defunctionalise |
LSGe | IRTS.Lang, IRTS.Defunctionalise |
LSGt | IRTS.Lang, IRTS.Defunctionalise |
LSHL | IRTS.Lang, IRTS.Defunctionalise |
LSLe | IRTS.Lang, IRTS.Defunctionalise |
LSLt | IRTS.Lang, IRTS.Defunctionalise |
lsrcPath | Idris.Imports |
LSRem | IRTS.Lang, IRTS.Defunctionalise |
LStdErr | IRTS.Lang, IRTS.Defunctionalise |
LStdIn | IRTS.Lang, IRTS.Defunctionalise |
LStdOut | IRTS.Lang, IRTS.Defunctionalise |
LStrConcat | IRTS.Lang, IRTS.Defunctionalise |
LStrCons | IRTS.Lang, IRTS.Defunctionalise |
LStrEq | IRTS.Lang, IRTS.Defunctionalise |
LStrFloat | IRTS.Lang, IRTS.Defunctionalise |
LStrHead | IRTS.Lang, IRTS.Defunctionalise |
LStrIndex | IRTS.Lang, IRTS.Defunctionalise |
LStrInt | IRTS.Lang, IRTS.Defunctionalise |
LStrLen | IRTS.Lang, IRTS.Defunctionalise |
LStrLt | IRTS.Lang, IRTS.Defunctionalise |
LStrRev | IRTS.Lang, IRTS.Defunctionalise |
LStrTail | IRTS.Lang, IRTS.Defunctionalise |
lteProp | Idris.ParseHelpers, Idris.Parser |
LTimes | IRTS.Lang, IRTS.Defunctionalise |
ltProp | Idris.ParseHelpers, Idris.Parser |
LTrunc | IRTS.Lang, IRTS.Defunctionalise |
LUDiv | IRTS.Lang, IRTS.Defunctionalise |
LUpdateVec | IRTS.Lang, IRTS.Defunctionalise |
LURem | IRTS.Lang, IRTS.Defunctionalise |
LV | IRTS.Lang, IRTS.Defunctionalise |
LVar | IRTS.Lang, IRTS.Defunctionalise |
lvar | IRTS.Simplified |
LVMPtr | IRTS.Lang, IRTS.Defunctionalise |
LXOr | IRTS.Lang, IRTS.Defunctionalise |
LZExt | IRTS.Lang, IRTS.Defunctionalise |
machine_inf | Idris.AbsSyntaxTree, Idris.AbsSyntax |
make | Pkg.Package |
MakeWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
MakeWithBlock | Idris.IdeSlave |
mangle | IRTS.Java.Mangling |
mangle' | IRTS.Java.Mangling |
mangleFull | IRTS.Java.Mangling |
mangleWithPrefix | IRTS.Java.Mangling |
mapCtxt | Idris.Core.TT |
mapDefCtxt | Idris.Core.Evaluate |
mapPT | Idris.AbsSyntaxTree, Idris.AbsSyntax |
mapsnd | Idris.AbsSyntax |
MArgTy | Idris.ElabDecls |
matchApp | Idris.ParseExpr, Idris.Parser |
matchClause | Idris.AbsSyntax |
matchClause' | Idris.AbsSyntax |
MatchFill | Idris.Core.ProofState, Idris.Core.Elaborate |
MatchProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
matchProblems | Idris.Core.Elaborate |
MatchRefine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
match_apply | Idris.Core.Elaborate |
match_fill | Idris.Core.Elaborate |
match_unify | Idris.Core.Unify |
mathType | IRTS.Java.JTypes |
MavenProject | IRTS.CodegenCommon |
maybeWithNS | Idris.ParseHelpers, Idris.Parser |
MetaInformation | Idris.Core.Evaluate |
MetaVarArg | Idris.Help |
Metavars | Idris.AbsSyntaxTree, Idris.AbsSyntax |
MethodN | Idris.Core.TT |
Missing | Idris.AbsSyntaxTree, Idris.AbsSyntax |
mkApp | Idris.Core.TT |
mkapp | IRTS.Simplified |
mkApply | IRTS.Defunctionalise |
mkApplyCase | IRTS.Defunctionalise |
mkBigCase | IRTS.Defunctionalise |
mkClassName | IRTS.Java.Mangling |
MKCON | IRTS.Bytecode |
mkDecls | IRTS.Compiler |
mkDirCmd | Pkg.Package |
mkEval | IRTS.Defunctionalise |
mkfapp | IRTS.Simplified |
mkFnCon | IRTS.Defunctionalise |
mkIBC | Idris.IBC |
mkIntIty | IRTS.Compiler |
mkIty | IRTS.Compiler |
mkIty' | IRTS.Compiler |
mkLDecl | IRTS.Compiler |
mkMultiPaths | Idris.Coverage |
mkName | Idris.ParseHelpers, Idris.Parser |
mkPApp | Idris.AbsSyntax |
mkPatTm | Idris.Coverage |
mkPE_TermDecl | Idris.PartialEval |
mkPE_TyDecl | Idris.PartialEval |
mkPrompt | Idris.REPL |
mkType | Idris.ParseExpr, Idris.Parser |
mkUnderCon | IRTS.Defunctionalise |
mkUniqueNames | Idris.AbsSyntax |
mkWith | Idris.CaseSplit |
MN | Idris.Core.TT |
modifyConst | Idris.ParseExpr, Idris.Parser |
ModImport | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ModuleArg | Idris.Help |
moduleHeader | Idris.Parser |
ModuleTree | Idris.Chaser |
module_aliases | Idris.AbsSyntaxTree, Idris.AbsSyntax |
mod_deps | Idris.Chaser |
mod_needsRecheck | Idris.Chaser |
mod_path | Idris.Chaser |
mod_time | Idris.Chaser |
MonadicParsing | Idris.ParseHelpers, Idris.Parser |
MoveLast | Idris.Core.ProofState, Idris.Core.Elaborate |
movelast | Idris.Core.Elaborate |
moveReg | IRTS.Bytecode |
Msg | Idris.Core.TT |
MTree | Idris.Chaser |
multiLineComment | Idris.ParseHelpers, Idris.Parser |
MultiPath | Idris.Coverage |
Mutual | Idris.Core.Evaluate |
mutual | Idris.Parser |
Name | Idris.Core.TT |
name | Idris.ParseHelpers, Idris.Parser |
NameArg | Idris.Help |
nameMissing | Idris.CaseSplit |
NameOutput | Idris.Core.TT |
NamePart | Idris.Core.TT |
nameRoot | Idris.CaseSplit |
namesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
namespace | |
1 (Function) | Idris.ElabTerm |
2 (Function) | Idris.Parser |
namesUsed | Idris.Core.CaseTree |
NameType | Idris.Core.TT |
natcase | Idris.Transforms |
Native | IRTS.Lang, IRTS.Defunctionalise |
NativeTy | Idris.Core.TT |
nativeTyToJType | IRTS.Java.JTypes |
nativeTyWidth | Idris.Core.TT |
natTrans | Idris.Transforms |
natural | Idris.ParseHelpers, Idris.Parser |
NErased | Idris.Core.TT |
newContext | IRTS.Java.JTypes |
newContextID | IRTS.Java.JTypes |
newProof | Idris.Core.ProofState, Idris.Core.Elaborate |
nextName | Idris.Core.TT |
nextname | Idris.Core.ProofState, Idris.Core.Elaborate |
next_tvar | Idris.Core.Evaluate |
NLet | Idris.Core.TT |
NoArg | Idris.Help |
NoBanner | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NoBasePkgs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NoBuiltins | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NoCoverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Node | IRTS.CodegenJavaScript |
noErrors | Idris.AbsSyntax |
noImplicits | Idris.ParseExpr, Idris.Parser |
NoInline | IRTS.Lang, IRTS.Defunctionalise |
NonCollapsiblePostulate | Idris.Core.TT |
NONE | IRTS.CodegenCommon |
NonFunctionType | Idris.Core.TT |
noOccurrence | Idris.Core.TT |
NOP | |
1 (Data Constructor) | IRTS.BCImp |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
noPartial | Idris.Coverage |
NoPrelude | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NoREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NoRewriting | Idris.Core.TT |
normalise | Idris.Core.Evaluate |
normaliseAll | Idris.Core.Evaluate |
normaliseC | Idris.Core.Evaluate |
normaliseTrace | Idris.Core.Evaluate |
NoSuchVariable | Idris.Core.TT |
NotCovering | Idris.Core.Evaluate |
notEndApp | Idris.ParseHelpers, Idris.Parser |
notEndBlock | Idris.ParseHelpers, Idris.Parser |
NotEquality | Idris.Core.TT |
NotInjective | Idris.Core.TT |
notOpenBraces | Idris.ParseHelpers, Idris.Parser |
NotPositive | Idris.Core.Evaluate |
NotProductive | Idris.Core.Evaluate |
notunified | Idris.Core.ProofState, Idris.Core.Elaborate |
NoTypeDecl | Idris.Core.TT |
no_errors | Idris.Core.Elaborate |
no_imp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
NS | Idris.Core.TT |
nsroot | Idris.Core.TT |
nt_arity | Idris.Core.TT |
nt_tag | Idris.Core.TT |
NULL | IRTS.Bytecode |
Object | IRTS.CodegenCommon |
objectType | IRTS.Java.JTypes |
OK | Idris.Core.TC, Idris.Core.TT |
OLogging | Idris.AbsSyntaxTree, Idris.AbsSyntax |
OP | IRTS.Bytecode |
opChars | Idris.ParseHelpers, Idris.Parser |
openBlock | Idris.ParseHelpers, Idris.Parser |
Operator | Idris.Core.Evaluate |
operator | Idris.ParseHelpers, Idris.Parser |
operatorFront | Idris.ParseOps, Idris.Parser |
operatorLetter | Idris.ParseHelpers, Idris.Parser |
opName | IRTS.Java.JTypes |
Opt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt | Idris.REPL |
Optimisable | Idris.DataOpts |
Optimise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
OptInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Option | Idris.Core.TT |
OptionArg | Idris.Help |
OptLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
optLevel | Idris.AbsSyntax |
opt_cmdline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_codegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_coverage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_cpu | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_errContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_ibcsubdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_importdirs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_logLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_nobanner | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_optLevel | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_origerr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_outputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_repl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_showimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_triple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_typecase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_typeintype | Idris.AbsSyntaxTree, Idris.AbsSyntax |
opt_verbose | Idris.AbsSyntaxTree, Idris.AbsSyntax |
orderPats | Idris.Core.TT |
Other | Idris.Core.Evaluate |
Output | Idris.AbsSyntaxTree, Idris.AbsSyntax |
OutputAnnotation | Idris.Core.TT |
OutputMode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
OutputTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
outputTy | Idris.AbsSyntax |
OutputType | IRTS.CodegenCommon |
overload | Idris.ParseData, Idris.Parser |
P | Idris.Core.TT |
pAccess | Idris.IBC |
pairCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pairDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pairOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pairTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PAlternative | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PAppBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
params | |
1 (Function) | Idris.ElabTerm |
2 (Function) | Idris.Parser |
param_pos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ParentN | Idris.Core.TT |
PArg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PArg' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pargdoc | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pargopts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
parseArgs | Idris.REPL |
parseCmd | Idris.REPLParser |
parseCodegen | Idris.REPL |
parseExpr | Idris.Parser |
parseImports | Idris.Parser |
parseMessage | Idris.IdeSlave |
parseProg | Idris.Parser |
parseTactic | Idris.Parser |
Partial | Idris.Core.Evaluate |
PartialFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
partial_eval | Idris.PartialEval |
PatBind | Idris.Core.ProofState, Idris.Core.Elaborate |
patbind | Idris.Core.Elaborate |
Pattelab | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pattern | Idris.Parser |
PatternSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PatVar | Idris.Core.ProofState, Idris.Core.Elaborate |
patvar | Idris.Core.Elaborate |
pbinds | Idris.ElabDecls |
pbty | Idris.ElabDecls |
PCAF | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pCG | Idris.IBC |
pCGFlags | Idris.IBC |
PClass | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pClasses | Idris.IBC |
PClause | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PClause' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PClauseR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PClauses | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PCoerced | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pCoercions | Idris.IBC |
pconst | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PConstant | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PConstraint | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PData | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PData' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDatadecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pDatatypes | Idris.IBC |
PDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDecl' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pDefs | Idris.IBC |
PDirective | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDisamb | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDo' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDoBlock | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pDocs | Idris.IBC |
pdocstr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PDSL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pDSLs | Idris.IBC |
pDyLibs | Idris.IBC |
PEArgType | Idris.PartialEval |
PElabError | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PEq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pEraseType | Idris.Core.TT |
pErrorHandlers | Idris.IBC |
pErrRev | Idris.IBC |
PExp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pexp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PFalse | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PFix | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pFixes | Idris.IBC |
pFlags | Idris.IBC |
pFunctionErrorHandlers | Idris.IBC |
PGoal | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Phase | Idris.Core.CaseTree |
pHdrs | Idris.IBC |
PHidden | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Pi | Idris.Core.TT |
pi | Idris.ParseExpr, Idris.Parser |
piBind | Idris.AbsSyntaxTree, Idris.AbsSyntax |
piBindp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PIdiom | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pImports | Idris.IBC |
PImpossible | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pImps | Idris.IBC |
PInferRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pInstances | Idris.IBC |
pKeywords | Idris.IBC |
Pkg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PkgBuild | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PkgCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PkgClean | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PkgInstall | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PkgREPL | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Placeholder | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PLam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pLangExt | Idris.Parser |
PLaterdecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
plazy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PLet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pLibs | Idris.IBC |
Plicity | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pLineApps | Idris.IBC |
plog | Idris.Core.ProofState, Idris.Core.Elaborate |
ploop | Idris.Prover |
pmap | Idris.Core.TT |
PMatchApp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pMetaInformation | Idris.IBC |
PMetavar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PMutual | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pname | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pNameHints | Idris.IBC |
PNamespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PNoImplicits | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pObjs | Idris.IBC |
pomString | IRTS.Java.Pom |
popIndent | Idris.ParseHelpers, Idris.Parser |
pOptimise | Idris.IBC |
postulate | Idris.Parser |
PPair | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pparam | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PParams | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PPatvar | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PPi | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PPostulate | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pprintErr | Idris.Delaborate |
pprintPTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PProvider | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PQuote | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PReason | Idris.Core.Evaluate |
prec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PRecord | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PRef | Idris.AbsSyntaxTree, Idris.AbsSyntax |
prefix | Idris.ParseOps, Idris.Parser |
prefixCallNamespaces | IRTS.Java.Mangling |
PrefixN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PRefl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
prel | Idris.DataOpts |
premises | Idris.Core.ProofState, Idris.Core.Elaborate |
prepare_apply | Idris.Core.Elaborate |
PrepFill | Idris.Core.ProofState, Idris.Core.Elaborate |
prep_fill | Idris.Core.Elaborate |
PResolveTC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
prettyEnv | Idris.Core.TT |
prettyImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
prettyName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PReturn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
previous | Idris.Core.ProofState, Idris.Core.Elaborate |
PRewrite | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Prim | |
1 (Type/Class) | Idris.Primitives |
2 (Data Constructor) | Idris.Primitives |
primDefs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PrimFn | IRTS.Lang, IRTS.Defunctionalise |
primFnType | IRTS.Java.JTypes |
primitives | Idris.Primitives |
primNames | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Print | Idris.Core.Elaborate |
priority | Idris.AbsSyntaxTree, Idris.AbsSyntax |
problems | Idris.Core.ProofState, Idris.Core.Elaborate |
process | |
1 (Function) | Idris.IBC |
2 (Function) | Idris.REPL |
processInput | Idris.REPL |
processNetCmd | Idris.REPL |
processTactic | Idris.Core.ProofState, Idris.Core.Elaborate |
processTactic' | Idris.Core.Elaborate |
Productive | Idris.Core.Evaluate |
prog | Idris.Parser |
ProgramLineComment | Idris.Core.TT |
Proj | Idris.Core.TT |
ProjCase | Idris.Core.CaseTree |
PROJECT | IRTS.Bytecode |
PROJECTINTO | IRTS.Bytecode |
PromptColour | Idris.Colours |
promptColour | Idris.Colours |
proof | Idris.Core.Elaborate |
proofExpr | Idris.ParseExpr, Idris.Parser |
proofFail | Idris.Core.Elaborate |
Proofs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
proofs | Idris.REPL |
ProofSearch | |
1 (Data Constructor) | Idris.IdeSlave |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
proofSearch | Idris.ProofSearch |
proofSearch' | Idris.ElabTerm |
ProofSearchFail | Idris.Core.TT |
ProofState | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Type/Class) | Idris.Core.ProofState, Idris.Core.Elaborate |
3 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
proofstate | Idris.Core.Elaborate |
ProofTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
proof_list | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Prove | Idris.AbsSyntaxTree, Idris.AbsSyntax |
prove | Idris.Prover |
prover | Idris.Prover |
proverCompletion | Idris.Completion |
proverSettings | Idris.Prover |
provider | Idris.Parser |
ProviderError | Idris.Core.TT |
providerTy | Idris.Providers |
pruneAlt | Idris.ElabTerm |
pruneByType | Idris.ElabTerm |
prunStateT | Idris.Core.Elaborate |
PS | Idris.Core.ProofState, Idris.Core.Elaborate |
pscript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pshow | Idris.Delaborate |
psolve | Idris.ElabDecls |
pstatic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pStatics | Idris.IBC |
psubst | Idris.Core.TT |
PSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pSyntax | Idris.IBC |
ptacimp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTacImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTactic | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTactic' | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTactics | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pterm | Idris.Core.ProofState, Idris.Core.Elaborate |
pTotal | Idris.IBC |
pToV | Idris.Core.TT |
pToV' | Idris.Core.TT |
pToVs | Idris.Core.TT |
pTrans | Idris.IBC |
PTransform | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PtrType | Idris.Core.TT |
PTrue | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ptype | Idris.Core.ProofState, Idris.Core.Elaborate |
PTyped | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Public | Idris.Core.Evaluate |
PUnifyLog | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PunInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
pureTerm | Idris.Core.TT |
pushIndent | Idris.ParseHelpers, Idris.Parser |
putIState | Idris.AbsSyntax |
PVar | Idris.Core.TT |
pvars | Idris.ElabDecls |
PVTy | Idris.Core.TT |
PWith | Idris.AbsSyntaxTree, Idris.AbsSyntax |
PWithR | Idris.AbsSyntaxTree, Idris.AbsSyntax |
p_arity | Idris.Primitives |
p_def | Idris.Primitives |
p_lexp | Idris.Primitives |
p_name | Idris.Primitives |
p_total | Idris.Primitives |
p_type | Idris.Primitives |
QED | Idris.Core.ProofState, Idris.Core.Elaborate |
Qed | Idris.AbsSyntaxTree, Idris.AbsSyntax |
qed | Idris.Core.Elaborate |
qelem | Idris.Coverage |
qshow | Idris.Core.Elaborate |
quickEq | Idris.Coverage |
Quiet | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Quit | |
1 (Data Constructor) | Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Quote | Idris.Core.Evaluate |
quote | Idris.Core.Evaluate |
quoteGoal | Idris.ParseExpr, Idris.Parser |
RApp | Idris.Core.TT |
Raw | |
1 (Type/Class) | Idris.Core.TT |
2 (Data Constructor) | IRTS.CodegenCommon |
rawBool | Idris.ElabTerm |
rawCons | Idris.ElabTerm |
rawList | Idris.ElabTerm |
rawNil | Idris.ElabTerm |
RawOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
rawPair | Idris.ElabTerm |
rawPairTy | Idris.ElabTerm |
raw_apply | Idris.Core.TT |
raw_unapply | Idris.Core.TT |
RBind | Idris.Core.TT |
RConstant | Idris.Core.TT |
REBASE | IRTS.Bytecode |
receiveInput | Idris.Prover |
recheck | Idris.Core.Typecheck |
recheckC | Idris.ElabDecls |
record | Idris.ParseData, Idris.Parser |
recordType | Idris.ParseExpr, Idris.Parser |
recursive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Ref | Idris.Core.TT |
Refine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reflCall | Idris.ElabTerm |
Reflect | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reflect | Idris.ElabTerm |
reflectBinder | Idris.ElabTerm |
reflectConstant | Idris.ElabTerm |
reflectCtxt | Idris.ElabTerm |
reflectEnv | Idris.ElabTerm |
reflectErr | Idris.ElabTerm |
reflectFunctionErrors | Idris.ElabTerm |
Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ReflectionError | Idris.Core.TT |
ReflectionFailed | Idris.Core.TT |
reflectName | Idris.ElabTerm |
reflectNameType | Idris.ElabTerm |
reflectUExp | Idris.ElabTerm |
reflErrName | Idris.ElabTerm |
reflm | Idris.ElabTerm |
Reg | |
1 (Type/Class) | IRTS.BCImp |
2 (Type/Class) | IRTS.Bytecode |
Regret | Idris.Core.ProofState, Idris.Core.Elaborate |
regret | Idris.Core.Elaborate |
reify | Idris.ElabTerm |
reifyApp | Idris.ElabTerm |
reifyRaw | Idris.ElabTerm |
reifyRawApp | Idris.ElabTerm |
reifyReportPart | Idris.ElabTerm |
reifyTT | Idris.ElabTerm |
reifyTTApp | Idris.ElabTerm |
reifyTTBinder | Idris.ElabTerm |
reifyTTBinderApp | Idris.ElabTerm |
reifyTTConst | Idris.ElabTerm |
reifyTTConstApp | Idris.ElabTerm |
reifyTTName | Idris.ElabTerm |
reifyTTNameApp | Idris.ElabTerm |
reifyTTNamespace | Idris.ElabTerm |
reifyTTNameType | Idris.ElabTerm |
reifyTTUExp | Idris.ElabTerm |
Reload | Idris.AbsSyntaxTree, Idris.AbsSyntax |
removeProof | Idris.REPL |
renderWidth | Idris.AbsSyntax |
Reorder | Idris.Core.ProofState, Idris.Core.Elaborate |
reorder_claims | Idris.Core.Elaborate |
repl | Idris.REPL |
replaceSplits | Idris.CaseSplit |
replCompletion | Idris.Completion |
REPLCompletions | Idris.IdeSlave |
replPkg | Pkg.Package |
replSettings | Idris.REPL |
report | Idris.Error |
RESERVE | IRTS.Bytecode |
reserved | Idris.ParseHelpers, Idris.Parser |
reservedOp | Idris.ParseHelpers, Idris.Parser |
resetNameIdx | Idris.AbsSyntax |
resolveProof | Idris.REPL |
resolveTC | Idris.ElabTerm |
Rewrite | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
rewrite | Idris.Core.Elaborate |
rewriteTerm | Idris.ParseExpr, Idris.Parser |
RForce | Idris.Core.TT |
rhs | Idris.Parser |
RightOK | Idris.AbsSyntax |
rmIBC | Pkg.Package |
RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
RType | Idris.Core.TT |
rt_simplify | Idris.Core.Evaluate |
Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
runClient | Idris.REPL |
runElab | Idris.Core.Elaborate |
runInnerParser | Idris.ParseHelpers, Idris.Parser |
runIO | Idris.AbsSyntax |
runparser | Idris.ParseHelpers, Idris.Parser |
runTac | Idris.ElabTerm |
RunTime | Idris.Core.CaseTree |
runtimeExceptionType | IRTS.Java.JTypes |
RVal | |
1 (Data Constructor) | IRTS.BCImp |
2 (Data Constructor) | IRTS.Bytecode |
safeToEnum | Idris.IBC |
SAlt | IRTS.Simplified |
sAlt | IRTS.Simplified |
Same | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SApp | IRTS.Simplified |
saveState | Idris.Core.Elaborate |
SC | Idris.Core.CaseTree |
SC' | Idris.Core.CaseTree |
SCase | IRTS.Simplified |
scg | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SCGEntry | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SChkCase | IRTS.Simplified |
SCon | IRTS.Simplified |
SConCase | IRTS.Simplified |
SConst | IRTS.Simplified |
SConstCase | IRTS.Simplified |
scopecheck | IRTS.Simplified |
score | Idris.Core.TT |
SDecl | IRTS.Simplified |
SDefaultCase | IRTS.Simplified |
Search | Idris.AbsSyntaxTree, Idris.AbsSyntax |
serialize | IRTS.DumpBC |
serializeBC | IRTS.DumpBC |
serializeCase | IRTS.DumpBC |
serializeDefault | IRTS.DumpBC |
serializeReg | IRTS.DumpBC |
SError | IRTS.Simplified |
setAccess | Idris.Core.Evaluate |
setAccessibility | Idris.AbsSyntax |
setAndReport | Idris.Error |
setCmdLine | Idris.AbsSyntax |
setCodegen | Idris.AbsSyntax |
SetColour | Idris.AbsSyntaxTree, Idris.AbsSyntax |
setColour | Idris.AbsSyntax |
setColourise | Idris.AbsSyntax |
SetConsoleWidth | Idris.AbsSyntaxTree, Idris.AbsSyntax |
setContext | Idris.AbsSyntax |
setCoverage | Idris.AbsSyntax |
setErrContext | Idris.AbsSyntax |
setErrLine | Idris.AbsSyntax |
setFlags | Idris.AbsSyntax |
setIBCSubDir | Idris.AbsSyntax |
setIdeSlave | Idris.AbsSyntax |
setImportDirs | Idris.AbsSyntax |
setImpShow | Idris.AbsSyntax |
setinj | Idris.Core.Elaborate |
SetInjective | Idris.Core.ProofState, Idris.Core.Elaborate |
setLogLevel | Idris.AbsSyntax |
setMetaInformation | Idris.Core.Evaluate |
setNextName | Idris.Core.Elaborate |
setNoBanner | Idris.AbsSyntax |
SetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
setOptLevel | Idris.AbsSyntax |
setOutH | Idris.AbsSyntax |
setOutputTy | Idris.AbsSyntax |
setQuiet | Idris.AbsSyntax |
setREPL | Idris.AbsSyntax |
setShowOrigErr | Idris.AbsSyntax |
setSO | Idris.AbsSyntax |
setTargetCPU | Idris.AbsSyntax |
setTargetTriple | Idris.AbsSyntax |
setTotal | Idris.Core.Evaluate |
setTotality | Idris.AbsSyntax |
setTypeCase | Idris.AbsSyntax |
setTypeInType | Idris.AbsSyntax |
setVerbose | Idris.AbsSyntax |
setWidth | Idris.AbsSyntax |
set_context | Idris.Core.Elaborate |
SExp | |
1 (Type/Class) | Idris.IdeSlave |
2 (Type/Class) | IRTS.Simplified |
SExpable | Idris.IdeSlave |
SexpList | Idris.IdeSlave |
sexpToCommand | Idris.IdeSlave |
SForeign | IRTS.Simplified |
SFun | IRTS.Simplified |
shadow | Idris.AbsSyntax |
shortType | IRTS.Java.JTypes |
showCaseTrees | IRTS.Compiler |
showCG | Idris.Core.TT |
showCImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showDeclImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showDecls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showDImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showDoc | Idris.Docs |
showEnv | Idris.Core.TT |
showEnv' | Idris.Core.TT |
showEnvDbg | Idris.Core.TT |
showErr | Idris.Error |
ShowImpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ShowIncs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ShowLibdir | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ShowLibs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showName | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ShowOrigErr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showOrigErr | Idris.AbsSyntax |
ShowProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showProof | Idris.Prover |
showSep | Idris.Core.TT |
showTm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showTmImpls | Idris.AbsSyntaxTree, Idris.AbsSyntax |
showTotal | Idris.REPL |
showTotalN | Idris.REPL |
sigmaTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
simpleCase | Idris.Core.CaseTree |
simpleConstructor | Idris.ParseData, Idris.Parser |
SimpleExpr | Idris.AbsSyntaxTree, Idris.AbsSyntax |
simpleExpr | Idris.ParseExpr, Idris.Parser |
simpleExternalExpr | Idris.ParseExpr, Idris.Parser |
simpleMethod | IRTS.Java.ASTBuilding |
simpleWhiteSpace | Idris.ParseHelpers, Idris.Parser |
simple_app | Idris.Core.Elaborate |
Simplify | Idris.Core.ProofState, Idris.Core.Elaborate |
simplify | |
1 (Function) | Idris.Core.Evaluate |
2 (Function) | IRTS.Simplified |
3 (Function) | Idris.Core.Elaborate |
simplifyCasedef | Idris.Core.Evaluate |
singleLineComment | Idris.ParseHelpers, Idris.Parser |
sInstanceN | Idris.Core.TT |
SizeChange | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SLet | IRTS.Simplified |
SLIDE | IRTS.Bytecode |
small | Idris.Core.CaseTree |
Smaller | Idris.AbsSyntaxTree, Idris.AbsSyntax |
sMN | Idris.Core.TT |
SN | Idris.Core.TT |
sname | |
1 (Function) | IRTS.Compiler |
2 (Function) | Idris.Transforms |
SNothing | IRTS.Simplified |
sNS | Idris.Core.TT |
Solve | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
solve | Idris.Core.Elaborate |
solveAll | Idris.ElabTerm |
solved | Idris.Core.ProofState, Idris.Core.Elaborate |
solveDeferred | Idris.AbsSyntax |
SOp | IRTS.Simplified |
sourcefile | Idris.IBC |
sourceTypes | IRTS.Java.JTypes |
sParentN | Idris.Core.TT |
Spec | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SpecialHeaderArg | Idris.Help |
Specialise | Idris.AbsSyntaxTree, Idris.AbsSyntax |
specialise | Idris.Core.Evaluate |
SpecialName | Idris.Core.TT |
specType | Idris.PartialEval |
splitOnLine | Idris.CaseSplit |
SProj | IRTS.Simplified |
srcPath | Idris.Imports |
SSymbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
startServer | Idris.REPL |
StartUnify | Idris.Core.ProofState, Idris.Core.Elaborate |
start_unify | Idris.Core.Elaborate |
Static | |
1 (Type/Class) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
static | Idris.ParseExpr, Idris.Parser |
STerm | Idris.Core.CaseTree |
STOREOLD | IRTS.Bytecode |
Str | Idris.Core.TT |
str | Idris.Core.TT |
string | Idris.ParseHelpers, Idris.Parser |
StringAtom | Idris.IdeSlave |
stringLiteral | Idris.ParseHelpers, Idris.Parser |
stringType | IRTS.Java.JTypes |
stripCollapsed | Idris.DataOpts |
stripLinear | Idris.AbsSyntax |
stripUnmatchable | Idris.AbsSyntax |
StrType | Idris.Core.TT |
SubReport | Idris.Core.TT |
subst | Idris.Core.TT |
substMatch | Idris.AbsSyntax |
substMatches | Idris.AbsSyntax |
substMatchesShadow | Idris.AbsSyntax |
substMatchShadow | Idris.AbsSyntax |
substNames | Idris.Core.TT |
substTerm | Idris.Core.TT |
substV | Idris.Core.TT |
suc | Idris.Transforms |
SucCase | Idris.Core.CaseTree |
sUN | Idris.Core.TT |
SUpdate | IRTS.Simplified |
SV | IRTS.Simplified |
sVar | IRTS.Simplified |
Symbol | Idris.AbsSyntaxTree, Idris.AbsSyntax |
symbol | Idris.ParseHelpers, Idris.Parser |
SymbolAtom | Idris.IdeSlave |
symbols | Idris.IBC |
SymRef | Idris.Core.TT |
Syn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SynBind | Idris.ParseExpr, Idris.Parser |
SynContext | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SynMatch | Idris.ParseExpr, Idris.Parser |
Syntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
syntaxDecl | Idris.Parser |
SyntaxInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
syntaxRule | Idris.Parser |
syntaxSym | Idris.Parser |
syntax_keywords | Idris.AbsSyntaxTree, Idris.AbsSyntax |
syntax_rules | Idris.AbsSyntaxTree, Idris.AbsSyntax |
SynTm | Idris.ParseExpr, Idris.Parser |
syn_namespace | Idris.AbsSyntaxTree, Idris.AbsSyntax |
syn_params | Idris.AbsSyntaxTree, Idris.AbsSyntax |
T | IRTS.Bytecode |
table | Idris.ParseOps, Idris.Parser |
Tac | Idris.Core.Elaborate |
TacImp | Idris.AbsSyntaxTree, Idris.AbsSyntax |
tacimpl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Tactic | Idris.Core.ProofState, Idris.Core.Elaborate |
tactic | Idris.ParseExpr, Idris.Parser |
tacticsExpr | Idris.ParseExpr, Idris.Parser |
TAILCALL | IRTS.Bytecode |
TargetCPU | Idris.AbsSyntaxTree, Idris.AbsSyntax |
targetCPU | Idris.AbsSyntax |
TargetTriple | Idris.AbsSyntaxTree, Idris.AbsSyntax |
targetTriple | Idris.AbsSyntax |
TC | Idris.Core.TT |
TC' | Idris.Core.TC, Idris.Core.TT |
TCInstance | Idris.AbsSyntaxTree, Idris.AbsSyntax |
tclift | Idris.Error |
tcname | Idris.Core.TT |
TCon | Idris.Core.TT |
tctry | Idris.Error |
tc_dictionary | Idris.Core.Evaluate |
Term | Idris.Core.TT |
terminator | Idris.ParseHelpers, Idris.Parser |
TermPart | Idris.Core.TT |
TermSize | Idris.Core.TT |
termsize | Idris.Core.TT |
TermSyntax | Idris.AbsSyntaxTree, Idris.AbsSyntax |
TermTrans | Idris.Transforms |
TestInline | Idris.AbsSyntaxTree, Idris.AbsSyntax |
testLib | Pkg.Package |
TextPart | Idris.Core.TT |
tfail | Idris.Core.TT |
thead | Idris.Core.TT |
Theorem | Idris.Core.Elaborate |
thname | Idris.Core.ProofState, Idris.Core.Elaborate |
threadType | IRTS.Java.JTypes |
TI | Idris.AbsSyntaxTree, Idris.AbsSyntax |
timestampOlder | Idris.IBC |
tldeclared | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Tmp | IRTS.Bytecode |
tnull | Idris.Core.TT |
toAlist | Idris.Core.TT |
toBC | |
1 (Function) | IRTS.BCImp |
2 (Function) | IRTS.Bytecode |
toClassType | IRTS.Java.ASTBuilding |
toCons | IRTS.Defunctionalise |
toEither | Idris.AbsSyntax |
toIBCFile | Pkg.Package |
ToIR | IRTS.Compiler |
TooManyArguments | Idris.Core.TT |
TOPBASE | IRTS.Bytecode |
toplevel | Idris.ElabTerm |
toRefType | IRTS.Java.ASTBuilding |
toSExp | Idris.IdeSlave |
toTable | Idris.ParseOps, Idris.Parser |
Total | Idris.Core.Evaluate |
TotalFn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Totality | Idris.Core.Evaluate |
totality | Idris.Parser |
TotCheck | Idris.AbsSyntaxTree, Idris.AbsSyntax |
totcheck | Idris.AbsSyntax |
TRACE | IRTS.CodegenCommon |
traceUnused | Idris.UnusedArgs |
traceWhen | Idris.Core.TT |
Transform | Idris.Transforms |
transform | |
1 (Function) | Idris.Parser |
2 (Function) | Idris.Transforms |
Trivial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
trivial | Idris.ProofSearch |
trivial' | Idris.ElabTerm |
trun | Idris.Core.TT |
Try | Idris.AbsSyntaxTree, Idris.AbsSyntax |
try | Idris.Core.Elaborate |
try' | Idris.Core.Elaborate |
tryAll | Idris.Core.Elaborate |
tryLoadLib | Util.DynamicLinker |
tryWhen | Idris.Core.Elaborate |
TSeq | Idris.AbsSyntaxTree, Idris.AbsSyntax |
TT | Idris.Core.TT |
TTOpt | Idris.Transforms |
TType | Idris.Core.TT |
TTypeInTType | Idris.Core.TT |
tt_ctxt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
txt | Idris.Core.TT |
TyDecl | Idris.Core.Evaluate |
tyOptDeclList | Idris.ParseExpr, Idris.Parser |
Type | Idris.Core.TT |
type1Doc | Idris.AbsSyntax |
TypeCase | Idris.AbsSyntaxTree, Idris.AbsSyntax |
TypeColour | Idris.Colours |
typeColour | Idris.Colours |
typeDeclList | Idris.ParseExpr, Idris.Parser |
typeExpr | Idris.ParseExpr, Idris.Parser |
TypeInfo | Idris.AbsSyntaxTree, Idris.AbsSyntax |
TypeInType | Idris.AbsSyntaxTree, Idris.AbsSyntax |
typeInType | Idris.AbsSyntax |
TypeOf | Idris.IdeSlave |
TypeOrTerm | Idris.AbsSyntaxTree, Idris.AbsSyntax |
TypeOutput | Idris.Core.TT |
TypeProviders | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ucheck | Idris.Core.Constraints |
UConstraint | |
1 (Type/Class) | Idris.Core.TT |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
uconstraints | Idris.Core.Evaluate |
UCs | Idris.Core.TT |
UExp | Idris.Core.TT |
UImplicit | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ULE | Idris.Core.TT |
ULT | Idris.Core.TT |
UN | Idris.Core.TT |
unApply | Idris.Core.TT |
Unchecked | Idris.Core.Evaluate |
Unconditional | Idris.AbsSyntaxTree, Idris.AbsSyntax |
underline | Idris.Colours |
Undo | |
1 (Data Constructor) | Idris.Core.ProofState, Idris.Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
undo | Idris.Core.Elaborate |
unIdiom | Idris.DSL |
unified | Idris.Core.ProofState, Idris.Core.Elaborate |
UnifiedD | Idris.PartialEval |
unify | Idris.Core.Unify |
unifyLog | |
1 (Function) | Idris.Core.Elaborate |
2 (Function) | Idris.ParseExpr, Idris.Parser |
unifylog | Idris.Core.ProofState, Idris.Core.Elaborate |
UnifyProblems | Idris.Core.ProofState, Idris.Core.Elaborate |
unifyProblems | Idris.Core.Elaborate |
UnifyScope | Idris.Core.TT |
uniqueBinders | Idris.Core.TT |
uniqueName | Idris.Core.TT |
uniqueNameCtxt | Idris.Core.Evaluate |
uniqueNameFrom | Idris.Core.TT |
unique_hole | Idris.Core.Elaborate |
unique_hole' | Idris.Core.Elaborate |
unitCon | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unitDecl | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unitOpts | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unitTy | Idris.AbsSyntaxTree, Idris.AbsSyntax |
UniverseError | Idris.Core.TT |
Universes | Idris.AbsSyntaxTree, Idris.AbsSyntax |
Unknown | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unList | Idris.Core.TT |
unlit | Idris.Unlit |
UnmatchedCase | Idris.Core.CaseTree |
UnsetOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unusedpos | Idris.AbsSyntaxTree, Idris.AbsSyntax |
unwrapFC | Idris.Core.TT |
upd | Idris.Coverage |
UPDATE | IRTS.Bytecode |
updateAux | Idris.Core.Elaborate |
updateContext | Idris.AbsSyntax |
updateDef | Idris.Core.TT |
updateN | Idris.AbsSyntaxTree, Idris.AbsSyntax |
updateNs | Idris.AbsSyntaxTree, Idris.AbsSyntax |
update_term | Idris.Core.Elaborate |
Usage | Idris.AbsSyntaxTree, Idris.AbsSyntax |
UseCodegen | Idris.AbsSyntaxTree, Idris.AbsSyntax |
used | Idris.UnusedArgs |
usedArg | IRTS.Lang, IRTS.Defunctionalise |
usedIn | IRTS.Lang, IRTS.Defunctionalise |
usedNamesIn | Idris.AbsSyntaxTree, Idris.AbsSyntax |
usedns | Idris.Core.ProofState, Idris.Core.Elaborate |
useREPL | Idris.AbsSyntax |
UseUndef | Idris.Core.Evaluate |
Using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
using | Idris.AbsSyntaxTree, Idris.AbsSyntax |
usingDecl | Idris.Parser |
usingDeclList | Idris.Parser |
using_ | Idris.Parser |
UVal | Idris.Core.TT |
UVar | Idris.Core.TT |
V | Idris.Core.TT |
valIBCSubDir | Idris.AbsSyntax |
Value | Idris.Core.Evaluate |
VApp | Idris.Core.Evaluate |
Var | Idris.Core.TT |
var | Idris.DSL |
VBind | Idris.Core.Evaluate |
VBLet | Idris.Core.Evaluate |
VConstant | Idris.Core.Evaluate |
Ver | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ver | |
1 (Function) | Idris.IBC |
2 (Function) | Idris.REPL |
VErased | Idris.Core.Evaluate |
verbatimStringLiteral | Idris.ParseExpr, Idris.Parser |
Verbose | Idris.AbsSyntaxTree, Idris.AbsSyntax |
verbose | Idris.AbsSyntax |
ViaC | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ViaJava | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ViaJavaScript | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ViaLLVM | Idris.AbsSyntaxTree, Idris.AbsSyntax |
ViaNode | Idris.AbsSyntaxTree, Idris.AbsSyntax |
VImpossible | Idris.Core.Evaluate |
vinstances | Idris.Core.TT |
vivid | Idris.Colours |
VoidType | Idris.Core.TT |
voidType | IRTS.Java.JTypes |
VP | Idris.Core.Evaluate |
VProj | Idris.Core.Evaluate |
VTmp | Idris.Core.Evaluate |
vToP | Idris.Core.TT |
VType | Idris.Core.Evaluate |
VV | Idris.Core.Evaluate |
WarnOnly | Idris.AbsSyntaxTree, Idris.AbsSyntax |
WarnPartial | Idris.AbsSyntaxTree, Idris.AbsSyntax |
weakenEnv | Idris.Core.TT |
weakenTm | Idris.Core.TT |
weakenTmEnv | Idris.Core.TT |
wExpr | Idris.Parser |
whereBlock | Idris.Parser |
WhereN | Idris.Core.TT |
whiteSpace | Idris.ParseHelpers, Idris.Parser |
withErrorReflection | Idris.ElabTerm |
Wk | Idris.Core.TT |
WkEnv | Idris.Core.TT |
WkEnvTT | Idris.Core.TT |
writeIBC | Idris.IBC |
zero | Idris.Transforms |
zname | |
1 (Function) | IRTS.Compiler |
2 (Function) | Idris.Transforms |
~&&~ | IRTS.Java.ASTBuilding |
~==~ | IRTS.Java.ASTBuilding |
~> | IRTS.Java.ASTBuilding |