Rp-utilities
Some useful tools for rp-rewriter
Subtopics
- Rp-other-utilities
- Some names that are aliases to other tools
- Rule-syntaxp
- Syntax check for a 'rule' defined with rp::custom-rewrite-rule. If
warning key is set to non-nil, a warning is issued for failures.
- Defthm-lambda
- A useful utility to use rewrite rules that has lambda expression on
RHS for RP-Rewriter.
- 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
- 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.
- Show-rules
- Sets whether or not RP-Rewriter should print used rules when rewriting
a conjecture.
- Set-rp-backchain-limit
- Number of steps RP-Rewriter can take when rewriting the hypothesis of
a lemma
- Defthmrp
- A defthm macro that calls RP-Rewriter as a clause processor with some
capabilities.
- Preserve-current-theory
- A macro that detects the changes in the theory when a book is
included, and retains the current theory
- Context-from-rp
- Expands the context with the side-conditions from the term
- Falist-consistent
- Given a falist term (falist * *), checks consistence of arguments.
- Ex-from-rp-loose
- Same as ex-from-rp when term is rp-termp but
a little faster.
- Ex-from-rp
- Extracts a term if it is wrapped in an rp instance.
- Rp-equal
- Check if two terms are equivalent by discarding rp terms
- Set-rw-step-limit
- Number of steps RP-Rewriter can take when rewriting a conjecture.
- Rp-equal-cnt
- Same as rp-equal but when counts down from cnt and starts ~
using 'equal' when it hits 0.
- Ex-from-rp-all2
- Removes all instances of 'rp' from a term, including the stuff under falist
- Rp-termp
- Similarly to pseudo-termp, defines the syntax for terms.
- Rp-equal-cw
- Same as rp-equal but prints a mismatch.
- Ex-from-rp-all
- Removes all instances of 'rp' from a term
- Set-rp-backchain-limit-throws-error
- Whether or not to throw an error when backchain-limit is reached
- Include-fnc-subterms
- Searches a list of terms for an instance of fnc. Returns t or nil.
- Include-fnc
- Searches a term for an instance of fnc. Returns t or nil.
