RApp | Core.TT |
rational | Util.Pretty |
Raw | |
1 (Type/Class) | Core.TT |
2 (Data Constructor) | IRTS.CodegenCommon |
RawDatatype | Core.TT |
RawFun | |
1 (Type/Class) | Core.TT |
2 (Data Constructor) | Core.TT |
RawOutput | Idris.AbsSyntaxTree, Idris.AbsSyntax |
raw_apply | Core.TT |
raw_unapply | Core.TT |
RBind | Core.TT |
rbrace | Util.Pretty |
rbrack | Util.Pretty |
RConst | Core.TT |
RConstant | Core.TT |
RData | Core.TT |
RDatatype | Core.TT |
RDef | Core.TT |
REBASE | IRTS.Bytecode |
receiveInput | Idris.Prover |
recheck | Core.Typecheck |
recheckC | Idris.ElabDecls |
record | Idris.ParseData, Idris.Parser |
recordType | Idris.ParseExpr, Idris.Parser |
recursive | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reduceDoc | Util.Pretty |
Ref | Core.TT |
Refine | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reflCall | Idris.ElabTerm |
Reflect | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reflect | Idris.ElabTerm |
reflectBinder | Idris.ElabTerm |
reflectConstant | Idris.ElabTerm |
reflectEnv | Idris.ElabTerm |
reflectErr | Idris.ElabTerm |
Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
reflectName | Idris.ElabTerm |
reflectNameType | Idris.ElabTerm |
reflectUExp | Idris.ElabTerm |
reflm | Idris.ElabTerm |
Reg | |
1 (Type/Class) | IRTS.BCImp |
2 (Type/Class) | IRTS.Bytecode |
Regret | Core.ProofState, Core.Elaborate |
regret | Core.Elaborate |
reify | Idris.ElabTerm |
reifyApp | Idris.ElabTerm |
reifyRaw | Idris.ElabTerm |
reifyRawApp | 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 |
render | Util.Pretty |
renderStyle | Util.Pretty |
Reorder | Core.ProofState, Core.Elaborate |
reorder_claims | Core.Elaborate |
repl | Idris.REPL |
replaceSplits | Idris.CaseSplit |
replCompletion | Idris.Completion |
REPLCompletions | Idris.IdeSlave |
replSettings | Idris.REPL |
report | Idris.Error |
RESERVE | IRTS.Bytecode |
reserved | Idris.ParseHelpers, Idris.Parser |
reservedOp | Idris.ParseHelpers, Idris.Parser |
resolveProof | Idris.REPL |
resolveTC | Idris.ElabTerm |
Rewrite | |
1 (Data Constructor) | Core.ProofState, Core.Elaborate |
2 (Data Constructor) | Idris.AbsSyntaxTree, Idris.AbsSyntax |
rewrite | Core.Elaborate |
rewriteTerm | Idris.ParseExpr, Idris.Parser |
RForce | Core.TT |
RFunction | Core.TT |
rhs | Idris.Parser |
ribbonsPerLine | Util.Pretty |
RightOK | Idris.AbsSyntax |
rmFile | Util.System |
rmIBC | Pkg.Package |
RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
rparen | Util.Pretty |
RProgram | Core.TT |
RType | Core.TT |
rtype | Core.TT |
rt_simplify | Core.Evaluate |
Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
runClient | Idris.REPL |
runElab | Core.Elaborate |
runIdris | Main |
runInnerParser | Idris.ParseHelpers, Idris.Parser |
runIO | Idris.AbsSyntax |
runparser | Idris.ParseHelpers, Idris.Parser |
runTac | Idris.ElabTerm |
RunTime | Core.CaseTree |
runtimeExceptionType | IRTS.Java.JTypes |
RVal | |
1 (Data Constructor) | IRTS.BCImp |
2 (Data Constructor) | IRTS.Bytecode |
rval | Core.TT |