| RApp | Idris.Core.TT |
| RArg | Idris.Reflection |
| rArgToPArg | Idris.Reflection |
| Raw | |
| 1 (Type/Class) | Idris.Core.TT |
| 2 (Data Constructor) | IRTS.CodegenCommon |
| rawBool | Idris.ElabTerm |
| rawCons | Idris.ElabTerm |
| RawHtml | Idris.Docstrings |
| 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 |
| RConstraint | Idris.Reflection |
| RDeclare | Idris.Reflection |
| REBASE | IRTS.Bytecode |
| receiveInput | Idris.Prover |
| recents | Idris.Core.ProofState, Idris.Core.Elaborate |
| recheck | Idris.Core.Typecheck |
| recheckC | Idris.Elab.Utils |
| recheckC_borrowing | Idris.Elab.Utils |
| recheck_borrowing | Idris.Core.Typecheck |
| recinfo | Idris.ElabDecls |
| record | Idris.ParseData, Idris.Parser |
| recordType | Idris.ParseExpr, Idris.Parser |
| rec_elabDecl | 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 |
| reflectBinderQuote | Idris.ElabTerm |
| reflectBinderQuotePattern | Idris.ElabTerm |
| reflectConstant | Idris.ElabTerm |
| reflectCtxt | Idris.ElabTerm |
| reflectEnv | Idris.ElabTerm |
| reflectErr | Idris.ElabTerm |
| reflectFC | Idris.ElabTerm |
| Reflection | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| ReflectionError | Idris.Core.TT |
| ReflectionFailed | Idris.Core.TT |
| reflectName | Idris.ElabTerm |
| reflectNameQuotePattern | Idris.ElabTerm |
| reflectNameType | Idris.ElabTerm |
| reflectRaw | Idris.ElabTerm |
| reflectRawQuote | Idris.ElabTerm |
| reflectRawQuotePattern | Idris.ElabTerm |
| reflectTTQuote | Idris.ElabTerm |
| reflectTTQuotePattern | Idris.ElabTerm |
| reflectUExp | Idris.ElabTerm |
| reflectUniverse | Idris.ElabTerm |
| reflErrName | Idris.ElabTerm |
| reflm | Idris.ElabTerm |
| refocus | Idris.Core.ProofTerm |
| refsIn | Idris.Core.TT |
| 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 |
| reifyArithTy | Idris.ElabTerm |
| reifyIntTy | Idris.ElabTerm |
| reifyNativeTy | Idris.ElabTerm |
| reifyRaw | Idris.ElabTerm |
| reifyRawApp | Idris.ElabTerm |
| reifyReportPart | Idris.ElabTerm |
| reifyReportParts | 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 |
| reifyTyDecl | Idris.ElabTerm |
| Reload | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RemoveOpt | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| removeOptimise | Idris.AbsSyntax |
| removeProof | Idris.REPL |
| renderDocstring | Idris.Docstrings |
| renderDocTerm | Idris.Docstrings |
| renderExternal | Idris.Output |
| renderHtml | Idris.Docstrings |
| Reorder | Idris.Core.ProofState, Idris.Core.Elaborate |
| reorder_claims | Idris.Core.Elaborate |
| repl | Idris.REPL |
| replaceSplits | Idris.CaseSplit |
| replCompletion | Idris.Completion |
| REPLCompletions | Idris.IdeMode |
| replPkg | Pkg.Package |
| replSettings | Idris.REPL |
| repl_definitions | Idris.ASTUtils |
| report | Idris.Error |
| reportParserWarnings | Idris.ParseHelpers, Idris.Parser |
| RESERVE | IRTS.Bytecode |
| reserved | Idris.ParseHelpers, Idris.Parser |
| reservedOp | Idris.ParseHelpers, Idris.Parser |
| resetNameIdx | Idris.AbsSyntax |
| resolveProof | Idris.REPL |
| resolveTC | Idris.ElabTerm |
| resTC' | Idris.ElabTerm |
| resultCaseDecls | Idris.ElabTerm |
| resultContext | Idris.ElabTerm |
| resultMetavars | Idris.ElabTerm |
| resultTerm | Idris.ElabTerm |
| resultTyDecls | 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 |
| RExplicit | Idris.Reflection |
| RForce | Idris.Core.TT |
| rhs | Idris.Parser |
| RightOK | Idris.AbsSyntax |
| RImplicit | Idris.Reflection |
| rmFile | Util.System |
| rmIBC | Pkg.Package |
| rmIdx | Pkg.Package |
| RmProof | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| RTyDecl | Idris.Reflection |
| RType | Idris.Core.TT |
| rt_simplify | Idris.Core.Evaluate |
| Rule | Idris.AbsSyntaxTree, Idris.AbsSyntax |
| runArgParser | Idris.CmdOptions |
| runClient | Idris.REPL |
| runElab | Idris.Core.Elaborate |
| runIdeModeCommand | Idris.REPL |
| runInnerParser | Idris.ParseHelpers, Idris.Parser |
| runIO | Idris.AbsSyntax |
| runMain | Idris.REPL |
| runparser | Idris.ParseHelpers, Idris.Parser |
| runTac | Idris.ElabTerm |
| RunTactic' | Idris.Core.ProofTerm |
| runTactical | Idris.ElabTerm |
| runTactics | Idris.ParseExpr, Idris.Parser |
| RunTime | Idris.Core.CaseTree |
| RUType | Idris.Core.TT |
| RVal | |
| 1 (Data Constructor) | IRTS.BCImp |
| 2 (Data Constructor) | IRTS.Bytecode |