Index - R
| rActs | Theory.Model.Rule, Theory.Model, Theory |
| range | Theory.Model, Theory |
| rangeVFresh | Theory.Model, Theory |
| rankProofMethods | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| rational | Theory.Text.Pretty |
| rawEdgeRel | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| rawLessRel | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| rbrace | Theory.Text.Pretty |
| rbrack | Theory.Text.Pretty |
| rConc | Theory.Model.Rule, Theory.Model, Theory |
| rConcs | Theory.Model.Rule, Theory.Model, Theory |
| reducibleFormula | Theory.Constraint.Solver.Reduction |
| Reduction | Theory.Constraint.Solver.Reduction |
| refineWithTypingAsms | Theory.Constraint.Solver.CaseDistinctions, Theory.Constraint.Solver, Theory.Proof, Theory |
| removeLemma | Theory |
| removeRedundantCases | Theory.Constraint.Solver.CaseDistinctions |
| removeRenamings | Theory.Model, Theory |
| removeSolvedSplitGoals | Theory.Constraint.Solver.Reduction |
| rename | Theory.Model, Theory |
| renameAvoiding | Theory.Model, Theory |
| renameDropNamehint | Theory.Model, Theory |
| renameFresh | Theory.Model, Theory |
| renameFreshAvoiding | Theory.Model, Theory |
| renamePrecise | Theory.Model, Theory |
| render | Theory.Text.Pretty |
| renderStyle | Theory.Text.Pretty |
| replaceSorryProver | Theory.Proof, Theory |
| reservedRuleNames | Theory.Model.Rule, Theory.Model, Theory |
| resolveNodeConcFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| resolveNodePremFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| restrict | Theory.Model, Theory |
| restrictVFresh | Theory.Model, Theory |
| ReuseLemma | Theory |
| ribbonsPerLine | Theory.Text.Pretty |
| rInfo | Theory.Model.Rule, Theory.Model, Theory |
| root | Theory.Proof, Theory |
| roundRobinHeuristic | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| rparen | Theory.Text.Pretty |
| rPrem | Theory.Model.Rule, Theory.Model, Theory |
| rPrems | Theory.Model.Rule, Theory.Model, Theory |
| RRule | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| rrulesForMaudeSig | Theory.Model, Theory |
| Rule | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| RuleAC | Theory.Model.Rule, Theory.Model, Theory |
| RuleACConstrs | Theory.Model.Rule, Theory.Model, Theory |
| RuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| ruleACIntrToRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| ruleACIntrToRuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| ruleACToIntrRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| RuleInfo | Theory.Model.Rule, Theory.Model, Theory |
| ruleInfo | Theory.Model.Rule, Theory.Model, Theory |
| RuleItem | Theory |
| ruleName | Theory.Model.Rule, Theory.Model, Theory |
| runAutoProver | Theory.Proof, Theory |
| runProver | Theory.Proof, Theory |
| runReduction | Theory.Constraint.Solver.Reduction |