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 |