Rp-utilities
Some useful tools for rp-rewriter
Subtopics
- Defthmrp
- A defthm macro that calls RP-Rewriter as a clause processor with custom arguments.
- Show-rules
- Sets whether or not RP-Rewriter should print used rules when rewriting
a conjecture.
- Def-rw-opener-error
- A macro that causes RP-Rewriter to throw a readable error when a
certain pattern occurs.
- Valid-sc
- A function that checks the side-conditions in a term is correct
- Set-rp-backchain-limit
- Number of steps RP-Rewriter can take when rewriting the hypothesis of
a lemma
- Fetch-new-theory
- A macro that detects the changes in the theory when a book is
included, and creates a macro to enable users to enable and disable the new theory.
- Ex-from-rp
- Extracts a term if it is wrapped in an rp instance.
- Rp-other-utilities
- Some names that are aliases to other tools
- Rp-equal
- Check if two terms are equivalent by discarding rp terms
- Preserve-current-theory
- A macro that detects the changes in the theory when a book is
included, and retains the current theory
- Set-rw-step-limit
- Number of steps RP-Rewriter can take when rewriting a conjecture.
- Rp-termp
- Similarly to pseudo-termp, defines the syntax for terms.
- Include-fnc
- Searches a term for an instance of fnc. Returns t or nil.
- Set-rp-backchain-limit-throws-error
- Whether or not to throw an error when backchain-limit is reached
- Defwarrant-rp
- Calls defwarrant and register the resulting rule with RP, and disbled executable counterpart for the warrant
- Create-case-match-macro
- Creates a function and a macro to replace case-match, and prevent
excessive casesplitting when proving lemmas.
